Bisimulation on Speed: Lower Time Bounds

Foundations of Software Science and Computational Structures, FOSSACS 04
Ed.: I. Walukiewicz
Springer 2004, Lect. Notes Comput. Sci. 2987, 333 – 347
Copyright by Springer, Berlin, Heidelberg DOI: 10.1007/b95995

More than a decade ago, Moller and Tofts published their seminal work on relating processes that are annotated with lower time bounds, with respect to speed. Their paper has left open many questions concerning the semantic theory for their suggested bisimulation–based faster–than preorder, the MT–preorder, which have not been addressed since. The encountered difficulties concern a general compositionality result, a complete axiom system for finite processes, and a convincing intuitive justification of the MT–preorder.

This paper solves these difficulties by developing and employing novel tools for reasoning in discrete–time process algebra, in particular a general commutation lemma relating the sequencing of action and clock transitions. Most importantly, it is proved that the MT–preorder is fully–abstract with respect to a natural amortized preorder that uses a simple bookkeeping mechanism for deciding whether one process is faster than another. Together these results reveal the intuitive roots of the MT–preorder as a faster–than relation, while testifying to its semantic elegance. This lifts some of the barriers that have so far hampered progress in semantic theories for comparing the speed of processes.