Memory efficient algorithms for the verification of temporal properties

DOI10.1007/BFB0023737MaRDI QIDQ4037388zbMATH OpenFDO

Authors Moshe Y. Vardi, Pierre Wolper, Mihalis Yannakakis, Costas Courcoubetis

Publication date 18 May 1993

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0023737

zbMATH Keywords

Büchi automataemptiness problemverification of temporal properties of finite-state programs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 177248
• Automatic Verification of Sequential Circuits Using Temporal Logic
• Verifying temporal properties of sequential machines without building their state diagrams
• On-the-fly verification of linear temporal logic
• The complexity of probabilistic verification

Cited in

(17)

• Using partial orders for the efficient verification of deadlock freedom and safety properties
• Applicability of fair simulation
• On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties
• Automata-driven partial order reduction and guided search for LTL model checking
• Model checking for hybrid branching-time logics
• More efficient on-the-fly LTL verification with Tarjan's algorithm
• A space-efficient simulation algorithm on probabilistic automata
• Correcting a Space-Efficient Simulation Algorithm
• A Space-Efficient Probabilistic Simulation Algorithm
• From Philosophical to Industrial Logics
• scientific article; zbMATH DE number 177240 (Why is no real title available?)
• scientific article; zbMATH DE number 177248 (Why is no real title available?)
• LTL parameter synthesis of parametric timed automata
• Component-wise incremental LTL model checking
• From Monadic Logic to PSL
• Model checking \(\omega \)-regular properties with decoupled search
• Theoretical foundations of handling large substitution sets in temporal integrity monitoring

This page was built for publication: Memory efficient algorithms for the verification of temporal properties

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