Automated assume-guarantee reasoning for omega-regular systems
and specifications
Sagar
Chaki, Arie Gurfinkel,
Innovations in Systems and Software Engineering (ISSE), volume 7,
number 2, page 131-139, June 2011.
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.
Online
© Springer