Generic Emptiness Check for Fun and Profit
From MaRDI portal
Publication:3297604
DOI10.1007/978-3-030-31784-3_26zbMath1437.68092OpenAlexW2981424294MaRDI QIDQ3297604
Jan Strejček, Alexandre Duret-Lutz, František Blahoudek, David Müller, Joachim Klein, Christel Baier
Publication date: 20 July 2020
Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-030-31784-3_26
Analysis of algorithms (68W40) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Determinization and limit-determinization of Emerson-Lei automata ⋮ LTL to self-loop alternating automata with generic acceptance and back
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Rabinizer
- Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic
- Verification of multiprocess probabilistic protocols
- Modalities for model checking: Branching time logic strikes back
- Three SCC-Based Emptiness Checks for Generalized Büchi Automata
- Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition
- From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata
- Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata
- On-the-Fly Stuttering in the Construction of Deterministic ω-Automata
- Mechanizing the Powerset Construction for Restricted Classes of ω-Automata
- On-the-fly Emptiness Check of Transition-Based Streett Automata
- One Theorem to Rule Them All
- Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment
- Manipulating LTL Formulas Using Spot 1.0
- Rabinizer 2: Small Deterministic Automata for LTL ∖ GU
- Why These Automata Types?
- Tools and Algorithms for the Construction and Analysis of Systems
- Lazy probabilistic model checking without determinisation
- Model Checking Software
- Symbolic algorithms for graphs and Markov decision processes with fairness objectives
