Automata Theory and Model Checking
From MaRDI portal
Publication:3176362
DOI10.1007/978-3-319-10575-8_4zbMath1392.68255OpenAlexW2804031838MaRDI QIDQ3176362
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
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Temporal Logic and Fair Discrete Systems, Model Checking Procedural Programs, The mu-calculus and Model Checking, Multi-Valued Reasoning about Reactive Systems, Jumping automata over Infinite words, Quantitative vs. weighted automata, Automated temporal equilibrium analysis: verification and synthesis of multi-player games, Certifying inexpressibility, Calculational design of a regular model checker by abstract interpretation, On Repetition Languages
Uses Software
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
- On the frequency of the transfer paradox
- Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
- A stubborn attack on state explosion
- Alternating finite automata on \(\omega\)-words
- The complementation problem for Büchi automata with applications to temporal logic
- Automata-theoretic techniques for modal logics of programs
- Complementing deterministic Büchi automata in polynomial time
- Theories of automata on \(\omega\)-tapes: a simplified approach
- Infinite games on finitely coloured graphs with applications to automata on infinite trees
- A partial approach to model checking
- Reasoning about infinite computations
- On syntactic congruences for \(\omega\)-languages
- Modalities for model checking: Branching time logic strikes back
- NuSMV: A new symbolic model checker
- Interleaving set temporal logic
- Improved Ramsey-Based Büchi Complementation
- Beyond Hyper-Minimisation--Minimising DBAs and DPAs is NP-Complete
- Unifying Büchi Complementation Constructions.
- Alternating-time temporal logic
- On the Merits of Temporal Testers
- Complementation, Disambiguation, and Determinization of Büchi Automata Unified
- Weak alternating automata are not that weak
- Constructing Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata
- Alternation Removal in Büchi Automata
- Lower Bounds for Complementation of ω-Automata Via the Full Automata Technique
- Tighter Bounds for the Determinisation of Büchi Automata
- The complexity of propositional linear temporal logics
- Nondeterministic Space is Closed under Complementation
- Alternation
- Progress measures and stack assertions for fair termination
- An automata-theoretic approach to branching-time model checking
- Büchi Complementation Made Tight
- From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
- BÜCHI COMPLEMENTATION MADE TIGHTER
- TYPENESS FOR ω-REGULAR AUTOMATA
- Decision problems forω-automata
- Testing and generating infinite sequences by a finite automaton
- Decidability of Second-Order Theories and Automata on Infinite Trees
- Depth-First Search and Linear Graph Algorithms
- Sanity Checks in Formal Verification
- A space-efficient on-the-fly algorithm for real-time model checking
