Bisimulation on Speed: A Unified Approach

Foundations of Software Science and Computational Structures, FOSSACS 05
Eds.: V. Sassone
Springer 2005, Lect. Notes Comput. Sci. 3441, 79 – 94
Copyright by Springer, Berlin, Heidelberg DOI: 10.1007/b106850

Two process–algebraic approaches have been developed for comparing two bisimulation–equivalent processes with respect to speed: the one of Moller/Tofts equips actions with lower time bounds, while the one by Lüttgen/Vogler considers upper time bounds instead. This paper sheds new light on both approaches by testifying to their close relationship.

We introduce a general, intuitive concept of ldquofaster–thanrdquo, which is formalised by a notion of amortised faster–than preorder. When closing this preorder under all contexts, exactly the two faster–than preorders investigated by Moller/Tofts and Lüttgen/Vogler arise. For processes incorporating both lower and upper time bounds we also show that the largest precongruence contained in the amortised faster–than preorder is not a proper preorder but a timed bisimulation. In the light of this result we systematically investigate under which circumstances the amortised faster–than preorder degrades to an equivalence.