An Automata-Theoretic Approach to Infinite-State Systems
From MaRDI portal
Publication:3587257
DOI10.1007/978-3-642-13754-9_11zbMath1288.68158OpenAlexW1997450827MaRDI QIDQ3587257
Moshe Y. Vardi, Orna Kupferman, Nir Piterman
Publication date: 7 September 2010
Published in: Time for Verification (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-13754-9_11
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (6)
Solving Infinite Games in the Baire Space ⋮ Efficient CTL model-checking for pushdown systems ⋮ Branching Temporal Logic of Calls and Returns for Pushdown Systems ⋮ Unnamed Item ⋮ Analyzing pushdown systems with stack manipulation ⋮ Efficient CTL Model-Checking for Pushdown Systems
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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Results on the propositional \(\mu\)-calculus
- The theory of ends, pushdown automata, and second-order logic
- Automata-theoretic techniques for modal logics of programs
- Alternating automata on infinite trees
- Propositional dynamic logic of regular programs
- CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
- A partial approach to model checking
- Reasoning about infinite computations
- From bidirectionality to alternation.
- Monadic second-order logic on tree-like structures
- On infinite transition graphs having a decidable monadic theory
- Practical CTL* model checking: Should SPIN be extended?
- On Bounded Specifications
- On the analysis of interacting pushdown systems
- Alternating-time temporal logic
- Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains
- Automata for the modal μ-calculus and related results
- Visibly pushdown languages
- Tree-walking automata do not recognize all regular languages
- Adding Nesting Structure to Words
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Alternation
- FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
- FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- An automata-theoretic approach to branching-time model checking
- Pushdown Module Checking
- Mathematical Foundations of Computer Science 2003
- Regularity Problems for Visibly Pushdown Languages
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Automata, Languages and Programming
- Decidability of Second-Order Theories and Automata on Infinite Trees
- Computer Aided Verification
- Automata, Languages and Programming
- Languages of Nested Trees
- Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Foundations of Software Science and Computation Structures
- Computer Aided Verification
- On model checking for the \(\mu\)-calculus and its fragments
This page was built for publication: An Automata-Theoretic Approach to Infinite-State Systems
