Verifying increasingly expressive temporal logics for infinite-state systems

DOI10.1145/3060257MaRDI QIDQ4640287zbMATH OpenOpenAlexFDO

Authors Byron Cook, Heidy Khlaaf, Nir Piterman

Publication date 17 May 2018

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://discovery.ucl.ac.uk/id/eprint/10075277/

zbMATH Keywords

CTL*model checking

Mathematics Subject Classification ID

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

Recommendations

• On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
• Temporal prophecy for proving temporal properties of infinite-state systems
• TEMPORAL LOGICS FOR TRACE SYSTEMS: ON AUTOMATED VERIFICATION
• Constraint-based abstract semantics for temporal logic: a direct approach to design and implementation
• An automata-theoretic approach to infinite-state systems

Cited in

(10)

• On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
• Temporal prophecy for proving temporal properties of infinite-state systems
• \textsc{LTL} falsification in infinite-state systems
• Automatic discovery of fair paths in infinite-state transition systems
• Proving the existence of fair paths in infinite-state systems
• scientific article; zbMATH DE number 1670842 (Why is no real title available?)
• Efficient CTL verification via Horn constraints solving
• Temporal verification of programs via first-order fixpoint logic
• First order Büchi automata and their application to verification of LTL specifications
• Synchronized CTL over one-counter automata

This page was built for publication: Verifying increasingly expressive temporal logics for infinite-state systems

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