Timed Delay Bisimulation is an Equivalence Relation for Timed Transition Systems

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

Abstrakty

EN

Timed transition systems are a widely studied model for real-time systems. The intention of the paper is to show the applicability of the general categorical framework of openmaps in order to prove that timed delay equivalence is indeed an equivalence relation in the setting of timed transition systems with invariants. In particular, we define a category of the model under consideration and an accompanying (sub)category of observations to which the corresponding notion of open maps is developed. We then use the open maps framework to obtain an abstract equivalence relation which is established to coincide with timed delay bisimulation.

Słowa kluczowe

EN

timed transition systems; timed delay equivalence; category theory; open maps

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 93, nr 1-3
• Strony: 127--142
• Opis fizyczny: Bibliogr. 27 poz.

Twórcy

autor

Gribovskaya N.

autor

Virbitskaite I.

• A.P. Ershov Institute of Informatics Systems, SB RAS 6, Acad. Lavrentiev av., Novosibirsk, 630090, Russia, and Novosibirsk State University 2, Pirogova st., Novosibirsk, 630090, Russia,

Bibliografia

• [1] Aceto, L., Jeffrey, A.: A complete axiomatization of timed bisimulation for a class of timed regular behaviours, Theoretical Computer Science, 152, 1995, 251-268.
• [2] Alur, R., Courcoubetis, C., Henzinger, T.A.: The observational power of clocks, Proc. CONCUR'94 (B. Jonsson, J. Parrow, Eds.), LNCS 836, Springer-Verlag, Berlin, 1994.
• [3] Alur, R., Dill, D.: The theory of timed automata, Theoretical Computer Science, 126, 1994, 183-235.
• [4] Alur, R., Henziger, T.A.: Logics and models of real time: a survey, Proc. Real-Time: Theory in Practice (J.W. de Bakker, C. Huizing,W.P. de Roever, G. Rozenberg, Eds.), LNCS 600, Springer-Verlag, Berlin, 1991.
• [5] 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.
• [6] Andreeva, M.V., Virbitskaite, I.B.: Timed equivalences for timed event structures, Proc. Parallel Computing Technologies (V.E. Malyshkin, Ed.), LNSC 3606, Springer-Verlag, Berlin, 2005.
• [7] Baeten, J.C.M., Middelburg, C.A.: Process Algebra with timing, EATCS Monograph, Springer, 2002.
• [8] Bihler, E., Vogler, W.: Timed Petri Nets: Efficiency of asynchronous systems, Proc. Formal Methods for the Design of Real-Time Systems (M. Bernardo, F. Corradini, Eds.), LNCS 3185, Springer-Verlag, Berlin, 2004.
• [9] Borceux, F.: , Handbook of Categorical Algebra, vol. 2, 3, Encyclopedia of Mathematics and its Applications, vol. 51,52, Cambridge University Press, 1994.
• [10] Čerans, K.: Decidability of bisimulation equivalences for parallel timer processes, Proc. Computer Aided Verification (G. von Bochmann, D. K. Probst, Eds.), LNCS 663, Springer-Verlag, Berlin, 1993.
• [11] Chatain, T., Jard, C.: Time supervision of concurrent systems using symbolic unfoldings of time Petri nets, Proc. Formal Modeling and Analysis of Timed Systems (P. Pettersson, W. Yi, Eds.), LNCS 3829, Springer-Verlag, Berlin, 2005.
• [12] Fokkink, W., Pang, J., Wijs, A.: Is timed branching bisimilarity an equivalence indeed? Proc. Formal Modeling and Analysis of Timed Systems (P. Pettersson, W. Yi, Eds.), LNCS 3829, Springer-Verlag, Berlin, 2005.
• [13] Glabbeek, R., Weijland, W.P.: Brancing time and abstraction in bisimulation semantics, Proc. IFIP 11th World Computer Congress (G.X. Ritter, Ed.), Information Processing 89, 1989, 613-618.
• [14] Hennessy, M., Milner, R.: On observing nondeterminism and concurrency, Proc. Automata, Languages and Programming (J. W. de Bakker, Jan van Leeuwen, Eds.), LNCS 85, Springer-Verlag, Berlin, 1980.
• [15] Henzinger, T.A., Majumdar, R., Prabhu, V.S.: Quantifying similarities between timed systems, Proc. Formal Modeling and Analysis of Timed Systems (P. Pettersson, W. Yi, Eds.), LNCS 3829, Springer-Verlag, Berlin, 2005.
• [16] Hune, T., Nielsen, M.: Bisimulation and open maps for timed transition systems, Fundamenta Informaticae, 38, 1999, 61-77.
• [17] Joyal, A., Moerdijk, I.: A completeness theorem for open maps, Annual Pure Applied Logic, 70, 1997, 51-86.
• [18] Joyal, A., Nielsen, M., Winskel, G.: Bisimulation from open maps, Information and Computation, 127(2), 1996, 164-185.
• [19] Klusener A.S.: The silent step in time, Proc. CONCUR '92 (R. Cleaveland, Ed.), LNCS 630, Springer-Verlag, Berlin, 1992.
• [20] Milner, R.: A calculus of communicating systems, LNCS 92, Springer-Verlag, Berlin, 1980.
• [21] Milner, R.: Modal characterization of observable machine behaviour, Proc. CAAP '81 (E. Astesiano, C. Bohm, Eds.), LNCS 112, Springer-Verlag, Berlin, 1981.
• [22] Nielsen, M., Cheng, A.: Observing behaviour categorically, Proc. Foundations of Software Technology and Theoretical Computer Science (P.S. Thiagarajan, Ed.), LNCS 1026, Springer-Verlag, Berlin, 1996.
• [23] Nielsen M., Winskel G.: Petri nets and bisimulation. Theoretical Computer Science, 153 (1996)
• [24] B. Steffen, C. Weise.: Deciding testing equivalence for real-time processes with dense time, Proc. Mathematical Foundations of Computer Science (A.M. Borzyszkowski, S. Sokolowski, Eds.), LNCS 711, Springer-Verlag, Berlin, 1993.
• [25] Virbitskaite, I.B., Gribovskaya N.S.: Open maps and observational equivalences for timed partial order models, Fundamenta Informaticae, 60(1-4), 2004, 383-399.
• [26] Weise, C., Lenzkes, D.: Efficient scaling-invariant checking of timed bisimulation, Proc. STACS '97 (R. Reischuk, M. Morvan, Eds.), LNCS 1200, Springer-Verlag, Berlin, 1997.
• [27] van der Zwaag, M.B.: The cones and foci proof technique for timed transition systems, Information Processing Letters, 80(1), 2001, 33-40.