Skip to main content
SpringerLink
Log in

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

  • Conference paper
  • First Online:
Book cover Real-Time: Theory in Practice (REX 1991)

Part of the book series: Lecture Notes in Computer Science ((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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. E. Brinksma, “On the Design of Extended LOTOS“, Ph.D. Thesis, University of Twente, 1988.

    Google Scholar 

  2. 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. T. Bolognesi, E. Brinksma, “Introduction to the ISO Specification Language LOTOS”, Computer Networks and ISDN Systems, Vol. 14, No 1, 1987.

    Google Scholar 

  4. J.C.M. Baeten, J.A. Bergstra, ‘Real Time Process Algebra', Technical Report, Centre for Mathematics and Computer Science, Amsterdam, 1989.

    Google Scholar 

  5. 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. J. A. Bergstra, J. W. Klop, “Process Algebra for Synchronous Communication”, Information and Control, 60 (1–3), 1984.

    Google Scholar 

  7. 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. 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. 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. 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. 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–287

    Google Scholar 

  12. M. Hennessy, T. Regan, ‘A Temporal Process Algebra', Tech. Rep. 2/90, University of Sussex, April 1990.

    Google Scholar 

  13. N. D. Jones, L. H. Landweber, Y. E. Lien, “Complexity of some problems in Petri Nets”, Theoretical Computer Science 4, 1977, pp. 277–299.

    Article  Google Scholar 

  14. M. Minsky, “Recursive unsolvability of Post's problem”, Ann. of Math. 74, 1961, pp. 437–454.

    Google Scholar 

  15. R. Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, Vol.92, Springer-Verlag, 1980.

    Google Scholar 

  16. R. Milner, “Calculi for Synchrony and Asynchrony”, Theor. Computer Science, 25, 1983.

    Google Scholar 

  17. 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.

    Article  Google Scholar 

  18. F. Moller, C. Tofts, “A Temporal Calculus of Communicating Systems”, Proceed. of CONCUR'90, LNCS N. 458, North-Holland, 1990.

    Google Scholar 

  19. 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. 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. G. D. Plotkin, “A structural approach to operational semantics”, Tech. Rep. DAIMI FN-19, Aarhus Univ., Computer Science Dept., Denmark, 1981.

    Google Scholar 

  22. 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. 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. 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. 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. S. Schneider, ‘An Operational Semantics for Timed CSP', unpublished manuscript, Oxford University, Programming Research Group, may 1991.

    Google Scholar 

  27. 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. 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. 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 

Download references

Author information

Authors and Affiliations

  1. CNUCE/C.N.R., 36, Via S. Maria, 56100, Pisa, Italy

    Tommaso Bolognesi

  2. Fondazione U. Bordoni, 59, Via B. Castiglione, 00142, Roma, Italy

    Ferdinando Lucidi

Authors
  1. Tommaso Bolognesi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ferdinando Lucidi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. W. de Bakker C. Huizing W. P. de Roever G. Rozenberg

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bolognesi, T., Lucidi, F. (1992). Timed process algebras with urgent interactions and a unique powerful binary operator. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds) Real-Time: Theory in Practice. REX 1991. Lecture Notes in Computer Science, vol 600. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0031990

Download citation

  • DOI: https://doi.org/10.1007/BFb0031990

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55564-3

  • Online ISBN: 978-3-540-47218-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation