Title
Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis
Abstract
Symbolic techniques usually use characteristic functions for representing sets of states. Boolean functional vectors provide an alternate set representation which is suitable for symbolic simulation. Their use in symbolic reachability analysis and model checking is limited, however, by the lack of algorithms for performing set operations. We present algorithms for set union, intersection and quantification that work with a canonical Boolean functional vector representation and show how this enables efficient symbolic simulation based reachability analysis. Our experimental results for reachability analysis indicate that the Boolean functional vector representation is often more compact than the corresponding characteristic function, thus giving significant performance improvements on some benchmarks.
Year
DOI
Venue
2003
10.1109/DATE.2003.1253707
DATE
Keywords
Field
DocType
symbolic simulation,symbolic technique,efficient symbolic simulation,canonical boolean functional vector,boolean functional vectors,reachability analysis,alternate set representation,symbolic reachability analysis,boolean functional vector,boolean functional vector representation,set union,set manipulation,network analysis,characteristic function,encoding,data structures,boolean function,model checking,set intersection,computer science,set theory,computational modeling,boolean functions
Boolean function,Symbolic simulation,Model checking,Computer science,Algorithm,Theoretical computer science,Reachability,Symbolic data analysis,And-inverter graph,Boolean expression,Symbolic trajectory evaluation
Conference
ISBN
Citations 
PageRank 
0-7695-1870-2
3
0.40
References 
Authors
11
2
Name
Order
Citations
PageRank
Amit Goel127921.29
Randal E. Bryant292041194.64