Abstract
We address the issue of efficiently automating assume-guarantee reasoning for simulation conformance between finite state systems and specifications. We focus on a non-circular assume-guarantee proof rule, and show that there is a weakest assumption that can be represented canonically by a deterministic tree automata (DTA). We then present an algorithm L T that learns this DTA automatically in an incremental fashion, in time that is polynomial in the number of states in the equivalent minimal DTA. The algorithm assumes a teacher that can answer membership and candidate queries pertaining to the language of the unknown DTA. We show how the teacher can be implemented using a model checker. We have implemented this framework in the COMFORT toolkit and we report encouraging results (over an order of magnitude improvement in memory consumption) on non-trivial benchmarks.
Chapter PDF
Similar content being viewed by others
References
Alur, R., Cerný, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for java classes. In: POPL, pp. 98–109 (2005)
Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation 75(2), 87–106 (1987)
Barringer, H., Giannakopoulou, D., Pasareanu, C.S.: Proof rules for automated compositional verification. In: Proc. of the 2nd Workshop on SAVCBS (2003)
Bernard, M., de la Higuera, C.: Gift: Grammatical inference for terms. In: International Conference on Inductive Logic Programming (1999)
Carrasco, R.C., Oncina, J., Calera-Rubio, J.: Stochastic inference of regular tree languages. In: Honavar, V.G., Slutzki, G. (eds.) ICGI 1998. LNCS (LNAI), vol. 1433, pp. 187–198. Springer, Heidelberg (1998)
Chaki, S., Clarke, E., Groce, A., Ouaknine, J., Strichman, O., Yorav, K.: Efficient verification of sequential and concurrent C programs. FMSD 25(2–3) (2004)
Chaki, S., Ivers, J., Sharygina, N., Wallnau, K.: The comFoRT reasoning framework. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 164–169. Springer, Heidelberg (2005)
Clarke, E., Long, D., McMillan, K.: Compositional model checking. In: LICS (1989)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Proc. of CAV (2000)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and System (TOPLAS) 16(5), 1512–1542 (1994)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
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)
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications, ch.1 (2002), available at http://www.grappa.univ-lille3.fr/tata
Drewes, F., Hogberg, J.: Learning a regular tree language. In: Ésik, Z., Fülöp, Z. (eds.) DLT 2003. LNCS, vol. 2710, pp. 279–291. Springer, Heidelberg (2003)
Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. In: Proc. of ICSE (1999)
García, P., Oncina, J.: Inference of recognizable tree sets. Technical Report II/47/1993, Dept. de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia (1993)
Gold, E.M.: Language identification in the limit. Information and Control 10(5) (1967)
Gold, E.M.: Complexity of automaton identification from given data. Information and Control 37(3), 302–320 (1978)
Groce, A., Peled, D., Yannakakis, M.: Adaptive model checking. Tools and Algorithms for Construction and Analysis of Systems, 357–370 (2002)
Habermehl, P., Vojnar, T.: Regular model checking using inference of regular languages. In: Proc. of INFINITY 2004 (2004)
García, P., Oncina, J.: Identifying regular languages in polynomial time. Advances in Structural and Syntactic Pattern Recognition. World Scientific Publishing, Singapore (1992)
Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. In: FORTE/PSTV (1999)
Pnueli, A.: In transition from global to modular temporal reasoning about programs. Logics and models of concurrent systems, 123–144 (1985)
Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. Information and Computation 103(2), 299–347 (1993)
Sakakibara, Y.: Learning context-free grammars from structural data in polynomial time. Theoretical Computer Science (TCS) 76(2-3), 223–242 (1990)
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chaki, S., Clarke, E., Sinha, N., Thati, P. (2005). Automated Assume-Guarantee Reasoning for Simulation Conformance. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_51
Download citation
DOI: https://doi.org/10.1007/11513988_51
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)