Record Details

Efficient guided symbolic reachability using reachability expressions

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title Efficient guided symbolic reachability using reachability expressions
 
Creator THOMAS, D
CHAKRABORTY, S
PANDYA, P
 
Description Asynchronous systems consist of a set of transitions which are non-deterministically chosen and executed. We present a theory of guiding symbolic reachability in such systems by scheduling clusters of transitions. A theory of reachability expressions which specify the schedules is presented. This theory allows proving equivalence of different schedules which may have radically different performance in BDD-based search. We present experimental evidence to show that optimized reachability expressions give rise to significant performance advantages. The profiling is carried out in the NuSMV framework using examples from discrete timed automata and circuits with delays. A variant tool called NuSMV-DP has been developed for interpreting reachability expressions to carry out the experiments.
 
Publisher SPRINGER-VERLAG BERLIN
 
Date 2011-10-23T19:39:40Z
2011-12-15T09:10:45Z
2011-10-23T19:39:40Z
2011-12-15T09:10:45Z
2006
 
Type Article; Proceedings Paper
 
Identifier TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS,3920,120-134
3-540-33056-9
0302-9743
http://dspace.library.iitb.ac.in/xmlui/handle/10054/15218
http://hdl.handle.net/100/1637
 
Source 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,Vienna, AUSTRIA,MAR 25-APR 02, 2006
 
Language English