Automata theory and model checking

DOI10.1007/978-3-319-10575-8_4MaRDI QIDQ3176362zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

Recommendations

• Automata- and logic-based systems design
• scientific article; zbMATH DE number 5872401
• Finite-state automata on infinite inputs
• The automata-theoretic approach to verification of reactive systems
• Automata-Theoretic Model Checking Revisited

Cites work

• scientific article; zbMATH DE number 1670767 (Why is no real title available?)
• scientific article; zbMATH DE number 1670781 (Why is no real title available?)
• scientific article; zbMATH DE number 1701356 (Why is no real title available?)
• scientific article; zbMATH DE number 5542185 (Why is no real title available?)
• scientific article; zbMATH DE number 3983141 (Why is no real title available?)
• scientific article; zbMATH DE number 734956 (Why is no real title available?)
• scientific article; zbMATH DE number 1142314 (Why is no real title available?)
• scientific article; zbMATH DE number 1973991 (Why is no real title available?)
• scientific article; zbMATH DE number 2080056 (Why is no real title available?)
• scientific article; zbMATH DE number 1487477 (Why is no real title available?)
• scientific article; zbMATH DE number 1500523 (Why is no real title available?)
• scientific article; zbMATH DE number 1500643 (Why is no real title available?)
• scientific article; zbMATH DE number 1796123 (Why is no real title available?)
• scientific article; zbMATH DE number 3999901 (Why is no real title available?)
• scientific article; zbMATH DE number 1863182 (Why is no real title available?)
• scientific article; zbMATH DE number 1903366 (Why is no real title available?)
• scientific article; zbMATH DE number 3237829 (Why is no real title available?)
• scientific article; zbMATH DE number 3254905 (Why is no real title available?)
• A partial approach to model checking
• A space-efficient on-the-fly algorithm for real-time model checking
• A stubborn attack on state explosion
• Alternating finite automata on -words
• Alternating-time temporal logic
• Alternation
• Alternation removal in Büchi automata
• An automata-theoretic approach to branching-time model checking
• Automata-theoretic techniques for modal logics of programs
• Beyond hyper-minimisation -- minimising DBAs and DPAs is NP-complete
• BÜCHI COMPLEMENTATION MADE TIGHTER
• Büchi complementation made tight
• Complementation, Disambiguation, and Determinization of Büchi Automata Unified
• Complementing deterministic Büchi automata in polynomial time
• Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Decision problems forω-automata
• Depth-First Search and Linear Graph Algorithms
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• Improved Ramsey-based Büchi complementation
• Infinite games on finitely coloured graphs with applications to automata on infinite trees
• Interleaving set temporal logic
• Lower Bounds for Complementation of ω-Automata Via the Full Automata Technique
• Modalities for model checking: Branching time logic strikes back
• Nondeterministic Space is Closed under Complementation
• NuSMV: A new symbolic model checker
• On syntactic congruences for \(\omega\)-languages
• On the Merits of Temporal Testers
• On the frequency of the transfer paradox
• Parityizing Rabin and Streett
• Progress measures and stack assertions for fair termination
• Reasoning about infinite computations
• Sanity Checks in Formal Verification
• Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
• TYPENESS FOR ω-REGULAR AUTOMATA
• Testing and generating infinite sequences by a finite automaton
• The complementation problem for Büchi automata with applications to temporal logic
• The complexity of propositional linear temporal logics
• Theories of automata on \(\omega\)-tapes: a simplified approach
• Tighter Bounds for the Determinisation of Büchi Automata
• Unifying Büchi complementation constructions
• Weak alternating automata are not that weak

Cited in

(50)

• Finite-state automata on infinite inputs
• scientific article; zbMATH DE number 1507201 (Why is no real title available?)
• On Repetition Languages
• 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
• scientific article; zbMATH DE number 2208070 (Why is no real title available?)
• Jumping automata over Infinite words
• Linear-Time Model Checking: Automata Theory in Practice
• Monoids as storage mechanisms
• 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
• Automata over infinite alphabets
• A hierarchy of nondeterminism
• scientific article; zbMATH DE number 1203022 (Why is no real title available?)
• scientific article; zbMATH DE number 1786477 (Why is no real title available?)
• Stackelberg-Pareto synthesis
• First order Büchi automata and their application to verification of LTL specifications
• Usage Automata
• Automata theory. An algorithmic approach
• A Finite Union of DFAs in Symbolic Model Checking of Infinite Systems
• The design of checkable automata. II
• Jumping automata over infinite words
• Quantitative vs. weighted automata
• Finite-memory automata
• Representation of semiautomata by canonical words and equivalences. II: Specification of software modules
• scientific article; zbMATH DE number 4049055 (Why is no real title available?)
• Tightening the Exchange Rates Between Automata
• scientific article; zbMATH DE number 176242 (Why is no real title available?)
• scientific article; zbMATH DE number 1507202 (Why is no real title available?)
• An automata-theoretic approach to linear temporal logic
• scientific article; zbMATH DE number 1479635 (Why is no real title available?)
• scientific article; zbMATH DE number 5245252 (Why is no real title available?)
• Multi-Valued Reasoning about Reactive Systems
• Specification and verification of decentralized daisy chain arbiters with \(\omega\)-extended regular expressions
• Automata on infinite words and their applications in formal verification
• Automata theory: Its past and future

Describes a project that uses

Uses Software

• LTL2BA
• NuSMV
• SPIN

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)