Bounded LTL model checking with stable models

DOI10.1017/S1471068403001790zbMath1079.68058OpenAlexW2119055724MaRDI QIDQ4815032

Keijo Heljanko, Ilkka Niemelä

Publication date: 19 August 2004

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s1471068403001790

zbMATH Keywords

bounded model checkingLTLstable modelsstep semantics.

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Reasoning about actions with Temporal Answer Sets, Answer set programming based on propositional satisfiability, Model checking multi-agent systems with logic based Petri nets, Reasoning about actions with \(\mathcal{EL}\) ontologies and temporal answer sets for DLTL, Exploiting step semantics for efficient bounded model checking of asynchronous systems, SMT-based scenario verification for hybrid systems, Business process verification with constraint temporal answer set programming, Logic programs with abstract constraint atoms: the role of computations, A translational approach to constraint answer set solving, Logic programming for finding models in the logics of knowledge and its applications: A case study, Justifications for logic programs under answer set semantics

Uses Software

• PROD
• SPIN
• NuSMV
• Smodels
• Chaff