Paper Info
Title
Fine-Grain Conjunction Scheduling for Symbolic Reachability Analysis
Abstract
In symbolic model checking, image computation is the process of computing the successors of a set of states. Containing the cost of image computation depends critically on controlling the number of variables that appear in the functions being manipulated; this in turn depends on the order in which the basic operations of image computation--conjunctions and quantifications--are performed. In this paper we propose an approach to this ordering problem--the conjunction scheduling problem--that is especially suited to the case in which the transition relation is specified as the composition of many small relations. (This is the norm in hardware verification.) Our fine-grain approach leads to the formulation of conjunction scheduling in terms of minimum max-cut linear arrangement, an NP-complete problem for which efficient heuristics have been developed. The cut whose width is minimized is related to the number of variables active during image computation.We also propose a clustering technique that is geared toward the minimization of the max-cut, and pruning techniques for the transition relation that benefit especially from the fine-grain approach.
Year
DOI
Venue
2002
10.1007/3-540-46002-0_22
TACAS
Keywords
Field
DocType
basic operation,small relation,conjunction scheduling,fine-grain conjunction scheduling,conjunction scheduling problem,minimum max-cut linear arrangement,transition relation,clustering technique,image computation,np-complete problem,symbolic reachability analysis,fine-grain approach,scheduling problem,np complete problem
Discrete mathematics,Model checking,Scheduling (computing),Computer science,Symbolic computation,Algorithm,Reachability,Minification,Heuristics,Cluster analysis,Computation
Conference
Volume
ISSN
ISBN
2280
0302-9743
3-540-43419-4
Citations 
PageRank 
References 
15
0.72
16
Authors
3
Name
Order
Citations
PageRank
HoonSang Jin124415.15
Andreas Kuehlmann21217105.62
Fabio Somenzi33394302.47