LIF, Université de Provence (Marseille, FRANCE)
Symbolic state space generation and analysis of timed automata
ELSE (symbolic state space generator for timed automata)
CADP (Construction and Analysis of Distributed Processes)
ELSE is a prototype state space generator for timed automata, which
compiles timed automata to C programs that link with CADP. ELSE uses
clock constraints to abstract the state space to a finite set of
equivalence classes, and partial order reduction techniques to avoid
the generation of irrelevant interleavings.
ELSE differentiates from classical tools such as Kronos and Uppaal in using so-called event zones to represent time constraints. ELSE includes a library for event zones, called elsezone.
The ELSE prototype has been experimented on academic examples, which
tend to show that the event zone approach is more efficient than
classical approaches. On some example series, exponential savings
have been observed.
Sarah Zennou, Manuel Yguel, and Peter Niebert.
"ELSE: A New Symbolic State Generator for Timed Automata". In
Proceedings of the 1st International Workshop on Formal Modeling
and Analysis of Timed Systems FORMATS'2003 (Marseille, France),
Available on-line at: http://www.cmi.univ-mrs.fr/~niebert/docs/else.pdf
or from our FTP site in PDF or PostScript
LIF, Université de Provence
39, rue Jolliot-Curie
F-13453 Marseille Cedex 13
Tel: +33 (0)4 91 11 36 24
Fax: +33 (0)4 91 11 36 02
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|