Algorithmic metatheorems for decidable LTL model checking over infinite systems

DOI10.1007/978-3-642-12032-9_16MaRDI QIDQ3557854zbMATH OpenOpenAlexFDO

Authors Anthony Widjaja To, Leonid Libkin

Publication date 27 April 2010

Published in Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-12032-9_16

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A decidability result for the model checking of infinite-state systems
• scientific article; zbMATH DE number 1903366
• scientific article; zbMATH DE number 1956650
• An automata-theoretic approach to infinite-state systems
• Model checking CTL over restricted classes of automatic structures

Cited in

(13)

• Model checking CTL over restricted classes of automatic structures
• The complexity of reversal-bounded model-checking
• Fair termination for parameterized probabilistic concurrent systems
• scientific article; zbMATH DE number 1903366 (Why is no real title available?)
• Closure properties of synchronized relations
• Graph logics with rational relations: the role of word combinatorics
• Refining the process rewrite systems hierarchy via ground tree rewrite systems
• Refining the process rewrite systems hierarchy via ground tree rewrite systems
• Decidable models of integer-manipulating programs with recursive parallelism
• Regular model checking revisited
• Ramsey quantifiers over automatic structures: complexity and applications to verification
• Regular model checking for systems with effectively regular reachability relation
• Synchronizing relations on words

This page was built for publication: Algorithmic metatheorems for decidable LTL model checking over infinite systems

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