LTL model checking for modular Petri nets

DOI10.1007/978-3-540-27793-4_17MaRDI QIDQ5712335zbMATH OpenOpenAlexDBLPFDO

Authors Timo Latvala, Marko M. Mäkelä

Publication date 23 December 2005

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

Full work available at URL https://doi.org/10.1007/b98283

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

• An Incremental and Modular Technique for Checking LTL∖X Properties of Petri Nets
• Modular Analysis of Petri Nets
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• Parallel LTL-X model checking of high-level Petri nets based on unfoldings
• Model checking LTL using constraint programming

Cited in

(18)

• An experience in proving regular networks of processes by modular model checking
• Replication, refinement \& reachability: complexity in dynamic condition-response graphs
• Model checking Petri nets with MSVL
• Pre- and post-agglomerations for LTL model checking
• Maria: Modular reachability analyser for algebraic system nets
• scientific article; zbMATH DE number 1822435 (Why is no real title available?)
• Model checking safety properties in modular high-level nets
• Decompositional Petri Net Reductions
• An Incremental and Modular Technique for Checking LTL∖X Properties of Petri Nets
• Model checking LTL properties of high-level Petri nets with fairness constraints
• Net reductions for LTL model-checking
• LTL model checking with Neco
• Safety, liveness and run-time refinement for modular process-aware information systems with dynamic sub processes
• Parallel LTL-X model checking of high-level Petri nets based on unfoldings
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• Formal verification for event stream processing: model checking of BeepBeep stream processing pipelines
• Model checking LTL using constraint programming
• On the complexity of the linear-time μ-calculus for Petri Nets

Describes a project that uses

Uses Software

• PROD
• Maria
• LTL2BA

This page was built for publication: LTL model checking for modular Petri nets

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