Advertisement

Analysis of Reactive Systems with n Timers

  • Anne Bergeron
  • Riccardo Catalano
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2214)

Abstract

In this paper, we develop theoretical, as well as practical, tools for the synthesis and the verification of processes that contain n timers. Such tools are equally adapted to numerical calculations as to symbolical ones, thus allowing for parametric analysis. The results we have obtained rely on a simple and efficient representation of the states of an automaton that recognizes the behaviors of the process. This representation is based on a mechanical structure which helps us encode the states in a compact manner and leads to simple algorithms.

Keywords

Event Sequence Time Line Symbolic Timer Minimal Position Time Automaton 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    R. Alur and D. Dill, The Theory of Timed Automata, Theoretical Computer Science, 126 (1994) 183–235.CrossRefMathSciNetGoogle Scholar
  2. 2.
    A. Bergeron and A.M. Roy-Boulard, Contraintes temporelles paramétrisées et produits synchronisés, Proc. of NOTERE’97, Pau, France, (1997) 191–205.Google Scholar
  3. 3.
    A. Bergeron and A.M. Roy-Boulard, Contrôleurs temps-réel paramétrisés, Proc. of ADPM’98, Reims, France, (1998).Google Scholar
  4. 4.
    A. Bergeron, On the Rational Behaviors of Concurrent Timers, Theoretical Computer Science 189 (1997) 229–237.CrossRefMathSciNetGoogle Scholar
  5. 5.
    B. Berthomieu and M. Diaz, Modelingand Verification of Time Dependent systems Usingtime d Petri Nets, IEEE Transactions on Software Engineering, Vol. 17, No. 3, (1991), 259–273.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Anne Bergeron
    • 1
  • Riccardo Catalano
  1. 1.LACIMUniversité du Québec à MontréalMontréalCanada

Personalised recommendations