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, DINA
CHAKRABORTY, SUPRATIK
PANDYA, PARITOSH
 
Subject automata theory
codes (symbols)
delay circuits
scheduling
technology transfer
 
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 NuSMVDP has been developed for interpreting reachability expressions to carry out the experiments.
 
Publisher Springer
 
Date 2009-11-26T05:03:41Z
2011-11-25T15:54:14Z
2011-12-26T13:08:19Z
2011-12-27T05:56:19Z
2009-11-26T05:03:41Z
2011-11-25T15:54:14Z
2011-12-26T13:08:19Z
2011-12-27T05:56:19Z
2008
 
Type Article
 
Identifier International Journal on Software Tools for Technology Transfer (STTT) 10(2), 113-129
1433-2787
10.1007/s10009-007-0057-7
http://hdl.handle.net/10054/1722
http://dspace.library.iitb.ac.in/xmlui/handle/10054/1722
 
Language en