Abstract
Automata are a useful tool in infinite-state model checking, since they can represent infinite sets of integers and reals. However, analogous to the use of bdds to represent finite sets, the sizes of the automata are an obstacle in the automata-based set representation. In this paper, we generalize the notion of “don’t cares” for bdds to word languages as a means to reduce the automata sizes. We show that the minimal weak deterministic Büchi automaton (wdba) with respect to a given don’t care set, under certain restrictions, is uniquely determined and can be efficiently constructed. We apply don’t cares to improve the efficiency of a decision procedure for the first-order logic over the mixed linear arithmetic over the integers and the reals based on wdbas.
This work was supported by the German Research Foundation (DFG) and the Swiss National Science Foundation (SNF).
Due to space limitations, proofs are omitted. Details are in the technical report [10].
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
Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Fast acceleration of symbolic transition systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 118–121. Springer, Heidelberg (2003)
Bartzis, C., Bultan, T.: Widening arithmetic automata. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 321–333. Springer, Heidelberg (2004)
Boigelot, B., Bronne, L., Rassart, S.: An improved reachability analysis method for strongly linear hybrid systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 167–178. Springer, Heidelberg (1997)
Boigelot, B., Herbreteau, F., Jodogne, S.: Hybrid acceleration using real vector automata. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 193–205. Springer, Heidelberg (2003)
Boigelot, B., Jodogne, S., Wolper, P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM ToCL 6, 614–633 (2005)
Boigelot, B., Latour, L.: Counting the solutions of Presburger equations without enumerating them. TCS 313, 17–29 (2004)
Boigelot, B., Legay, A., Wolper, P.: Omega-regular model checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 561–575. Springer, Heidelberg (2004)
Büchi, J.: Weak second-order arithmetic and finite automata. Zeitschrift der mathematischen Logik und Grundlagen der Mathematik 6, 66–92 (1960)
On a decision method in restricted second order arithmetic. In: Logic, Methodology and Philosophy of Science. Stanford University Press, pp. 1–11 (1962)
Eisinger, J., Klaedtke, F.: Don’t care words with an application to the automata-based approach for real addition, Tech. Rep. 223, Institut für Informatik, Albert-Ludwigs-Universität Freiburg (2006)
Henzinger, T.: The theory of hybrid automata. In: LICS 1996, pp. 278–292 (1996)
Hong, Y., Beerel, P.A., Burch, J.R., McMillan, K.L.: Safe BDD minimization using don’t cares. In: DAC 1997, pp. 208–213. ACM Press, New York (1997)
Hopcroft, J.E.: An n logn algorithm for minimizing the states in a finite automaton. In: Theory of Machines and Computations, pp. 189–196 (1971)
Kupferman, O., Vardi, M.: Weak alternating automata are not that weak. ACM ToCL 2, 408–429 (2001)
LASH, The Liège Automata-based Symbolic Handler, http://www.montefiore.ulg.ac.be/~boigelot/research/lash/
Löding, C.: Efficient minimization of deterministic weak ω-automata. IPL 79, 105–109 (2001)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)
Staiger, L., Wagner, K.: Automatentheoretische und automatenfreie Charakterisierungen topologischer Klassen regulärer Folgenmengen. Elektronische Informationsverarbeitung und Kybernetik 10, 379–392 (1974)
Yavuz-Kahveci, T., Bartzis, C., Bultan, T.: Action language verifier, extended. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 413–417. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Eisinger, J., Klaedtke, F. (2006). Don’t Care Words with an Application to the Automata-Based Approach for Real Addition. In: Ball, T., Jones, R.B. (eds) Computer Aided Verification. CAV 2006. Lecture Notes in Computer Science, vol 4144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817963_10
Download citation
DOI: https://doi.org/10.1007/11817963_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37406-0
Online ISBN: 978-3-540-37411-4
eBook Packages: Computer ScienceComputer Science (R0)