Antichains for the Automata-Based Approach to Model-Checking
From MaRDI portal
Abstract: We propose and evaluate antichain algorithms to solve the universality and language inclusion problems for nondeterministic Buechi automata, and the emptiness problem for alternating Buechi automata. To obtain those algorithms, we establish the existence of simulation pre-orders that can be exploited to efficiently evaluate fixed points on the automata defined during the complementation step (that we keep implicit in our approach). We evaluate the performance of the algorithm to check the universality of Buechi automata using the random automaton model recently proposed by Tabakov and Vardi. We show that on the difficult instances of this probabilistic model, our algorithm outperforms the standard ones by several orders of magnitude.
Recommendations
- Antichains: A New Algorithm for Checking Universality of Finite Automata
- Improved Algorithms for the Automata-Based Approach to Model-Checking
- Antichain algorithms for finite automata
- When simulation meets antichains. (On checking language inclusion of nondeterministic finite (tree) automata)
- Efficient Büchi universality checking
Cited in
(20)- Looking at mean payoff through foggy windows
- Strategy construction for parity games with imperfect information
- A general language-based framework for specifying and verifying notions of opacity
- State of Büchi complementation
- Symbolic model checking in non-Boolean domains
- Antichain algorithms for finite automata
- When simulation meets antichains. (On checking language inclusion of nondeterministic finite (tree) automata)
- Efficient Büchi universality checking
- Antichain-Based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata
- On the power of unambiguity in Büchi complementation
- Safe and optimal scheduling for hard and soft tasks
- Coinductive algorithms for Büchi automata
- Random models for evaluating efficient Büchi universality checking
- Ramsey-based inclusion checking for visibly pushdown automata
- Antichains: A New Algorithm for Checking Universality of Finite Automata
- Improved Algorithms for the Automata-Based Approach to Model-Checking
- On the power of finite ambiguity in Büchi complementation
- Proving Non-inclusion of Büchi Automata Based on Monte Carlo Sampling
- FORQ-Based Language Inclusion Formal Testing
- Model-checking real-time systems: revisiting the alternating automaton route
This page was built for publication: Antichains for the Automata-Based Approach to Model-Checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3623017)
