Compositional SCC Analysis for Language Emptiness

Autor:	Fabio Somenzi, Gary D. Hachtel, Chao Wang, Kavita Ravi, Roderick Bloem
Rok vydání:	2006
Předmět:	Set (abstract data type) Model checking Hardware and Architecture Computer science Computation Enumeration State space Monotonic function Isolation (database systems) State (functional analysis) Algorithm Software Theoretical Computer Science
Zdroj:	Formal Methods in System Design. 28:5-36
ISSN:	1572-8102 0925-9856
DOI:	10.1007/s10703-006-4617-3
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::c4349f7b7caf2a08487a980b5bc9f51d https://doi.org/10.1007/s10703-006-4617-3 Zobrazit plný text záznamu Full text from SpringerLink