Pre- and post-agglomerations for LTL model checking

DOI10.1007/3-540-44988-4_22MaRDI QIDQ2766576zbMATH OpenFDO

Authors Denis Poitrenaud, Jean-François Pradat-Peyre

Publication date 13 June 2002

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

Full work available at URL https://doi.org/10.1007/3-540-44988-4_22

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Net reductions for LTL model-checking
• Decompositional Petri Net Reductions
• Simplification of CTL formulae for efficient model checking of Petri nets
• A more efficient time Petri net state space abstraction useful to model checking timed linear properties
• Applications and Theory of Petri Nets 2004

Cited in

(5)

• LTL under reductions with weaker conditions than stutter invariance
• Self-Loop Aggregation Product — A New Hybrid Approach to On-the-Fly LTL Model Checking
• Decompositional Petri Net Reductions
• Net reductions for LTL model-checking
• Structural reductions and stutter sensitive properties

This page was built for publication: Pre- and post-agglomerations for LTL model checking

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