Abstract
Recent studies have suggested the applicability of learning to automated compositional verification. However, current learning algorithms fall short when it comes to learning liveness properties. We extend the automaton synthesis paradigm for the infinitary languages by presenting an algorithm to learn an arbitrary regular set of infinite sequences (an ω-regular language) over an alphabet Σ. Our main result is an algorithm to learn a nondeterministic Büchi automaton that recognizes an unknown ω-regular language. This is done by learning a unique projection of it on Σ * using the framework suggested by Angluin for learning regular subsets of Σ *.
This research was sponsored by the iCAST project of the National Science Council, Taiwan, under the grant no. NSC96-3114-P-001-002-Y and the Semiconductor Research Corporation (SRC) under the grant no. 2006-TJ-1366.
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
Alur, R., Madhusudan, P., Nam, W.: Symbolic compositional verification by learning assumptions. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 548–562. Springer, Heidelberg (2005)
Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation 75(2), 87–106 (1987)
Arnold, A.: A syntactic congruence for rational omega-language. Theoretical Computer Science 39, 333–335 (1985)
Büchi, J.R.: On a decision method in restricted second-order arithmetic. In: Proceedings of the 1960 International Congress on Logic, Methodology and Philosophy of Science, pp. 1–11 (1962)
Calbrix, H., Nivat, M., Podelski, A.: Ultimately periodic words of rational ω-languages. In: Main, M.G., Melton, A.C., Mislove, M.W., Schmidt, D., Brookes, S.D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 554–566. Springer, Heidelberg (1994)
Calbrix, H., Nivat, M., Podelski, A.: Sur les mots ultimement périodiques des langages rationnels de mots infinis. Comptes Rendus de l’Académie des Sciences 318, 493–497 (1994)
Chaki, S., Clarke, E., Sinha, N., Thati, P.: Automated assume-guarantee reasoning for simulation conformance. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 534–547. Springer, Heidelberg (2005)
Cobleigh, J.M., Giannakopoulou, D., Păsăreanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)
Farzan, A., Chen, Y., Clarke, E., Tsay, Y., Wang, B.: Extending automated compositional verification to the full class of omega-regular languages. Technical Report CMU-CS-2008-100, Carnegie Mellon University, Department of Computer Science (2008)
Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translations. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)
Gupta, A., McMillan, K.L., Fu, Z.: Automated assumption generation for compositional verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 420–432. Springer, Heidelberg (2007)
Hopcroft, J.E.: A n logn algorithm for minimizing states in a finite automaton. Technical report, Stanford University (1971)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading (1979)
Maler, O., Pnueli, A.: On the learnability of infinitary regular sets. Information and Computation 118(2), 316–326 (1995)
Manna, Z., Pnueli, A.: A hierarchy of temporal properties. Technical Report STAN-CS-87-1186, Stanford University, Department of Computer Science (1987)
Michel, M.: Complementation is more difficult with automata on infinite words. In: CNET, Paris (1988)
Perrin, D., Pin, J.E.: Infinite Words: Automata, Semigroups, Logic and Games. Academic Press, London (2003)
Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. Information and Computation 103(2), 299–347 (1993)
Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)
Tsay, Y., Chen, Y., Tsai, M., Wu, K., Chan, W.: GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 466–471. Springer, Heidelberg (2007)
Van, D.L., Le Saëc, B., Litovsky, I.: Characterizations of rational omega-languages by means of right congruences. Theor. Comput. Sci. 143(1), 1–21 (1995)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Farzan, A., Chen, YF., Clarke, E.M., Tsay, YK., Wang, BY. (2008). Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages. In: Ramakrishnan, C.R., Rehof, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2008. Lecture Notes in Computer Science, vol 4963. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78800-3_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-78800-3_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78799-0
Online ISBN: 978-3-540-78800-3
eBook Packages: Computer ScienceComputer Science (R0)