Advertisement

Open Maps and Trace Semantics for Timed Partial Order Models

  • Irina B. Virbitskaite
  • Nataly S. Gribovskaja
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2890)

Abstract

The intention of the paper is to show the applicability of the general categorical framework of open maps to the setting of partial order models with a dense time domain. In particular, we define a category of timed event structures, where the morphisms are to be thought of as simulations, and an accompanying (sub)category of timed pomsets which provides us with a notion of open maps. Then, we show that the abstract equivalence obtained from the framework of open maps coincides with a timed extension of the well-known trace equivalence based on Pratt’s partial orders.

Keywords

Category theory timed event structures partial order semantics trace equivalence 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., Courcoubetis, C., Dill, D.: Model checking in dense real time. Information and Computation 104, 2–34 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Alur, R., Dill, D.: The theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Andreeva, M.V., Bozhenkova, E.N., Virbitskaite, I.B.: Analysis of timed concurrent models based on testing equivalence. Fundamenta Informaticae 43(1-4), 1–20 (2000)zbMATHMathSciNetGoogle Scholar
  4. 4.
    Aceto, L., Murphi, D.: Timing and causality in process algebra. Acta Informatica 33(4), 317–350 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Baier, C., Katoen, J.-P., Latella, D.: Metric semantics for true concurrent real time. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 568–579. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  6. 6.
    Bednarczyk, M.A.: Hereditory history preserving bisimulation or what is the power of the future perfect in program logics. Technical Report, Polish Academy of Science, Gdansk (1991)Google Scholar
  7. 7.
    Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 485–496. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  8. 8.
    Čerāns, K.: Decidability of bisimulation equivalences for parallel timer processes. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 302–315. Springer, Heidelberg (1993)Google Scholar
  9. 9.
    Goltz, U., Wehrheim, H.: Causal testing. In: Penczek, W., Szałas, A. (eds.) MFCS 1996. LNCS, vol. 1113, pp. 394–406. Springer, Heidelberg (1996)Google Scholar
  10. 10.
    Henzinger, T.A., Manna, Z., Pnueli, A.: Timed transition systems. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 226–251. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  11. 11.
    Hune, T., Nielsen, M.: Timed bisimulation and open maps. In: Brim, L., Gruska, J., Zlatuška, J. (eds.) MFCS 1998. LNCS, vol. 1450, pp. 378–387. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  12. 12.
    Jacobs, B., Rutten, J.: A tutorial on (Co)algebras and (Co)induction. EATCS Bulletin 62, 222–259 (1997)zbMATHGoogle Scholar
  13. 13.
    Joyal, A., Nielsen, M., Winskel, G.: Bisimulation from open maps. Information and Computation 127(2), 164–185 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Katoen, J.-P., Langerak, R., Latella, D., Brinksma, E.: On specifying realtime systems in a causality-based setting. In: Jonsson, B., Parrow, J. (eds.) FTRTFT 1996. LNCS, vol. 1135, pp. 385–404. Springer, Heidelberg (1996)Google Scholar
  15. 15.
    Laroussinie, F., Larsen, K.G., Weise, C.: From timed automata to logic and back. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 529–539. Springer, Heidelberg (1995)Google Scholar
  16. 16.
    Maggiolo-Schettini, A., Winkowski, J.: Towards an algebra for timed behaviours. Theoretical Computer Science 103, 335–363 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Murphy, D.: Time and duration in noninterleaving concurrency. Fundamenta Informaticae 19, 403–416 (1993)zbMATHMathSciNetGoogle Scholar
  18. 18.
    Nielsen, M., Cheng, A.: Observing behaviour categorically. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 263–278. Springer, Heidelberg (1995)Google Scholar
  19. 19.
    Pratt, V.R.: Modeling concurrency with partial orders. Int. Journal of Parallel Programming 15(1), 33–71 (1986)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Virbitskaite, I.B.: An observation semantics for timed event structures. In: Bjørner, D., Broy, M., Zamulin, A.V. (eds.) PSI 2001. LNCS, vol. 2244, pp. 215–225. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  21. 21.
    Weise, C., Lenzkes, D.: Efficient scaling-invariant checking of timed bisimulation. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 176–188. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  22. 22.
    Winskel, G.: An introduction to event structures. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol. 354, pp. 364–397. Springer, Heidelberg (1989)CrossRefGoogle Scholar
  23. 23.
    Winskel, G., Nielsen, M.: Models for concurrency. Handbook of Logic in Computer Science 4 (1995)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Irina B. Virbitskaite
    • 1
  • Nataly S. Gribovskaja
    • 1
  1. 1.Siberian Division of the Russian Academy of SciencesA.P. Ershov Institute of Informatics SystemsNovosibirskRussia

Personalised recommendations