Simplification of CTL formulae for efficient model checking of Petri nets

DOI10.1007/978-3-319-91268-4_8MaRDI QIDQ2280185zbMATH OpenOpenAlexFDO

Authors Jakob Dyhr, Mads Johannsen, Jiří Srba, Frederik M. Bønneland, Peter Gjøl Jensen

Publication date 18 December 2019

Full work available at URL https://doi.org/10.1007/978-3-319-91268-4_8

Mathematics Subject Classification ID

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

Recommendations

• Solving finite-linear-path CTL-formulas using the CEGAR approach
• scientific article; zbMATH DE number 1852166
• CTL* model checking for time Petri nets
• Sequential and distributed model checking of Petri net specifications
• Decompositional Petri Net Reductions

Cited in

(12)

• Symbolic and structural model-checking
• Skeleton abstraction for universal temporal properties
• scientific article; zbMATH DE number 1696466 (Why is no real title available?)
• Taking Some Burden Off an Explicit CTL Model Checker
• Structural reductions revisited
• Solving finite-linear-path CTL-formulas using the CEGAR approach
• Automata-driven partial order reduction and guided search for LTL model checking
• Using approximation for the verification of token-scaling models
• Avoiding exponential explosion in Petri net models of control flows
• Skeleton Abstraction for Universal Temporal Properties
• Sequential and distributed model checking of Petri net specifications
• Decompositional Petri Net Reductions

Describes a project that uses

Uses Software

• TAPAAL

This page was built for publication: Simplification of CTL formulae for efficient model checking of Petri nets

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