Timed Process Algebras: A Tutorial

  • Matthew Hennessy
Part of the NATO ASI Series book series (NATO ASI F, volume 118)


In this set of notes we give an overview of a particular approach to describing timed concurrent systems. The starting point is a well-developed semantic theory of process algebras based on testing. This consists of an operational semantics for a “time-free” process description language, a behavioural equivalence based on testing and an algebraic characterisation of this equivalence. We add to this language one timing construct, a time-out operator, and show how the theory can be extended to this time enriched language. This extended language is certainly restricted in its ability to describe timing phenomena but in the last section we show how it may be used as the basis for more expressive timed process description languages.

This extended language is certainly restricted in its ability to describe timing phenomena but in the last section we show how it may be used as the basis for more expressive timed process description languages.


Transition System Clock Cycle Finite Subset Operational Semantic Proof System 
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. [BB92]
    J. C. M. Baeten and J. A. Bergstra. Discrete time process algebra. Technical Report P9208, University of Amsterdam, 1992.Google Scholar
  2. [BG88]
    G. Berry and G. Gonthier. The synchronous programming language ESTEREL: design, semantics, implementation. Report 842, INRIA, Centre Sophia-Antipolis, Valbonne Cedex, 1988. To appear in Science of Computer Programming Google Scholar
  3. [DH84]
    R. DeNicola and M. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 24: 83–113, 1984.MathSciNetCrossRefGoogle Scholar
  4. [Gro90]
    J.F. Groote. Specification and verification of real time systems in ACP. Report CS-R9015, CWI, Amsterdam, 1990. An extended abstract appeared in L. L.grippo, R.L. Probert and H. Ural, editors, Proceedings 10 t h International Symposium on Protocol Specification, Testing and Verification, Ottawa, pages 261–274, 1990.Google Scholar
  5. [Gue81]
    I. Guessarian. Algebraic Semantics. Lecture Notes in Computer Science vol 99, 1981.Google Scholar
  6. [Han91]
    Hans A. Hansson. Time and Probability in Formal Design of Distributed Systems. Ph.d. thesis, Uppsala University, 1991.Google Scholar
  7. [Hen88]
    M. Hennessy. An Algebraic Theory of Processes. MIT Press, 1988.Google Scholar
  8. [Hen91]
    M. Hennessy. A proof system for communicating processes with value—passing. Formal Aspects of Computer Science, 3: 346–366, 1991.CrossRefMATHGoogle Scholar
  9. [HI91]
    M. Hennessy and A. Ingolfsdottir. A theory of communicating processes with value-passing. Information and Computation, to appear, 1991.Google Scholar
  10. [Hoa85]
    C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.Google Scholar
  11. [HR91]
    M. Hennessy and T. Regan. A process algebra for timed systems. Technical Report 5/91, CSAI, University of Sussex, 1991.Google Scholar
  12. [Lan89]
    R. Langerak. A testing theory for LOTOS using deadlock detection. In E. Brinksma, G. Scollo, and C.A. Vissers, editors, Proceedings of the Ninth International Conference on Protocol Specification, Testing and Verification, 1989.Google Scholar
  13. Lin91] H. Lin. Process Algebra Manipulator: User Guide. In K. Larsen, A. Skou (eds.), Proceedings of CAV91,Lecture Notes in Computer Science 575, Springer-Verlag 1991. Also Sussex Computer Science Tech. Rep. 9/91.Google Scholar
  14. [Mí189]
    R. Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
  15. MT90] F. Moller and C. Tofts. A temporal calculus of communicating systems. In Proc. Concur 90,pages 401–415. Springer-Verlag, 1990. LNCS 458.Google Scholar
  16. [MV89]
    S. Mauw and G.J. Veltink. An introduction to PSFa. In J. Diaz and F. Orejas, editors, TAPSOFT89, vol 2, volume 352 of Lecture Notes in Computer Science, pages 272–285, 1989.Google Scholar
  17. [NS90]
    X. Nicollin and J. Sifakis. The algebra of timed processes ATP: Theory and application. Technical Report RT-C26, Laboratoire de Génie Informatique de Grenoble, 1990. to appear in Information and Computation.Google Scholar
  18. [P1o81]
    G.D. Plotkin. A structural approach to operational semantics. Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.Google Scholar
  19. [Reg92]
    T. Regan. A Process Algebra for Real-Time Systems. Ph.d. thesis, University of Sussex, 1992.Google Scholar
  20. [Wan91]
    Wang Yi. A Calculus of Real Time Systems. Ph.D. thesis, Chalmers University, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Matthew Hennessy
    • 1
  1. 1.University of SussexUK

Personalised recommendations