Compositional SCC Analysis for Language Emptiness |
| |
Authors: | Chao Wang Roderick Bloem Gary D Hachtel Kavita Ravi Fabio Somenzi |
| |
Affiliation: | (1) NEC Laboratories America, 4 Independence Way, Suite 200, Princeton, NJ 08540, USA;(2) Graz University of Technology, Austria;(3) University of Colorado, Boulder, USA;(4) Cadence Design Systems, USA |
| |
Abstract: | We propose a refinement approach to language emptiness, which is based on the enumeration and the successive refinements of
SCCs on over-approximations of the exact system. Our algorithm is compositional: It performs as much computation as possible
on the abstract systems, and prunes uninteresting part of the search space as early as possible. It decomposes the state space
disjunctively so that each state subset can be checked in isolation to decide language emptiness for the given system. We
prove that the strength of an SCC or a set of SCCs decreases monotonically with composition. This allows us to deploy the
proper model checking algorithms according to the strength of the SCC at hand. We also propose to use the approximate distance
of a fair cycle from the initial states to guide the search. Experimental studies on a set of LTL model checking problems
prove the effectiveness of our method.
This work was done when the first two authors were in University of Colorado at Boulder. Parts of this work appeared in preliminary
form in 38] and 39]. |
| |
Keywords: | language emptiness model checking abstraction refinement LTL BDD |
本文献已被 SpringerLink 等数据库收录! |
|