scientific article; zbMATH DE number 177248

MaRDI QIDQ4037099zbMATH OpenFDO

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

Publication date 18 May 1993

zbMATH Keywords

automata on infinite wordsBüchi automatacomputer protocolsemptiness problemfinite-state programsproduct automatonreachability analysistemporal propertiesverification

Mathematics Subject Classification ID

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

Recommendations

• Memory efficient algorithms for the verification of temporal properties
• 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

(26)

• An explicit transition system construction approach to LTL satisfiability checking
• On a class of timer hybrid systems reducible to finite state automata
• Iterative bounded synthesis for efficient cycle detection in parametric timed automata
• GSTE is partitioned model checking
• Distributed breadth-first search LTL model checking
• Optimized temporal monitors for SystemcC
• Analysing sanity of requirements for avionics systems
• Explicit-state model checking
• Partial-Order Reduction
• From Philosophical to Industrial Logics
• Survey on Directed Model Checking
• Hierarchical Adaptive State Space Caching Based on Level Sampling
• Automata-Based Termination Proofs
• Checking timed Büchi automata emptiness using LU-abstractions
• Memory efficient algorithms for the verification of temporal properties
• Automated verification of parallel nested DFS
• Alternating automata: unifying truth and validity checking for temporal logics
• Model checking of biological systems
• On Locally Checkable Properties
• Flash memory efficient LTL model checking
• “On the fly” verification of behavioural equivalences and preorders
• Bounded-memory algorithms for verification on-the-fly
• Using partial orders for the efficient verification of deadlock freedom and safety properties
• AutoHyper: explicit-state model checking for HyperLTL
• Checking timed Büchi automata emptiness efficiently
• Theoretical foundations of handling large substitution sets in temporal integrity monitoring

This page was built for publication:

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