Automata-Theoretic Model Checking Revisited
From MaRDI portal
Publication:5452603
Recommendations
Cites work
- scientific article; zbMATH DE number 1705164 (Why is no real title available?)
- scientific article; zbMATH DE number 1705167 (Why is no real title available?)
- scientific article; zbMATH DE number 438994 (Why is no real title available?)
- scientific article; zbMATH DE number 5542185 (Why is no real title available?)
- scientific article; zbMATH DE number 3714896 (Why is no real title available?)
- scientific article; zbMATH DE number 3757688 (Why is no real title available?)
- scientific article; zbMATH DE number 734956 (Why is no real title available?)
- scientific article; zbMATH DE number 1069483 (Why is no real title available?)
- scientific article; zbMATH DE number 1973991 (Why is no real title available?)
- scientific article; zbMATH DE number 1979545 (Why is no real title available?)
- scientific article; zbMATH DE number 2079387 (Why is no real title available?)
- scientific article; zbMATH DE number 2080056 (Why is no real title available?)
- scientific article; zbMATH DE number 1479635 (Why is no real title available?)
- scientific article; zbMATH DE number 1487477 (Why is no real title available?)
- scientific article; zbMATH DE number 1759609 (Why is no real title available?)
- scientific article; zbMATH DE number 1796123 (Why is no real title available?)
- scientific article; zbMATH DE number 219271 (Why is no real title available?)
- scientific article; zbMATH DE number 1903365 (Why is no real title available?)
- scientific article; zbMATH DE number 2090309 (Why is no real title available?)
- scientific article; zbMATH DE number 7354705 (Why is no real title available?)
- scientific article; zbMATH DE number 3237829 (Why is no real title available?)
- A new heuristic for bad cycle detection using BDDs
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- BÜCHI COMPLEMENTATION MADE TIGHTER
- Cluster-Based LTL Model Checking of Large Systems
- Computer Aided Verification
- Concepts of Automata Construction from LTL
- Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata
- Formal Methods in Computer-Aided Design
- From linear time to branching time
- Graph-Based Algorithms for Boolean Function Manipulation
- Liveness checking as safety checking for infinite state spaces
- Lower Bounds for Complementation of ω-Automata Via the Full Automata Technique
- Model Checking Software
- Model checking of safety properties
- Nested emptiness search for generalized Büchi automata
- On complementing nondeterministic Büchi automata
- Reasoning about infinite computations
- Symbolic model checking: \(10^{20}\) states and beyond
- Temporal logic can be more expressive
- The complementation problem for Büchi automata with applications to temporal logic
- Theories of automata on \(\omega\)-tapes: a simplified approach
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Verification, Model Checking, and Abstract Interpretation
- Weak alternating automata are not that weak
Cited in
(37)- On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties
- scientific article; zbMATH DE number 1701767 (Why is no real title available?)
- Linear temporal logic symbolic model checking
- On Model Checking for Visibly Pushdown Automata
- Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition
- scientific article; zbMATH DE number 2101008 (Why is no real title available?)
- An explicit transition system construction approach to LTL satisfiability checking
- Linear-Time Model Checking: Automata Theory in Practice
- The automata-theoretic approach to verification of reactive systems
- Model-Checking First-Order Logic: Automata and Locality
- Automated Termination in Model Checking Modulo Theories
- scientific article; zbMATH DE number 1507201 (Why is no real title available?)
- Automata-driven partial order reduction and guided search for LTL model checking
- State of Büchi complementation
- Transformation from PLTL to automata via NFGs
- Automated Technology for Verification and Analysis
- On-the-fly emptiness check of transition-based Streett automata
- Finite Models vs Tree Automata in Safety Verification
- SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
- Automated formal analysis and verification: an overview
- Linear temporal logic -- from infinite to finite horizon
- State coverage metrics for specification-based testing with Büchi automata
- Random models for evaluating efficient Büchi universality checking
- Symmetry and partial order reduction techniques in model checking Rebeca
- From Philosophical to Industrial Logics
- An \(O(n^2)\) time algorithm for alternating Büchi games
- An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking
- The design of checkable automata. II
- The complexity of synchronizing Markov decision processes
- Büchi Complementation and Size-Change Termination
- Formal Approaches to Software Testing
- Mediating for reduction (on minimizing alternating Büchi automata)
- Generalizations of checking stack automata: characterizations and hierarchies
- Automata theory and model checking
- LTL under reductions with weaker conditions than stutter invariance
- From Monadic Logic to PSL
- 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)
