Model checking LTL using constraint programming

DOI10.1007/3-540-63139-9_26zbMath1523.6804MaRDI QIDQ6487366

Unnamed Author, Javier Esparza

Publication date: 9 December 2022

Mathematics Subject Classification ID

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) Temporal logic (03B44)

Related Items (4)

Replication, refinement \& reachability: complexity in dynamic condition-response graphs ⋮ Decidability of infinite-state timed CCP processes and first-order LTL ⋮ Model checking LTL using constraint programming ⋮ Safety, Liveness and Run-Time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes

Cites Work

• Unnamed Item
• Trapping mutual exclusion in the box calculus
• A stubborn attack on state explosion
• Reasoning about infinite computations
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• An improved algorithm for decentralized extrema-finding in circular configurations of processes
• Free Choice Petri Nets
• Model checking LTL using constraint programming

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