Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

Metric semantics for true concurrent real time

  • Conference paper
  • First Online:

Part of the book series:Lecture Notes in Computer Science ((LNCS,volume 1443))

Included in the following conference series:

Abstract

This paper investigates the use of a complete metric space framework for providing denotational semantics to a real-time process algebra. The study is carried out in a non-interleaving setting and is based on a timed extension of Langerak's bundle event structures, a variant of Winskel's event structures. The distance function is based on the amount of time to which event structures do ‘agree’. We show that this intuitive notion of distance is a pseudo metric (but not a metric) on the set of timed event structures. A generalisation to equivalence classes of timed event structures in which we abstract from event names and non-executable events (events that can never appear) is shown to be a complete ultra-metric space. We show that the resulting metric semantics is an abstraction of an existing cpo-based denotational and a related operational semantics for the considered language.

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

Access this chapter

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A.F. Ates, M. Bilgic, S. Saito and B. Sarikaya. Using timed CSP for specification verification and analysis of multi-media synchronization.IEEE J. on Sel. Areas in Comm.,14(1):126–137, 1996.

    Article  Google Scholar 

  2. C. Baier and M.E. Majster-Cederbaum. Denotational semantics in the cpo and metric approach.Th. Comp. Sci.,135:171–220, 1994.

    Article MATH MathSciNet  Google Scholar 

  3. C. Baier and M.E. Majster-Cederbaum. How to interpret consistency and establish consistency results for semantics of concurrent programming languages.Fund. Inf.,29:225–256, 1997.

    MATH MathSciNet  Google Scholar 

  4. C. Baier and M.E. Majster-Cederbaum. Metric semantics from partial order semantics.Acta Inf.,34:701–735, 1997.

    Article MATH MathSciNet  Google Scholar 

  5. J.W. de Bakker and J.I. Zucker. Processes and the denotational semantics of concurrency.Inf. and Contr.,54(1/2):70–120, 1982.

    MATH  Google Scholar 

  6. J.W. de Bakker and E.P. de Vink.Control Flow Semantics. MIT Press, 1996.

    Google Scholar 

  7. T. Bolognesi and E. Brinksma. Introduction to the ISO specification language LOTOS.Comp. Netw. & ISDN Syst.,14:25–59, 1987.

    Article  Google Scholar 

  8. J. Davies, J.W. Bryans and S.A. Schneider. Real-time LOTOS and timed observations. InFormal Description Techniques VIII. Chapmann & Hall, 1995.

    Google Scholar 

  9. J-P. Katoen.Quantitative and Qualitative Extensions of Event Structures. PhD thesis, University of Twente, 1996.

    Google Scholar 

  10. J-P. Katoen, D. Latella, R. Langerak and E. Brinksma. On specifying real-time systems in a causality-based setting. InFormal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 1135, pages 385–405. Springer-Verlag, 1996.

    Google Scholar 

  11. R. Langerak. Bundle event structures: a non-interleaving semantics for LOTOS. InFormal Description Techniques V, pages 331–346. North-Holland, 1993.

    Google Scholar 

  12. R. Loogen and U. Goltz. Modelling nondeterministic concurrent processes with event structures.Fund. Inf.,14(1):39–74, 1991.

    MATH MathSciNet  Google Scholar 

  13. D. Murphy. Time and duration in noninterleaving concurrency.Fund. Inf.,19:403–416, 1993.

    MATH MathSciNet  Google Scholar 

  14. X. Nicollin and J. Sifakis. An overview and synthesis on timed process algebras. InReal-Time: Theory in Practice, LNCS 600, pages 526–548. Springer-Verlag, 1992.

    Google Scholar 

  15. M. Nivat. Infinite words, infinite trees, infinite computations. InFoundations of Computer Science III, Mathematical Centre Tracts109, pages 3–52, 1979.

    MathSciNet  Google Scholar 

  16. M. Nielsen, G.D. Plotkin and G. Winskel. Petri nets, event structures and domains, part 1.Th. Comp. Sc.,13(1):85–108, 1981.

    Article MATH MathSciNet  Google Scholar 

  17. G.M. Reed and A.W. Roscoe. A timed model for Communicating Sequential Processes.Th. Comp. Sc.,58:249–261, 1988.

    Article MATH MathSciNet  Google Scholar 

  18. J.J. Žic. Time-constrained buffer specifications in CSP+T and timed CSP.ACM Transactions on Programming Languages and Systems, 16(6):1661–1674, 1994.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fakultät für Mathematik und Informatik, Universität Mannheim, Seminargebäude A5, D-68159, Mannheim, Germany

    Christel Baier

  2. Lehrstuhl für Informatik VII, Friedrich- Alexander- Universität Erlangen-Nürnberg, Martensstrasse 3, D-91058, Erlangen, Germany

    Joost-Pieter Katoen

  3. CNUCE Istituto del CNR, Via Santa Maria 36, I-56100, Pisa, Italy

    Diego Latella

Authors
  1. Christel Baier

    You can also search for this author inPubMed Google Scholar

  2. Joost-Pieter Katoen

    You can also search for this author inPubMed Google Scholar

  3. Diego Latella

    You can also search for this author inPubMed Google Scholar

Editor information

Kim G. Larsen Sven Skyum Glynn Winskel

Rights and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Baier, C., Katoen, JP., Latella, D. (1998). Metric semantics for true concurrent real time. In: Larsen, K.G., Skyum, S., Winskel, G. (eds) Automata, Languages and Programming. ICALP 1998. Lecture Notes in Computer Science, vol 1443. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055085

Download citation

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp