RT Book, Section
T1 Bisimulations Up-to for the Linear Time Branching Time Spectrum
A1 Frutos Escrig, David De
A1 Gregorio Rodríguez, Carlos
A2 Abadi, Martín
A2 De Alfaro, Luca
AB 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.
PB Springer
SN 978-3-540-28309-6
YR 2005
FD 2005
LK https://hdl.handle.net/20.500.14352/53218
UL https://hdl.handle.net/20.500.14352/53218
LA eng
NO Frutos Escrig, D. & Gregorio Rodríguez, C. «Bisimulations Up-to for the Linear Time Branching Time Spectrum». CONCUR 2005 – Concurrency Theory, editado por Martín Abadi y Luca De Alfaro, vol. 3653, Springer Berlin Heidelberg, 2005, pp. 278-92. DOI.org (Crossref), https://doi.org/10.1007/11539452_23.
DS Docta Complutense
RD 7 abr 2025