From ATP to timed graphs and hybrid systems

  • Xavier Nicollin
  • Joseph Sifakis
  • Sergio Yovine
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 600)


The paper presents results of ongoing work aiming at the unification of some behavioural description formalisms for timed systems.

We propose for ATP a very general semantics in terms of a time domain.

It is then shown how ATP can be translated into a variant of timed graphs. This result allows the application of existing model-checking techniques to ATP.

Finally, we propose a notion of hybrid systems as a generalisation of timed graphs. Such systems can evolve, either by executing a discrete transition, or by performing some “continuous” transformation.

The formalisms studied admit the same class of models: time deterministic and time continuous, possibly infinitely branching transition systems labelled by actions or durations.


real-time specification of timed systems process algebra timed graphs hybrid systems 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [ACD90]
    R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proceedings of the fifth annual IEEE symposium on Logic In Computer Science, pages 414–425, Philadelphia, PA., June 1990.Google Scholar
  2. [BC85]
    G. Berry and L. Cosserat. The Esterel synchronous programming language and its mathematical semantics. In LNCS 197: Proceedings CMU Seminar on Concurrency, Springer-Verlag, 1985.Google Scholar
  3. [BK84]
    J.A. Bergstra and J.W. Klop. Algebra of Communicating Processes. Technical Report CS-R8420, Centre for Mathematics and Computer Science, Amsterdam, the Netherlands, 1984.Google Scholar
  4. [BK86]
    J.A. Bergstra and J.W. Klop. Process algebra: specification and verification in bisimulation semantics. In M. Hazewinkel, J.K. Lenstra, and L.G.L.T. Meertens, editors, Proceedings of the CWI Symposium Mathematics and Computer Science II (CWI Monograph 4), pages 61–94, North Holland, Amsterdam, 1986.Google Scholar
  5. [MT90]
    F. Moller and C. Tofts. A Temporal Calculus of Communicating Processes. In J.C.M. Baeten and J.W. Klop, editors, LNCS 458. Proceedings of CONCUR '90 (Theories of Concurrency: Unification and Extension), Amsterdam, the Netherlands, pages 401–415, Springer-Verlag, August 1990.Google Scholar
  6. [NRSV90]
    X. Nicollin, J.-L. Richier, J. Sifakis, and J. Voiron. ATP: an Algebra for Timed Processes. In Proceedings of the IFIP TC 2 Working Conference on Programming Concepts and Methods, Sea of Gallilee, Israel, April 1990.Google Scholar
  7. [NS90]
    X. Nicollin and J. Sifakis. The algebra of timed processes ATP: theory and application. Technical Report RT-C26, LGI-IMAG, Grenoble, Prance, December 1990.Google Scholar
  8. [Plo81]
    G.D. Plotkin. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, Århus University. Computer Science Department, Århus, Denmark, 1981.Google Scholar
  9. [Wan90]
    Wang Yi. Real-time behaviour of asynchronous agents. In J.C.M. Baeten and J.W. Klop, editors, LNCS 458. Proceedings of CONCUR '90 (Theories of Concurrency: Unification and Extension), Amsterdam, the Netherlands, pages 502–520, Springer-Verlag, August 1990.Google Scholar
  10. [Wan91]
    Wang Yi. CCS + Time = an Interleaving Model for Real Time Systems. In Proceedings of ICALP '91, Madrid, Spain, July 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Xavier Nicollin
    • 1
  • Joseph Sifakis
    • 1
  • Sergio Yovine
    • 1
  1. 1.Laboratoire de Génie InformatiqueGrenoble CedexFrance

Personalised recommendations