Antichains: a new algorithm for checking universality of finite automata. We propose and evaluate a new algorithm for checking the universality of nondeterministic finite automata. In contrast to the standard algorithm, which uses the subset construction to explicitly determinize the automaton, we keep the determinization step implicit. Our algorithm computes the least fixed point of a monotone function on the lattice of antichains of state sets. We evaluate the performance of our algorithm experimentally using the random automaton model recently proposed by Tabakov and Vardi. We show that on the difficult instances of this probabilistic model, the antichain algorithm outperforms the standard one by several orders of magnitude. We also show how variations of the antichain method can be used for solving the language-inclusion problem for nondeterministic finite automata, and the emptiness problem for alternating finite automata.

References in zbMATH (referenced in 27 articles )

Showing results 1 to 20 of 27.
Sorted by year (citations)

1 2 next

  1. Clemente, Lorenzo; Mayr, Richard: Efficient reduction of nondeterministic automata with application to language inclusion testing (2019)
  2. Fiedor, Tomáš; Holík, Lukáš; Lengál, Ondřej; Vojnar, Tomáš: Nested antichains for WS1S (2019)
  3. Menghi, Claudio; Spoletini, Paola; Chechik, Marsha; Ghezzi, Carlo: A verification-driven framework for iterative design of controllers (2019)
  4. Majumdar, Rupak; Raskin, Jean-François: Symbolic model checking in non-Boolean domains (2018)
  5. Bohy, Aaron; Bruyère, Véronique; Raskin, Jean-François; Bertrand, Nathalie: Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes (2017)
  6. Černý, Pavol; Clarke, Edmund M.; Henzinger, Thomas A.; Radhakrishna, Arjun; Ryzhyk, Leonid; Samanta, Roopsha; Tarrach, Thorsten: From non-preemptive to preemptive scheduling using synchronization synthesis (2017)
  7. Fernau, Henning; Krebs, Andreas: Problems on finite automata and the exponential time hypothesis (2017)
  8. Fisher, Corey; Fogarty, Seth; Vardi, Moshe: Random models for evaluating efficient Büchi universality checking (2017)
  9. Hague, Matthew; Meyer, Roland; Muskalla, Sebastian: Domains for higher-order games (2017)
  10. Brunet, Paul; Pous, Damien: Algorithms for Kleene algebra with converse (2016)
  11. Peleg, Hila; Shoham, Sharon; Yahav, Eran; Yang, Hongseok: Symbolic automata for representing big code (2016)
  12. Friedmann, Oliver; Klaedtke, Felix; Lange, Martin: Ramsey-based inclusion checking for visibly pushdown automata (2015)
  13. Chatterjee, Krishnendu; Randour, Mickael; Raskin, Jean-François: Strategy synthesis for multi-dimensional quantitative objectives (2014)
  14. Jacobs, Bart; Silva, Alexandra: Automata learning: a categorical perspective (2014)
  15. Geeraerts, Gilles; Goossens, Joël; Lindström, Markus: Multiprocessor schedulability of arbitrary-deadline sporadic tasks: complexity and antichain algorithm (2013)
  16. Abdulla, Parosh Aziz; Chen, Yu-Fang; Clemente, Lorenzo; Holík, Lukáš; Hong, Chih-Duo; Mayr, Richard; Vojnar, Tomáš: Advanced Ramsey-based Büchi automata inclusion testing (2011)
  17. Filiot, Emmanuel; Jin, Naiyong; Raskin, Jean-François: Antichains and compositional algorithms for LTL synthesis (2011)
  18. Guerraoui, Rachid; Henzinger, Thomas A.; Singh, Vasu: Verification of STM on relaxed memory models (2011)
  19. Berwanger, Dietmar; Chatterjee, Krishnendu; De Wulf, Martin; Doyen, Laurent; Henzinger, Thomas A.: Strategy construction for parity games with imperfect information (2010)
  20. Ganty, Pierre; Maquet, Nicolas; Raskin, Jean-François: Fixed point guided abstraction refinement for alternating automata (2010)

1 2 next