Advertisement

Timed process algebras with urgent interactions and a unique powerful binary operator

  • Tommaso Bolognesi
  • Ferdinando Lucidi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 600)

Abstract

A timed process algebra called ρ1 is introduced, which offers operators for specifying time-dependent behaviours and, in particular, the urgency of a given (inter-)action involving one or more processes. The formal semantics of the language is given in a style similar to the one adopted by Tofts and Moller for TCCS: two independent sets of inference rules are provided, which handle, respectively, the occurrence of actions and the passing of time. The language, partly inspired to LOTOS, can specify in a natural way the “wait-until-timeout” scenario, and we prove that, due to its two time-related operators, it can simulate Turing machines. The formalism appears as a most natural transposition in the realm of process algebras of an expressivity-preserving subset of the well known Time Petri Nets of Merlin and Farber. An enhanced timed process algebra called ρ2, which includes only five operators, and preserves the expressivity of ρ1, is then proposed: it combines mutual disabling, choice, parallel composition with synchronization, and pure interleaving, into a unique, general-purpose, parametric binary operator.

Keywords

timed process algebra timed Petri Net 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [B88]
    E. Brinksma, “On the Design of Extended LOTOS“, Ph.D. Thesis, University of Twente, 1988.Google Scholar
  2. [B89]
    E. Brinksma (ed.) — ISO — Information Processing Systems — Open Systems Interconnection — “LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour”, IS 8807, 1989.Google Scholar
  3. [BB87]
    T. Bolognesi, E. Brinksma, “Introduction to the ISO Specification Language LOTOS”, Computer Networks and ISDN Systems, Vol. 14, No 1, 1987.Google Scholar
  4. [BB89]
    J.C.M. Baeten, J.A. Bergstra, ‘Real Time Process Algebra', Technical Report, Centre for Mathematics and Computer Science, Amsterdam, 1989.Google Scholar
  5. [BC89]
    T. Bolognesi, P. Cremonese, “The Weakness of Some Timed Models for Concurrent Systems”, Technical Report CNUCE C89-29, CNUCE-C.N.R., Pisa, October 1989.Google Scholar
  6. [BK84]
    J. A. Bergstra, J. W. Klop, “Process Algebra for Synchronous Communication”, Information and Control, 60 (1–3), 1984.Google Scholar
  7. [BLT90]
    T. Bolognesi, F. Lucidi, S. Trigila, “From Timed Petri Nets to Timed LOTOS”, Proceedings of the Tenth International IFIP WG6.1 Symposium on Protocol Specification, Testing, and Verification, L. Logrippo, R. L. Probert, H. Ural editors, North-Holland 1990.Google Scholar
  8. [BLT90a]
    T. Bolognesi, F. Lucidi, S. Trigila, “New Proposals for Timed-Interaction LOTOS”, Technical Rep. 5-B-55-90, Fondazione U. Bordoni, Roma, Italy, 1990.Google Scholar
  9. [BR85]
    T. Bolognesi, H. Rudin, “On the Analysis of Time-Dependent Protocols by Network Flow Algorithms”, Proceedings of the IFIP WG6.1 Fourth International Workshop on Protocol Specification, Testing, and Verification, Y. Yemini, R. Strom, S. Yemini editors, North-Holland 1985, pp.491–514.Google Scholar
  10. [G90]
    J. F. Groote, “Specification and Verification of Real Time Systems in ACP”, Proceedings of the Tenth International IFIP WG6.1 Symposium on Protocol Specification, Testing, and Verification, L. Logrippo, R. L. Probert, H. Ural editors, North-Holland 1990.Google Scholar
  11. [HJ90]
    H. Hansson, B. Jonsson, “A Calculus for Communicating Systems with Time and Probabilities', Proceedings of the 11th Real-Time Systems Symposium, IEEE Computer Society, 1990, pp. 278–287Google Scholar
  12. [HR90]
    M. Hennessy, T. Regan, ‘A Temporal Process Algebra', Tech. Rep. 2/90, University of Sussex, April 1990.Google Scholar
  13. [JLL77]
    N. D. Jones, L. H. Landweber, Y. E. Lien, “Complexity of some problems in Petri Nets”, Theoretical Computer Science 4, 1977, pp. 277–299.CrossRefGoogle Scholar
  14. [M61]
    M. Minsky, “Recursive unsolvability of Post's problem”, Ann. of Math. 74, 1961, pp. 437–454.Google Scholar
  15. [M80]
    R. Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, Vol.92, Springer-Verlag, 1980.Google Scholar
  16. [M83]
    R. Milner, “Calculi for Synchrony and Asynchrony”, Theor. Computer Science, 25, 1983.Google Scholar
  17. [MF76]
    P. Merlin, D. J. Farber, “Recoverability of Communication Protocols — Implications of a Theoretical Study”, IEEE Trans. Commun., Vol. COM-24, Sept. 1976, pp. 1036–1043.CrossRefGoogle Scholar
  18. [MT90]
    F. Moller, C. Tofts, “A Temporal Calculus of Communicating Systems”, Proceed. of CONCUR'90, LNCS N. 458, North-Holland, 1990.Google Scholar
  19. [NRSV90]
    X. Nicollin, J.-L. Richier, J. Sifakis, J. Voiron, “ATP: An Algebra for Timed Processes” Project SPECTRE, Groupe Spécification et Analyse des Systemes, Laboratoire de Génie Informatique de Grenoble, Technical Report RT-C16, Jan. 1990.Google Scholar
  20. [NS90]
    X. Nicollin, J. Sifakis “The Algebra of Timed Processes ATP: Theory and Applications” Project SPECTRE, Groupe Spécification et Analyse des Systemes, Laboratoire de Génie Informatique de Grenoble, Technical Report RT-C26, Dec. 1990.Google Scholar
  21. [P81]
    G. D. Plotkin, “A structural approach to operational semantics”, Tech. Rep. DAIMI FN-19, Aarhus Univ., Computer Science Dept., Denmark, 1981.Google Scholar
  22. [QAF89]
    J. Quemada, A. Azcorra, D.Frutos “A Timed Calculus for LOTOS”, Proceedings of FORTE '89 Second International Conference on Formal Description Techniques for Distributed Systems and Communications Protocols, Vancouver,Canada, December 1989.Google Scholar
  23. [QF87]
    J. Quemada, A. Fernandez, “Introduction of Quantitative Relative Time into LOTOS”, Proceedings of IFIP WG 6.1 Seventh International Conference on Protocol Specification, Testing, and Verification, H.Rudin, C. H. West Editors, North-Holland, 1987, pp. 105–121.Google Scholar
  24. [R85]
    H. Rudin, “Time in Formal Protocol Specifications”, Proceedings of the GI/NTG Conference on Communication in Distrib. Systems, Karlsruhe, West Germany, March 11–15, 1985, Springer-Verlag Informatic Series N. 95, pp. 575–587.Google Scholar
  25. [RR86]
    G. M. Reed and A. W. Roscoe, “A Timed Model for Communicating Sequential Processes”, Proceedings of ICALP'86, Lecture Notes in Computer Science n. 226, Springer-Verlag, 1986, pp. 314–323.Google Scholar
  26. [S91]
    S. Schneider, ‘An Operational Semantics for Timed CSP', unpublished manuscript, Oxford University, Programming Research Group, may 1991.Google Scholar
  27. [VHTZ89]
    W. H. P. van Hulzen, P. A. J. Tilanus, H. Zuidweg, “LOTOS Extended with Clocks”, proceedings of FORTE '89, Second International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, S. T. Vuong editor, North-Holland 1990.Google Scholar
  28. [W83]
    B. Walter, “Timed Petri-Nets for Modelling and Analyzing Protocols with Real-Time Characteristics”, Proceedings of 3rd IFIP Workshop on Protocol Specification, Testing, and Verification, (H.Rudin, C. H. West Editors), North-Holland, 1983, pp. 149–159.Google Scholar
  29. [Y90]
    W. Yi, ‘Real-time behaviour of asynchronous agents', in J. C. M. Baeten and J. W. Klop, editors, LNCS 458, Proceedings of Concur '90, Amsterdam, The Netherlands, Springer-Verlag, Aug. 1990, pp. 502–520.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Tommaso Bolognesi
    • 1
  • Ferdinando Lucidi
    • 2
  1. 1.CNUCE/C.N.R.PisaItaly
  2. 2.Fondazione U. BordoniRomaItaly

Personalised recommendations