Encodings of Bounded LTL Model Checking in Effectively Propositional Logic

DOI10.1007/978-3-540-73595-3_24zbMath1213.68386OpenAlexW2124498114MaRDI QIDQ3608783

Andrei Voronkov, Juan Antonio Navarro Pérez

Publication date: 6 March 2009

Published in: Automated Deduction – CADE-21 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-73595-3_24

Mathematics Subject Classification ID

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

Related Items (6)

Symbolic backward reachability with effectively propositional logic. Application to security policy analysis ⋮ Deciding Effectively Propositional Logic Using DPLL and Substitution Sets ⋮ Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning ⋮ Planning with Effectively Propositional Logic ⋮ Deciding effectively propositional logic using DPLL and substitution sets ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates

Uses Software

• NuSMV
• TPTP

This page was built for publication: Encodings of Bounded LTL Model Checking in Effectively Propositional Logic