ELSE: A New Symbolic State Generator for Timed Automata

  • Sarah Zennou
  • Manuel Yguel
  • Peter Niebert
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2791)


We present ELSE, a new state generator for timed automata. ELSE is based on VERIMAG’s IF-2.0 specification language and is designed to be used with state exploration tools like CADP. In particular, it compiles IF-2.0 specifications to C programs that link with CADP. It thus concentrates on the generation of comparatively small state spaces and integrates into existing tool chains. The emphasis of the ELSE development is on fundamentally different data structures and algorithms, notably on the level of zones. Rather than representing possible values of clocks at a given symbolic state, event zones represent in an abstract way the timing constraints of past and future events.


Symbolic State Reachability Graph Time Automaton Event Zone Partial Order Reduction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AD94]
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  2. [BFG+99]
    Bozga, M., Fernandez, J.-C., Ghirvu, L., Graf, S., Krimm, J.-P., Mounier, L.: IF: An intermediate representation and validation environment for timed asynchronous systems. World Congress on Formal Methods (1), 307–327 (1999)Google Scholar
  3. [BJLY98]
    Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 485–500. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  4. [BLP+99]
    Behrmann, G., Larsen, K., Pearson, J., Weise, C., Yi, W., Lind-Nielsen, J.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 341–353. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  5. [DT98]
    D’Souza, D., Thiagarajan, P.S.: Distributed interval automata: A subclass of timed automata, Internal Report TCS-98-3 (1998)Google Scholar
  6. [DY96]
    Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. In: IEE Real-Time Systems Symposium, pp. 73–81 (December 1996)Google Scholar
  7. [God96]
    Godefroid, P.: Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. In: Godefroid, P. (ed.) Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032, Springer, Heidelberg (1996)Google Scholar
  8. [LNZ03]
    Lugiez, D., Niebert, P., Zennou, S.: Clocked mazurkiewicz traces for partial order reductions of timed automata, draft (2003), available at
  9. [LPY95]
    Larsen, K., Pettersson, P., Yi, W.: Model-checking for real-time systems. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, pp. 62–88. Springer, Heidelberg (1995)Google Scholar
  10. [Min99]
    Minea, M.: Partial order reduction for verification of timed systems, Ph.D. thesis, Carnegie Mellon University (1999)Google Scholar
  11. [Pel93]
    Peled, D.: All from one, one for all: On model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)Google Scholar
  12. [YS97]
    Yoneda, T., Schlingloff, B.-H.: Efficient verification of parallel real-time systems. Formal Methods in System Design 11(2), 197–215 (1997)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Sarah Zennou
    • 1
  • Manuel Yguel
    • 1
  • Peter Niebert
    • 1
  1. 1.Laboratoire d’Informatique Fondamentale de MarseilleUniversité de Provence – CMIMarseille Cedex 13

Personalised recommendations