Abstract
Coinductive definitions of semantics based on bisimulations have rather pleasant properties and are simple to use. In order to get coinductive characterisations of those semantic equivalences that are weaker than strong bisimulation we use a variant of the bisimulation up-to technique in which we allow the use of a given preorder relation. We prove that under some technical conditions our bisimulations up-to characterise the kernel of the given preorder. It is remarkable that the adequate orientation of the ordering relation is crucial to get this result. As a corollary, we get nice coinductive characterisations of all the axiomatic semantic equivalences in Van Glabbeek’s spectrum. Although we first prove our results for finite processes, reasoning by induction, then we see, by using continuity arguments, that they are also valid for infinite (finitary) processes.
Partially supported by the projects TERMAS TIC2003-07848-C02-01, MIDAS TIC2003-01000, PAC-03-001 and MRTN-CT-2003-505121/TAROT.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Boreale, M., Gadducci, F.: Denotational testing semantics in coinductive form. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 279–289. Springer, Heidelberg (2003)
Cleaveland, R., Hennessy, M.: Testing equivalence as a bisimulation equivalence. Formal Aspects of Computing 3, 1–21 (1992)
Cleaveland, R., Smolka, S.A.: Strategic directions in concurrency research. ACM Computing Surveys 28(4), 607–625 (1996)
de Frutos-Escrig, D., Gregorio-Rodríguez, C.: Semantics equivalences defined with global bisimulations. Annual meeting of the IFIP Working Group 2.2, Bertinoro, Italy (September 2004)
de Frutos-Escrig, D., López, N., Núñez, M.: Global timed bisimulation: An introduction. In: Formal Methods for Protocol Engineering and Distributed Systems, FORTE XII / PSTV XIX, pp. 401–416. Kluwer Academic Publishers, Dordrecht (1999)
Gardiner, P.: Power simulation and its relation to traces and failures refinement. Theoretical Computer Science 309, 157–176 (2003)
van Glabbeek, R.J.: The Linear Time – Branching Time Spectrum I: The Semantics of Concrete, Sequential Processes. In: Handbook of Process Algebra, pp. 3–99. Elsevier, Amsterdam (2001)
Jacobs, B.: Trace semantics for coalgebras. In: CMCS 2004: 7th International Workshop on Coalgebraic Methods in Computer Science. Electronic Notes in Theoretical Computer Science, vol. 106. Elsevier, Amsterdam (2004)
Jacobs, B., Hughes, J.: Simulations in coalgebra. In: CMCS 2003: 6th International Workshop on Coalgebraic Methods in Computer Science, Electronic Notes in Theoretical Computer Science, vol. 82. Elsevier, Amsterdam (2003)
Klin, B.: A coalgebraic approach to process equivalence and a coinductive principle for traces. In: CMCS 2004: 7th International Workshop on Coalgebraic Methods in Computer Science. Electronic Notes in Theoretial Computer, vol. 106. Springer, Heidelberg (1981)
Kučera, A., Mayr, R.: Why is simulation harder than bisimulation? In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 594–610. Springer, Heidelberg (2002)
Kucera, A., Mayr, R.: Simulation preorder over simple process algebra. Information and Computation 173(2), 184–198 (2002)
Klin, B., Sobocinski, P.: Syntactic formats for free. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 72–86. Springer, Heidelberg (2003)
Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)
David, M.R.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)
Plotkin, G.D.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University (1981)
Rutten, J.J.M.M.: Behavioural differential equations: a coinductive calculus of streams, automata, and power series. Theoretical Computer Science 308(1-3), 1–53 (2003)
Sangiorgi, D.: On the bisimulation proof method. Journal of Mathematical Structures in Computer Science 8(5), 447–479 (1998)
Sangiorgi, D., Milner, R.: The problem of “Weak Bisimulation up to”. In: Cleveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 32–46. Springer, Heidelberg (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Frutos Escrig, D., Rodríguez, C.G. (2005). Bisimulations Up-to for the Linear Time Branching Time Spectrum. In: Abadi, M., de Alfaro, L. (eds) CONCUR 2005 – Concurrency Theory. CONCUR 2005. Lecture Notes in Computer Science, vol 3653. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11539452_23
Download citation
DOI: https://doi.org/10.1007/11539452_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28309-6
Online ISBN: 978-3-540-31934-4
eBook Packages: Computer ScienceComputer Science (R0)