scientific article; zbMATH DE number 177248

zbMATH Open0786.68060MaRDI QIDQ4037099FDOQ4037099

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

Publication date: 18 May 1993

Title of this publication is not available (Why is that?)

Recommendations

• scientific article; zbMATH DE number 177519
• Automatic Verification of Sequential Circuits Using Temporal Logic
• scientific article; zbMATH DE number 177500
• scientific article; zbMATH DE number 1487477
• The complexity of probabilistic verification

zbMATH Keywords

verificationreachability analysistemporal propertiesautomata on infinite wordsemptiness problemfinite-state programsBüchi automatacomputer protocolsproduct automaton

Mathematics Subject Classification ID

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

Cited In (26)

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

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)