Model checking LTL using constraint programming

DOI10.1007/3-540-63139-9_26zbMATH Open1523.6804MaRDI QIDQ6487366FDOQ6487366

Authors: Javier Esparza 

Publication date: 9 December 2022

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

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• A stubborn attack on state explosion
• An improved algorithm for decentralized extrema-finding in circular configurations of processes
• Free Choice Petri Nets
• 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)

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

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)