Abstract
We develop a learning-based automated assume-guarantee (AG) reasoning framework for verifying ω-regular properties of concurrent systems. We study the applicability of non-circular (AG-NC) and circular (AG-C) AG proof rules in the context of systems with infinite behaviors. In particular, we show that AG-NC is incomplete when assumptions are restricted to strictly infinite behaviors, while AG-C remains complete. We present a general formalization, called LAG, of the learning based automated AG paradigm. We show how existing approaches for automated AG reasoning are special instances of LAG. We develop two learning algorithms for a class of systems, called ∞-regular systems, that combine finite and infinite behaviors. We show that for ∞-regular systems, both AG-NC and AG-C are sound and complete. Finally, we show how to instantiate LAG to do automated AG reasoning for ∞-regular, and ω-regular, systems using both AG-NC and AG-C as proof rules.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Alur R, Madhusudan P, Nam W (2005) Symbolic compositional verification by learning assumptions. In: Etessami K, Rajamani SK (eds) Proceedings of the 17th international conference on computer aided verification (CAV ’05), New York, July 6–10, 2005. Lecture notes in computer science, vol 3576. Springer, Edinburgh, pp 548–562
Angluin D: Learning regular sets from queries and counterexamples. Inform Comput 75(2), 87–106 (1987)
Barringer H, Giannakopoulou D, Păsăreanu CS (2003) Proof rules for automated compositional verification through learning. In: Proceedings of the second workshop on specification and verification of component based systems (SAVCBS ’03), Helsinki, September 1–2, 2003. Iowa State University, Ames, pp 14–21
Calbrix H, Nivat M, Podelski A (1993) Ultimately periodic words of rational ω-languages. In: Brookes SD, Main MG, Melton A, Mislove MW, Schmidt DA (eds) Proceedings of the 9th international conference on mathematical foundations of programming semantics (MFPS ’93). Lecture notes in computer science, vol 802. Springer, New Orleans, pp 554–566
Chaki S, Sinha N (2006) Assume-guarantee reasoning for deadlock. In: Proceedings of the 6th international conference on formal methods in computer-aided design (FMCAD ’06), San Jose, November 12–16, 2006. IEEE Computer Society, Washington, DC, pp 134–144
Chaki S, Strichman O (2007) Optimized L* for assume-guarantee reasoning. In: Grumberg O, Huth M (eds) Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems (TACAS ’07), Braga, March 24–April 1, 2007. Lecture notes in computer science, vol 4424. Springer, New York, pp 276–291
Chaki S, Clarke EM, Sinha N, Thati P (2005) Automated assume-guarantee reasoning for simulation conformance. In: Etessami K, Rajamani SK (eds) Proceedings of the 17th international conference on computer aided verification (CAV ’05). Lecture notes in computer science, vol 3576. Springer, Edinburgh, pp 534–547
Clarke E, Long D, McMillan K (1989) Compositional model checking. In: Proceedings of the 4th annual IEEE symposium on logic in computer science (LICS ’89), Pacific Grove, June 5–8, 1989. IEEE Computer Society, Washington, DC, pp 353–362
Cobleigh JM, Giannakopoulou D, Păsăreanu CS (2003) Learning assumptions for compositional verification. In: Garavel H, Hatcliff J (eds) Proceedings of the 9th international conference on tools and algorithms for the construction and analysis of systems (TACAS ’03), Warsaw, April 7–11, 2003. Lecture notes in computer science, vol 2619. Springer, New York, pp 331–346
Farzan A, Chen Y, Clarke E, Tsan Y, Wang B (2008) Extending automated compositional verification to the full class of omega-regular languages. In: Ramakrishnan CR, Rehof J (eds) Proceedings of the 14th international conference on tools and algorithms for the construction and analysis of systems (TACAS ’08), Budapest. Lecture notes in computer science, vol 4963. Springer, Berlin, pp 2–17
Gheorghiu M, Giannakopoulou D, Păsăreanu CS (2007) Refining interface alphabets for compositional verification. In: Grumberg O, Huth M (eds) Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems (TACAS ’07), Braga, March 24–April 1, 2007. Lecture notes in computer science, vol 4424. Springer, New York, pp 292–307
Gold EM: Language identification in the limit. Inform Control 10(5), 447–474 (1967)
Grumberg O, Long DE: Model checking and modular verification. ACM Trans Program Lang Syst (TOPLAS) 16(3), 843–871 (1994)
Henzinger TA, Qadeer S, Rajamani SK (2000) Decomposing refinement proofs using assume-guarantee reasoning. In: Proceedings of the 2000 international conference on computer-aided design (ICCAD ’00), San Jose. IEEE Computer Society, Washington, DC, pp 245–252
Hoare CAR: Communicating sequential processes. Prentice Hall, London (1985)
Jones CB (1983) Specification and design of (Parallel) programs. In: Mason REA (ed) Proceedings of the 9th IFIP World Congress, Paris, France, vol 83. Information processing, pp 321–332
Maler O, Pnueli A: On the learnability of infinitary regular sets. Inform Comput 118(2), 316–326 (1995)
Misra J, Chandy KM: Proofs of networks of processes. IEEE Trans Softw Eng (TSE) 7(4), 417–426 (1981)
Pnueli A: In transition from global to modular temporal reasoning about programs. Logics Models Concurrent Syst 13, 123–144 (1985)
Rivest RL, Schapire RE: Inference of finite automata using homing sequences. Inform Comput 103(2), 299–347 (1993)
Sinha N, Clarke E (2007) SAT-based compositional verification using lazy learning. In: Damm W, Hermanns H (eds) Proceedings of the 19th international conference on computer aided verification (CAV ’07), Berlin, July 3–7, 2007. Lecture notes in computer science, vol 4590. Springer, New York, pp 39–54
Tsay YK, Wang BY (2008) Automated compositional reasoning of intuitionistically closed regular properties. In: Ibarra OH, Ravikumar B (eds) Proceedings of the 13th international conference on implementation and applications of automata (CIAA ’08), San Francisco, July 21–24, 2008. Lecture notes in computer science, vol 5148. Springer, New York, pp 36–45
Wang BY (2007) Automatic derivation of compositional rules in automated compositional reasoning. In: Caires L, Vasconcelos VT (eds) Proceedings of the 18th international conference on concurrency theory (CONCUR ’07), Lisbon, September 3–8, 2007. Lecture notes in computer science, vol 4703. Springer, New York, pp 303–316
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Chaki, S., Gurfinkel, A. Automated assume-guarantee reasoning for omega-regular systems and specifications. Innovations Syst Softw Eng 7, 131–139 (2011). https://doi.org/10.1007/s11334-011-0148-1
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11334-011-0148-1