Automata-Theoretic Model Checking Revisited
From MaRDI portal
Publication:5452603
DOI10.1007/978-3-540-69738-1_10zbMATH Open1132.68483OpenAlexW1698053229MaRDI QIDQ5452603FDOQ5452603
Authors: 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
Recommendations
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Graph-Based Algorithms for Boolean Function Manipulation
- Title not available (Why is that?)
- Symbolic model checking: \(10^{20}\) states and beyond
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Temporal logic can be more expressive
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Reasoning about infinite computations
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The complementation problem for Büchi automata with applications to temporal logic
- Model checking of safety properties
- Weak alternating automata are not that weak
- Title not available (Why is that?)
- Title not available (Why is that?)
- Tools and Algorithms for the Construction and Analysis of Systems
- Verification, Model Checking, and Abstract Interpretation
- Theories of automata on \(\omega\)-tapes: a simplified approach
- Title not available (Why is that?)
- Formal Methods in Computer-Aided Design
- Title not available (Why is that?)
- Model Checking Software
- Title not available (Why is that?)
- Title not available (Why is that?)
- Liveness checking as safety checking for infinite state spaces
- Title not available (Why is that?)
- Concepts of Automata Construction from LTL
- A new heuristic for bad cycle detection using BDDs
- From linear time to branching time
- Title not available (Why is that?)
- Computer Aided Verification
- Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata
- Title not available (Why is that?)
- On complementing nondeterministic Büchi automata
- Tools and Algorithms for the Construction and Analysis of Systems
- Nested emptiness search for generalized Büchi automata
- BÜCHI COMPLEMENTATION MADE TIGHTER
- Lower Bounds for Complementation of ω-Automata Via the Full Automata Technique
- Cluster-Based LTL Model Checking of Large Systems
Cited In (35)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The complexity of synchronizing Markov decision processes
- An explicit transition system construction approach to LTL satisfiability checking
- Symmetry and partial order reduction techniques in model checking Rebeca
- Automated Termination in Model Checking Modulo Theories
- Büchi Complementation and Size-Change Termination
- Finite Models vs Tree Automata in Safety Verification
- State of Büchi complementation
- An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking
- Model-Checking First-Order Logic: Automata and Locality
- On-the-fly emptiness check of transition-based Streett automata
- Automated formal analysis and verification: an overview
- On Model Checking for Visibly Pushdown Automata
- Linear-Time Model Checking: Automata Theory in Practice
- The automata-theoretic approach to verification of reactive systems
- Transformation from PLTL to automata via NFGs
- Automata-driven partial order reduction and guided search for LTL model checking
- Linear temporal logic -- from infinite to finite horizon
- State coverage metrics for specification-based testing with Büchi automata
- From Monadic Logic to PSL
- Linear temporal logic symbolic model checking
- Mediating for reduction (on minimizing alternating Büchi automata)
- Formal Approaches to Software Testing
- LTL under reductions with weaker conditions than stutter invariance
- From Philosophical to Industrial Logics
- Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition
- Automated Technology for Verification and Analysis
- On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties
- Title not available (Why is that?)
- The design of checkable automata. II
- SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
- Generalizations of checking stack automata: characterizations and hierarchies
- Model Checking Using Generalized Testing Automata
This page was built for publication: Automata-Theoretic Model Checking Revisited
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5452603)
