Automated Assume-Guarantee Reasoning for Omega-Regular Systems and SpecificationsWe develop a learning-based automated Assume-Guarantee (AG) reasoning framework for verifying omega-regular properties of concurrent systems. We study the applicability of non-circular (AGNC) 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 infinite regular systems, that combine finite and infinite behaviors. We show that for infinity-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 infinite regular, and omega-regular, systems using both AG-NC and AG-C as proof rules
Document ID
20100018534
Acquisition Source
Langley Research Center
Document Type
Conference Paper
Authors
Chaki, Sagar (Carnegie-Mellon Univ. Pittsburgh, PA, United States)
Gurfinkel, Arie (Carnegie-Mellon Univ. Pittsburgh, PA, United States)
Date Acquired
August 24, 2013
Publication Date
April 1, 2010
Publication Information
Publication: Proceedings of the Second NASA Formal Methods Symposium