Thumbnail
Access Restriction
Open

Author Goel, Amit ♦ Bryant, Randal E.
Source CiteSeerX
Content type Text
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Reachability Analysis ♦ Symbolic Technique ♦ Model Checking ♦ Boolean Functional Vector Representation ♦ Boolean Functional Vector ♦ Corresponding Characteristic Function ♦ Canonical Boolean Functional Vector Representation ♦ Efficient Symbolic Simulation ♦ Symbolic Reachability Analysis ♦ Experimental Result ♦ Characteristic Function ♦ Set Manipulation ♦ Present Algorithm ♦ Symbolic Simulation ♦ Significant Performance Improvement
Description 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.
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Publisher Date 2003-01-01
Publisher Institution IN PROCEEDINGS OF DESIGN AUTOMATION AND TEST IN EUROPE (DATE’03