Access Restriction

Author Thomas, D. ♦ Chakraborty, S. ♦ Pandya, P.
Source IIT Bombay
Content type Text
File Format HTM / HTML
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Technology ♦ Medicine & health ♦ Diseases
Abstract 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.
ISBN 3540330569
ISSN 03029743
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2006-04-02
Volume Number 3920