Efficient guided symbolic reachability using reachability expressions
DSpace at IIT Bombay
View Archive InfoField | 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
|
|