Open Maps and Observational Equivalences for Timed Partial Order Models

• Autorzy: Virbitskaite I.B. , Gribovskaya N.S.
• Języki publikacji: EN

Abstrakty

EN

The intention of the paper is to show the applicability of the general categorical framework of open maps to the setting of timed extensions of partial order models, in order to transfer general concepts of equivalences to the models. In particular, we define categories of timed event structures, whose morphisms are to be thought of as simulations, and accompanying (sub)categories of observations, to which the corresponding notions of open maps are developed. We then use the open maps framework to obtain abstract bisimilarities which are established to coincide with timed extensions of well-known partial order based equivalences.

Słowa kluczowe

EN

categorical theory; open maps; timed event structures; timed partial order equivalences

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 60, nr 1-4
• Strony: 383--399
• Opis fizyczny: Bibliogr. 39 poz.

Twórcy

autor

Virbitskaite I.B.

• A.P. Ershov Institute of Informatics Systems, Siberian Division of the Russian Academy of Sciences, 6, Acad. Lavrentiev avenue, 630090, Novosibirsk, Russia

autor

Gribovskaya N.S.

• A.P. Ershov Institute of Informatics Systems, Siberian Division of the Russian Academy of Sciences, 6, Acad. Lavrentiev avenue, 630090, Novosibirsk, Russia

Bibliografia

• [1] ACETO, L., DE NICOLA, R., FANTECHI, A.: Testing equivalences forevent structures. Lecture Notes in Computer Science 280, 1987. 1-20.
• [2] ACETO, L.. MURPHI. D.: Timing and causality in process algebra. Acta Informática 33(4), 1996. 317-350.
• [3] ALUR, R., DILL. D.: The theory of timed automata. Theoretical Computer Science 126. 1994, 183-235.
• [4] ANDREEVA, M.V., BOZHENKOVA. E.N., VIRBITSKAITE, I.B.: Analysis of timed concurrent models based on testing equivalence. Fundamenta Informaticae 43(1-4). 2000. 1-20.
• [5] BAIER, C., KATOEN, J.-P., LATELLA, D.: Metric semantics for true concurrent real time. In Proc. 25th Int. Colloquium, ICALP’98, Aalborg. Denmark, 1998. 568-579.
• [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.
• [7] BORCEUX, F.: Handbook of Categorical Algebra, vol. 2, 3. Encyclopedia of Mathematics and its Applications, vol. 51.52. Cambridge University Press, 1994.
• [8] BOUDOL, G., CASTELLANI, I.: Concurrency and atomicity. Theoretical Computer Science 59. 1989. 25-84.
• [9] CASLEY. R.T., CREW, R.F., MESEGUER. J., PRATT, V.R.:Temporal structures. Mathematical Structures in Computer Science 1(2). 1991, 179-213.
• [10] CATTANI, G.L., SASSONE, V.: Higher dimentional transition systems. In Proc. L1CS'96, 1996, 55-62.
• [11] CERÄNS. K.: Decidability of bisimulation equivalences for parallel timer processes. Lecture Notes in Computer Science 663. 1993,302-315.
• [12] FlORE, M., CATTANI, G.L., WINSKEL, G.: Weak bisimulation and open maps. In Proc. LICS'99, 1999, 214-225.
• [13] FROESCHLE, S.: Decidability of plain and hereditary history-preserving bisimilatiry for BPP In Proc. EX-PRESS'99, 1999.
• [14] VAN GLABBEEK. R.J.: The linear time - branching time spectrum II: the semantics of sequential systems with silent moves. Extended abstract. Lecture Notes in Computer Science 715. 1993, 66-81.
• [15] GLABBEEK. R., GOLTZ, U.: Equivalence notions for concurrent systems and refinement of action. Lecture Notes in Computer Science 379, 1989, 237-248.
• [16] GOLTZ, U., WEHRHEIM, H.: Causal testing. Lecture Notes in Computer Science 1113. 1996, 394-406.
• [17] HENNESSY, M., MILNER. R.: Algebraic laws for nondeterminism and concurrency. Journal of ACM 32. 1985.137-162.
• [18] HENZINGF.R. T.A., MANNA, Z., PNUELI, A.: Timed transition systems. Lecture Notes in Computer Science 600, 1991,226-251.
• [19] HOARE C.A.R.: Communicating sequential processes. Prentice-Hall, London, 1985.
• [20] HlJNE, Т., NIELSEN, М.: Bisimulation and open maps for timed transition systems. Fundamenta Informaticae 38, 1999,61-77.
• [21] JACOBS, B.. RUTTEN, J.: A tutorial on (Co)algebras and (Co)imduction. EATCS Bulletin 62, 1997,222-259.
• [22] JURDZINSKI, M., NIELSEN, М.: Hereditory history preserving bisimilarity is undecidable. Lecture Notes in Computer Science 1770. 2000, 358-372.
• [23] JOYAL, A., NIELSEN, M., WINSKEL. G.: Bisimulation from open maps. Information and Computation 127(2), 1996, 164-185.
• [24] KATOEN, J.-R: Quantitative and qualitative extensions of event structures. PhD thesis. University of Twente. The Netherlands, 1996.
• [25] KATOEN, J.-P., Langerak, R., Latella, D., Brinksma, E.: On specifying real-time systems in a causality-based setting. Lecture Notes in Computer Science 1135, 1996, 385-404.
• [26] LAROUSSINIE. F., LARSEN. K.G., WEISE, C.: From timed automata to logic and back. Lecture Notes in Computer Science 969, 1995, 529-539.
• [27] LlLIUS, J.: Efficient state space search for time Petri nets. In Proc. MFCS'98 Workshop on Concurrency, August 1998. Brno (Czech Republic), FIMU Report Series. FIMU RS-98-06. 1998. 123-130.
• [28] MAGGIOLO-SCHETTINI, A., WINKOWSKI, J.: Towards an algebra for timed behaviours. Theoretical Computer Science 103. 1992. 335-363.
• [29] MUKUND, M.: Hereditary history preserving bisimulation is decidable for trace-labelled systems. Lecture Notes in Computer Science 2255, 2002, 289-300.
• [30] MURPHY, D.: Time and duration in noninterleaving concurrency. Fundamenta lnformaticae 19. 1993,403-416.
• [31] De NICOLA. R., HENNESSY. M.: Testing equiavalence for processes. Theoretical Computer Science 34. 1984, 83-133.
• [32] NIELSEN. M., CHENG, A.: Observing behaviour categorically. Lecture Notes in Computer Science 1026. 1996, 263-278.
• [33] PARK, D.: Concurrency and automata on infinite sequences. Lecture Notes in Computer Science 104. 1981. 167-183.
• [34] PRATT, V.R.: Modeling concurrency with partial orders. Int. Journal of Parallel Programming 15(1). 1986. 33-71.
• [35] VIRBITSKAITE, LB.: An observation semantics for timed event structures. Lecture Notes in Computer Science 2244, 2001,215-225.
• [36] VOGLER. W.: Bisimulation and action refinement. Lecture Notes in Computer Science 480. 1991, 309-321
• [37] WEISE, C., LENZKES, D.: Efficient scaling-invariant checking of timed bisimulation. Lecture Notes in Computer Science 1200. 1997, 176-188.
• [38] WINSKEL. G.: An introduction to event structures. Lecture Notes in Computer Science 354. 1988, 364-397.
• [39] WINSKEL, G., NIELSEN, M.: Models for concurrency. In Handbook of Logic in Computer Science 4, 1995.