Automata theory and model checking
From MaRDI portal
Publication:3176362
DOI10.1007/978-3-319-10575-8_4zbMATH Open1392.68255OpenAlexW2804031838MaRDI QIDQ3176362FDOQ3176362
Authors: Orna Kupferman 
Publication date: 20 July 2018
Published in: Handbook of Model Checking (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_4
Recommendations
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- NuSMV: A new symbolic model checker
- Alternating-time temporal logic
- Title not available (Why is that?)
- Depth-First Search and Linear Graph Algorithms
- The complexity of propositional linear temporal logics
- Title not available (Why is that?)
- Decidability of Second-Order Theories and Automata on Infinite Trees
- Sanity Checks in Formal Verification
- Nondeterministic Space is Closed under Complementation
- Alternation
- A stubborn attack on state explosion
- Reasoning about infinite computations
- An automata-theoretic approach to branching-time model checking
- Alternating finite automata on \(\omega\)-words
- On syntactic congruences for \(\omega\)-languages
- Parityizing Rabin and Streett
- Alternation removal in Büchi automata
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Testing and generating infinite sequences by a finite automaton
- Title not available (Why is that?)
- Infinite games on finitely coloured graphs with applications to automata on infinite trees
- Tighter Bounds for the Determinisation of Büchi Automata
- Title not available (Why is that?)
- From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
- Automata-theoretic techniques for modal logics of programs
- On the frequency of the transfer paradox
- The complementation problem for Büchi automata with applications to temporal logic
- Modalities for model checking: Branching time logic strikes back
- Title not available (Why is that?)
- Complementing deterministic Büchi automata in polynomial time
- Weak alternating automata are not that weak
- Title not available (Why is that?)
- Title not available (Why is that?)
- Büchi complementation made tight
- Theories of automata on \(\omega\)-tapes: a simplified approach
- Title not available (Why is that?)
- Decision problems forω-automata
- Title not available (Why is that?)
- Complementation, Disambiguation, and Determinization of Büchi Automata Unified
- Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
- On the Merits of Temporal Testers
- A partial approach to model checking
- Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata
- Title not available (Why is that?)
- Title not available (Why is that?)
- Interleaving set temporal logic
- Title not available (Why is that?)
- A space-efficient on-the-fly algorithm for real-time model checking
- Title not available (Why is that?)
- Title not available (Why is that?)
- BÜCHI COMPLEMENTATION MADE TIGHTER
- Title not available (Why is that?)
- TYPENESS FOR ω-REGULAR AUTOMATA
- Progress measures and stack assertions for fair termination
- Beyond hyper-minimisation -- minimising DBAs and DPAs is NP-complete
- Improved Ramsey-based Büchi complementation
- Lower Bounds for Complementation of ω-Automata Via the Full Automata Technique
- Unifying Büchi complementation constructions
Cited In (49)
- On Repetition Languages
- Title not available (Why is that?)
- Automata and finite model theory
- Certifying inexpressibility
- From Muller to parity and Rabin qutomata: optimal transformations preserving (history) determinism
- Implementation and Application of Automata
- Model checking procedural programs
- A process-theoretic look at automata
- Title not available (Why is that?)
- Jumping automata over Infinite words
- Monoids as storage mechanisms
- Linear-Time Model Checking: Automata Theory in Practice
- The automata-theoretic approach to verification of reactive systems
- \(X\)-automata on \(\omega\)-words
- Temporal logic and fair discrete systems
- Automated temporal equilibrium analysis: verification and synthesis of multi-player games
- A formal theory of simulations between infinite automata
- The mu-calculus and Model Checking
- Co-determinism and unambiguity of automata accepting finite or infinite words
- Calculational design of a regular model checker by abstract interpretation
- Verification, Model Checking, and Abstract Interpretation
- Automata- and logic-based systems design
- Automata-Theoretic Model Checking Revisited
- Automata over infinite alphabets
- ω-Automata
- Title not available (Why is that?)
- Title not available (Why is that?)
- First order Büchi automata and their application to verification of LTL specifications
- Stackelberg-Pareto synthesis
- Automata theory. An algorithmic approach
- Usage Automata
- A Finite Union of DFAs in Symbolic Model Checking of Infinite Systems
- Jumping automata over infinite words
- The design of checkable automata. II
- Quantitative vs. weighted automata
- Title not available (Why is that?)
- Representation of semiautomata by canonical words and equivalences. II: Specification of software modules
- Tightening the Exchange Rates Between Automata
- Title not available (Why is that?)
- Finite-memory automata
- An automata-theoretic approach to linear temporal logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Multi-Valued Reasoning about Reactive Systems
- Automata on infinite words and their applications in formal verification
- Specification and verification of decentralized daisy chain arbiters with \(\omega\)-extended regular expressions
- Automata theory: Its past and future
- Finite-state automata on infinite inputs
Uses Software
This page was built for publication: Automata theory and model checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3176362)
