Automata-Theoretic Model Checking Revisited

DOI10.1007/978-3-540-69738-1_10zbMath1132.68483OpenAlexW1698053229MaRDI QIDQ5452603

Moshe Y. Vardi

Publication date: 4 April 2008

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

Full work available at URL: https://doi.org/10.1007/978-3-540-69738-1_10

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (21)

Symmetry and partial order reduction techniques in model checking Rebeca ⋮ Linear temporal logic -- from infinite to finite horizon ⋮ Automata-driven partial order reduction and guided search for LTL model checking ⋮ Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition ⋮ LTL under reductions with weaker conditions than stutter invariance ⋮ Linear-Time Model Checking: Automata Theory in Practice ⋮ On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties ⋮ An explicit transition system construction approach to LTL satisfiability checking ⋮ Linear temporal logic symbolic model checking ⋮ The complexity of synchronizing Markov decision processes ⋮ State Coverage Metrics for Specification-Based Testing with Büchi Automata ⋮ Transformation from PLTL to automata via NFGs ⋮ From Philosophical to Industrial Logics ⋮ From Monadic Logic to PSL ⋮ Büchi Complementation and Size-Change Termination ⋮ State of Büchi Complementation ⋮ Mediating for reduction (on minimizing alternating Büchi automata) ⋮ SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking ⋮ On-the-fly Emptiness Check of Transition-Based Streett Automata ⋮ Unnamed Item ⋮ Automated formal analysis and verification: an overview

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The complementation problem for Büchi automata with applications to temporal logic
• Symbolic model checking: \(10^{20}\) states and beyond
• Theories of automata on \(\omega\)-tapes: a simplified approach
• Reasoning about infinite computations
• Temporal logic can be more expressive
• Weak alternating automata are not that weak
• Constructing Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata
• Cluster-Based LTL Model Checking of Large Systems
• Lower Bounds for Complementation of ω-Automata Via the Full Automata Technique
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• From linear time to branching time
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Concepts of Automata Construction from LTL
• Model Checking Software
• BÜCHI COMPLEMENTATION MADE TIGHTER
• Formal Methods in Computer-Aided Design
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Correct Hardware Design and Verification Methods
• A new heuristic for bad cycle detection using BDDs
• Model checking of safety properties

This page was built for publication: Automata-Theoretic Model Checking Revisited