Observational Equivalences for Timed Stable Event Structures

• Autorzy: Andreeva M.V. , Virbitskaite I.B.
• Języki publikacji: EN

Abstrakty

EN

The intention of the paper is to develop a framework for weak observational equivalences in the setting of a real-time partial order model. In particular, we introduce a family of equivalences of linear time - branching time spectrum based on interleaving, causal tree and partial order semantics, in the setting of a dense time extension of stable event structures with internal actions. We study the relationships between the equivalences showing, on one hand, the discriminating power of the approaches of the spectrum and, on the other hand, the coincidence of some semantics in a concrete approach. Furthermore, when dealing with particular subclasses of the model under consideration, there is no difference between more concrete and more abstract observations.

Słowa kluczowe

EN

real-time system; comparative concurrency semantics; observational equivalences; timed event structures

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 72, nr 1-3
• Strony: 1--19
• Opis fizyczny: bibliogr. 33 poz.

Twórcy

autor

Andreeva M.V.

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,

Bibliografia

• [1] L. ACETO. History preserving, causal and mixed-ordering equivalence over stable event structures Fundamenta Informaticae 17(4) (1992) 319-331.
• [2] L. ACETO, R. DE NICOLA, A. FANTECHI. Testing Equivalences for Event Structures. Lecture Notes in Computer Science 280 (1987) 1-20.
• [3] L. ACETO, D. MURPHI. Timing and causality in process algebra. Acta Informatica 33(4), 1996, 317-350.
• [4] R. ALUR, D. DILL. The theory of timed automata. Theoretical Computer Science 126 (1994) 183-235.
• [5] R. ALUR, T.A. HENZINGER. Logics and models of real time: a survey. Lecture Notes in Computer Science 600 (1992) 74-106.
• [6] M.V. ANDREEVA, I.B. VIRBITSKAITE. Timed equivalences for timed event structures. Lecture Notes in Computer Science 3606 (2005) 16-25.
• [7] C. BAIER, J.-P. KATOEN, D. LATELLA. Metric semantics for true concurrent real time. In Proc. 25th Int. Colloquium, ICALP'98, Aalborg, Denmark, 1998, 568-579.
• [8] J. BENGTSSON, W. YI. Timed Automata: Semantics, Algorithms and Tools. Lecture Notes in Computer Science 3098 (2004) 87-124.
• [9] K. Č ERĀNS. Decidability of bisimulation equivalences for parallel timer processes. Lecture Notes in Computer Science 663 (1993) 302-315.
• [10] PH. DARONDEAU, P. DEGANO. Causal Trees: Interleaving + Causality. Lecture Notes in Computer Science 469 (1990) 239-255.
• [11] PH. DARONDEAU, P. DEGANO. Refinement of actions in event structures and causal trees. Theoretical Computer Science 118 (1993) 21-48.
• [12] R. DE NICOLA, M. HENNESSY. Testing Equivalence for Processes. Theoretical Computer Science 34 (1984) 83-133.
• [13] J. ENGELFRIET. Determinacy → (observation equivalence = trace equivalence). Theoretical Computer Science 36 (1985) 21-25.
• [14] M. FIORE, G.L. CATTANI, G. WINSKEL. Weak bisimulation and open maps. In Proc. LICS'99, 1999, 214-225.
• [15] R.J. VAN GLABBEEK. What is branching time semantics and why to use it? Bulletin of the EATCS 53 (1994) 191-198.
• [16] R.J. VAN GLABBEEK. Handbook of Process Algebras, chapter The linear time - branching time spectrum I: The Semantics of Concrete, Sequential Processes. Elsevier (2001) 3-99.
• [17] R.J. VAN GLABBEEK, U. GOLTZ. Refinement of actions and equivalence notions for concurrent systems. Acta Informatica 37 (2001) 229-327.
• [18] R.J. VAN GLABBEEK, G.D. PLOTKIN. Event Structures for Resolvable Conflict. Lecture Notes in Computer Science 3153 (2004) 550-561.
• [19] U. GOLTZ, H. WEHRHEIM. Causal testing. Lecture Notes in Computer Science 1113 (1996) 394-406.
• [20] T.A. HENZINGER, Z. MANNA, A. PNUELI. Timed transition systems. Lecture Notes in Computer Science 600, 1991, 226-251.
• [21] C.A.R. HOARE Communicating sequential processes. Prentice-Hall, London (1985).
• [22] P.W. HOOGERS, H.C.M. KLEIJN, P.S. THIAGARAJAN. An event structure semantics for general Petri net. Theoretical Computer Science 153 (1996) 129-170.
• [23] A. MAGGIOLO-SCHETTINI, J. WINKOWSKI. Towards an algebra for timed behaviours. Theoretical Computer Science 103, 1992, 335-363.
• [24] R. MILNER. A calculus of communicating systems. Lecture Notes in Computer Science 92 (1980).
• [25] D. MURPHY. Testing, betting and timed true concurrency. Lecture Notes in Computer Science 527 (1991) 439-454.
• [26] M. NIELSEN, G. WINSKEL. Petri nets and bisimulations. Theoretical Computer Science 153(1-2) (1996) 211-244.
• [27] D. PARK Concurrency and automata on infinite sequences. Lecture Notes in Computer Science 104 (1981) 167-183.
• [28] JAN J. M.M. RUTTEN. Universal coalgebra: a theory of systems. Theoretical Computer Science 249 (2000) 3-80.
• [29] B. STEFFEN, C. WEISE. Deciding testing equivalence for real-time processes with dense time. Lecture Notes in Computer Science 711 (1993) 703-713.
• [30] F.W. VAANDRAGER. An explicit representation of equivalence classes of the history preserving bisimulation. Manuscript, CWI-Amsterdam, 1989.
• [31] I.B. VIRBITSKAITE. N.S. GRIBOVSKAYA. Open maps and observational equivalences for timed partial order models. Fundamenta Informaticae 60(1-4) (2004) 383-399.
• [32] C. WEISE, D. LENZKES. Efficient scaling-invariant checking of timed bisimulation. Lecture Notes in Computer Science 1200 (1997) 176-188.
• [33] G. WINSKEL. Event structures. Lecture Notes in Computer Science 255 (1987) 325-392.