Bounded LTL model checking with stable models

DOI10.1017/S1471068403001790MaRDI QIDQ4815032zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• scientific article; zbMATH DE number 1884391
• Model Checking Abstract State Machines with Answer Set Programming
• Model checking LTL using constraint programming
• scientific article; zbMATH DE number 1863166
• scientific article; zbMATH DE number 1337888

Cited in

(21)

• 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
• Semi-external LTL Model Checking
• Model checking multi-agent systems with logic based Petri nets
• Model Checking Abstract State Machines with Answer Set Programming
• scientific article; zbMATH DE number 1903359 (Why is no real title available?)
• scientific article; zbMATH DE number 1863166 (Why is no real title available?)
• Exploiting step semantics for efficient bounded model checking of asynchronous systems
• Reasoning about actions with Temporal Answer Sets
• Answer set programming based on propositional satisfiability
• Formal Methods in Computer-Aided Design
• A translational approach to constraint answer set solving
• Bounded model checking with SNF, alternating automata, and Büchi automata
• Checking bounded reachability in asynchronous systems by symbolic event tracing
• Justifications for logic programs under answer set semantics
• Logic programming for finding models in the logics of knowledge and its applications: a case study
• scientific article; zbMATH DE number 7559425 (Why is no real title available?)
• scientific article; zbMATH DE number 1884391 (Why is no real title available?)
• Reasoning about actions with \(\mathcal{EL}\) ontologies and temporal answer sets for DLTL
• Theory and Applications of Satisfiability Testing

Describes a project that uses

Uses Software

• Chaff
• Smodels
• NuSMV
• SPIN
• PROD

This page was built for publication: Bounded LTL model checking with stable models

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