Model checking LTL using constraint programming

DOI10.1007/3-540-63139-9_26MaRDI QIDQ6487366zbMATH OpenFDO

Authors Javier Esparza

Publication date 9 December 2022

Full work available at URL https://doi.org/10.1007/3-540-63139-9_26

Mathematics Subject Classification ID

Temporal logic (03B44) Analysis of algorithms and problem complexity (68Q25) 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

• scientific article; zbMATH DE number 1852166
• scientific article; zbMATH DE number 1755146
• BDD-based bounded model checking for temporal properties of 1-safe Petri nets
• Applications and Theory of Petri Nets 2004
• scientific article; zbMATH DE number 1822435

Cites work

• A stubborn attack on state explosion
• An improved algorithm for decentralized extrema-finding in circular configurations of processes
• Free Choice Petri Nets
• scientific article; zbMATH DE number 976922 (Why is no real title available?)
• Model checking LTL using constraint programming
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Reasoning about infinite computations
• Trapping mutual exclusion in the box calculus

Cited in

(19)

• Replication, refinement \& reachability: complexity in dynamic condition-response graphs
• Decidability of infinite-state timed CCP processes and first-order LTL
• Automatic software model checking via constraint logic
• scientific article; zbMATH DE number 1615250 (Why is no real title available?)
• scientific article; zbMATH DE number 1696809 (Why is no real title available?)
• BDD-based bounded model checking for temporal properties of 1-safe Petri nets
• Model Checking LTL Formulae in RAISE with FDR
• scientific article; zbMATH DE number 408787 (Why is no real title available?)
• Constraint LTL satisfiability checking without automata
• scientific article; zbMATH DE number 1852166 (Why is no real title available?)
• scientific article; zbMATH DE number 1884391 (Why is no real title available?)
• Bounded LTL model checking with stable models
• Manipulating LTL Formulas Using Spot 1.0
• LTL model checking with Neco
• Safety, liveness and run-time refinement for modular process-aware information systems with dynamic sub processes
• Computer Science Logic
• Applications and Theory of Petri Nets 2004
• Constrained properties, semilinear systems, and Petri nets
• Model checking LTL using constraint programming

This page was built for publication: Model checking LTL using constraint programming

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