EDP Sciences Journals List
Home Document
Subscriber Authentication Point
Issue RAIRO-Theor. Inf. Appl.
Volume 39, Number 3, July-September 2005
Foundations of Software Science and Computer Structures (FOSSACS'04)
Page(s) 587 - 618
DOI 10.1051/ita:2005030

Theoret. Informatics Appl. 39, 587-618 (2005)
DOI: 10.1051/ita:2005030

Bisimulation on speed: Lower time bounds

Gerald Lüttgen1 and Walter Vogler2

1  Department of Computer Science, The University of York, York YO10 5DD, UK; gerald.luettgen@cs.york.ac.uk
2  Institut für Informatik, Universität Augsburg, 86135 Augsburg, Germany; walter.vogler@informatik.uni-augsburg.de


Abstract
More than a decade ago, Moller and Tofts published their seminal work on relating processes, which are annotated with lower time bounds, with respect to speed. Their paper has left open many questions regarding the semantic theory for the 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, a convincing intuitive justification of the MT-preorder, and the abstraction from internal computation. This article solves these difficulties by developing and employing a novel commutation lemma relating the sequencing of action and clock transitions in discrete-time process algebra. 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.


Mathematics Subject Classification. 68Q85

Key words: Asynchronous systems -- timed process algebra -- lower time bounds -- faster-than relation -- Moller-Tofts preorder -- bisimulation.


© EDP Sciences 2005


What is OpenURL?

The OpenURL standard is a protocol for transmission of metadata describing the resource that you wish to access. An OpenURL link contains article metadata and directs it to the OpenURL server of your choice. The OpenURL server can provide access to the resource and also offer complementary services (specific search engine, export of references...). The OpenURL link can be generated by different means.
  • If your librarian has set up your subscription with an OpenURL resolver, OpenURL links appear automatically on the abstract pages.
  • You can define your own OpenURL resolver with your EDPS Account. In this case your choice will be given priority over that of your library.
  • You can use an add-on for your browser (Firefox or I.E.) to display OpenURL links on a page (see http://www.openly.com/openurlref/). You should disable this module if you wish to use the OpenURL server that you or your library have defined.