Taking Some Burden Off an Explicit CTL Model Checker

DOI10.1007/978-3-030-21571-2_18MaRDI QIDQ6184728zbMATH OpenOpenAlexFDO

Authors Torsten Liebke, Karsten Wolf

Publication date 29 January 2024

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-21571-2_18

zbMATH Keywords

CTL model checkingpartial order reduction

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Publication:4507830
• scientific article; zbMATH DE number 1487478
• Simplification of CTL formulae for efficient model checking of Petri nets
• Model Checking CTL is Almost Always Inherently Sequential
• scientific article; zbMATH DE number 2102715

Cites work

• A partial approach to model checking
• A partial order approach to branching time logic model checking.
• Applying CEGAR to the Petri net state equation
• Depth-First Search and Linear Graph Algorithms
• scientific article; zbMATH DE number 1708021 (Why is no real title available?)
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 1059329 (Why is no real title available?)
• scientific article; zbMATH DE number 1069483 (Why is no real title available?)
• scientific article; zbMATH DE number 1515297 (Why is no real title available?)
• scientific article; zbMATH DE number 4119616 (Why is no real title available?)
• Model Checking Software
• More efficient on-the-fly LTL verification with Tarjan's algorithm
• New algorithms for deciding the siphon-trap property
• Question-guided stubborn set methods for state properties
• Simplification of CTL formulae for efficient model checking of Petri nets
• Stubborn set intuition explained
• TAPAAL 2.0: integrated development environment for timed-arc Petri nets

Cited in

(3)

• 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

This page was built for publication: Taking Some Burden Off an Explicit CTL Model Checker

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