Abstract
We propose and evaluate new algorithms to support the automata-based approach to model-checking: algorithms to solve the universality and language inclusion problems for nondeterministic Büchi automata. To obtain those new algorithms, we establish the existence of 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 our new algorithm to check for universality of Büchi automata experimentally 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. This work is an extension to the infinite words case of new algorithms for the finite words case that we and co-authors have presented in a recent paper [DDHR06].
Supported by the FRFC project “Centre Fédéré en Vérification” funded by the Belgian National Science Foundation (FNRS) under grant nr 2.4530.02.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Büchi, J.R., Landweber, L.H.: Definability in the monadic second-order theory of successor. J. Symb. Log. 34(2), 166–170 (1969)
De Wulf, M., et al.: Antichains: A new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17–30. Springer, Heidelberg (2006)
Doyen, L., Raskin, J.-F.: Improved Algorithms for the Automata-Based Approach to Model-Checking (extended version). Tech. Rep. 76, U.L.B. – Federated Center in Verification (2006), http://www.ulb.ac.be/di/ssd/cfv/publications.html
Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for büchi automata. SIAM J. Comput. 34(5), 1159–1175 (2005)
Gurumurthy, S., et al.: On complementing nondeterministic büchi automata. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 96–110. Springer, Heidelberg (2003)
Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)
Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. In: Proceedings of ISTCS’97, pp. 147–158. IEEE Computer Society Press, Los Alamitos (1997)
Miyano, S., Hayashi, T.: Alternating finite automata on omega-words. In: CAAP, pp. 195–210 (1984)
Michel, M.: Complementation is more difficult with automata on infinite words. In: CNET, Paris (1988)
Ruys, T.C., Holzmann, G.J.: Advanced spin tutorial. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 304–305. Springer, Heidelberg (2004)
Safra, S.: On the complexity of ω-automata. In: Proc. of FOCS: Foundations of Computer Science, pp. 319–327. IEEE Computer Society Press, Los Alamitos (1988)
Sistla, A.P., Vardi, M.Y., Wolper, P.: The Complementation Problem for Büchi Automata with Applications to Temporal Logic. Theor. Comput. Sci. 49, 217–237 (1987)
Tabakov, D.: Experimental evaluation of explicit and symbolic approaches to complementation of non-deterministic buechi automata. Talk at “Games and Verification” workshop, Newton Institute for Math. Sciences (July 2006)
Tabakov, D., Vardi, M.Y.: Experimental evaluation of classical automata constructions. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 396–411. Springer, Heidelberg (2005)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (prelim. report). In: LICS, pp. 332–344. IEEE Computer Society Press, Los Alamitos (1986)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Doyen, L., Raskin, JF. (2007). Improved Algorithms for the Automata-Based Approach to Model-Checking. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_34
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)