A CTL* Model Checker for Petri Nets

DOI10.1007/978-3-030-51831-8_21zbMath1503.68179OpenAlexW3037724080MaRDI QIDQ5100762

Elvio Gilberto Amparore, Francesco Gallà, Susanna Donatelli

Publication date: 1 September 2022

Published in: Application and Theory of Petri Nets and Concurrency (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-51831-8_21

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)

Related Items (1)

Taming strategy logic: non-recurrent fragments

Uses Software

• TINA
• SPIN
• LTSmin
• SPOT
• nuXmv
• Meddly
• Sylvan

Cites Work

• Results on the propositional \(\mu\)-calculus
• CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
• Reasoning about infinite computations
• Sylvan
• Practical CTL* model checking: Should SPIN be extended?
• “Sometimes” and “not never” revisited
• The tool TINA – Construction of abstract state spaces for petri nets and time petri nets
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A CTL* Model Checker for Petri Nets