|
| Final Report of the COST-247 Action |
EFFICIENT SYMBOLIC TRAVERSAL ALGORITHMS USING PARTITIONED TRANSITION RELATIONS
Zmago Brezocnik, Ales Casar, Tatjana Kapus
| Faculty of Electrical Engineering and Computer Science |
| University of Maribor |
| Smetanova ul. 17, SI-2000 Maribor, Slovenia |
| Email: brezocnik@uni-mb.si , casar@uni-mb.si , kapus@uni-mb.si |
| Tel: +386 62 221-112 |
| Fax: +386 62 225-013 |
This paper presents an efficient tool for symbolic state space traversal of finite state machines. Both algorithms for searching reachable states and for model checking in CTL owe their efficiency primarily to an improved state variables substitution algorithm and to the use of partitioned transition relations. Partitioning of the relations is fully automatic. We give experimental results on the performance of the algorithms applied to a set of synchronous benchmark circuits.
This presentation has been given during the COST-247 International Workshop on Applied Formal Methods in System Design (Maribor, Slovenia, June 17--19, 1996).
COST-247 Working Group(s): 2
This Page was prepared by Mark Jorgensen.
Back to the VASY Home page