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

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

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

(12)

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

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)