Implementing LTL model checking with net unfoldings

DOI10.1007/3-540-45139-0_4MaRDI QIDQ4531752zbMATH OpenFDO

Authors Javier Esparza, Keijo Heljanko

Publication date 23 May 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2057/20570037

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Computer Aided Verification
• A new unfolding approach to LTL model checking
• scientific article; zbMATH DE number 1822435
• Unfoldings of unbounded Petri nets
• Designing a LTL model-checker based on unfolding graphs

Cited in

(14)

• Executability of scenarios in Petri nets
• Model checking using net unfoldings
• Path planning for robotic teams based on LTL specifications and Petri net models
• Model checking Petri nets with MSVL
• A new unfolding approach to LTL model checking
• Designing a LTL model-checker based on unfolding graphs
• Efficient Contextual Unfolding
• Decompositional Petri Net Reductions
• Efficient unfolding of contextual Petri nets
• Model checking using net unfoldings
• Computer Aided Verification
• A Practical Approach to Verification of Mobile Systems Using Net Unfoldings
• Formal verification for event stream processing: model checking of BeepBeep stream processing pipelines
• Model checking \(\omega \)-regular properties with decoupled search

Describes a project that uses

Uses Software

• SPIN
• PROD

This page was built for publication: Implementing LTL model checking with net unfoldings

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4531752)