next up previous

Final Report of the COST-247 Action


Verification using Leap Automata

H. Yenigun(1), K. Inan (2)

(1) Bell Laboratories
Lucent Technologies
700 Mountain Avenue, Murray Hill
NJ 07974, USA
Tel: +1-908-582 6165
Fax: +1-908-582 5857
E-Mail: husnu@research.bell-labs.com
~
(2) Electrical & Electronics Engineering Department
Middle East Technical University
Balgat-Ankara
Turkey
Tel: +90-312-210 1298
Tel: +90-312-210 1411
E-mail: inan@srdc.metu.edu.tr

Abstract:

Transition leaping mechanism is presented in the literature as an additional and powerful complexity reducing mechanism used together with partial order methods for finite state verification. In this paper we improve on the original leaping approach by setting it in a more general context thereby enhancing the potential for greater complexity reduction. In particular by allowing ample sets that are not necessarily disjoint we present leaping results both for safety and liveness verification where the latter is presented only under a fairness assumption.

This presentation has been given during the COST-247 2nd International Workshop on Applied Formal Methods in System Design (Zagreb, Croatia, June 18-19, 1997).

COST-247 Working Group(s):

Web Links :


This Page was prepared by Mark Jorgensen.


Back to the VASY Home page