Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aceto, L., Ingólfsdóttir, A., Pedersen, M.L., Poulsen, J.: Characteristic formulae for timed automata. RAIRO, Theoretical Informatics and Applications 34, 565–584 (2000)
Aceto, L., Murphy, D.: Timing and causality in process algebra. Acta Inform. 33(4), 317–350 (1996)
Arun-Kumar, S., Hennessy, M.C.B.: An efficiency preorder for processes. Acta Inform. 29(8), 737–760 (1992)
Arun-Kumar, S., Natarajan, V.: Conformance: A precongruence close to bisimilarity. In: STRICT 1995, Workshops in Comp. pp.55–68. Springer, Heidelberg,(1995)
Badouel, E., Darondeau, P.: On guarded recursion. TCS 82(2), 403–408 (1991)
Baeten, J.C.M., Middelburg, C.A.: Process algebra with timing: Real time and discrete time. In: Bergstra, et al. (eds.) [7], ch. 10, pp. 627–684.
Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier Science, Amsterdam (2001)
Cleaveland, R., Lüttgen, G., Mendler, M.: An algebraic theory of multiple clocks. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 166–180. Springer, Heidelberg (1997)
Cleaveland, R., Sims, S.: The NCSU Concurrency Workbench. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 394–397. Springer, Heidelberg (1996)
Corradini, F., Gorrieri, R., Roccetti, M.: Performance preorder and competitive equivalence. Acta Inform. 34(11), 805–835 (1997)
Corradini, F., Vogler, W., Jenner, L.: Comparing the worst-case efficiency of asynchronous systems with PAFAS. Acta Informatica 38, 735–792 (2002)
De Nicola, R., Hennessy, M.C.B.: Testing equivalences for processes. TCS 34(1-2), 83–133 (1984)
Gorrieri, R., Roccetti, M., Stancampiano, E.: A theory of processes with durational actions. TCS 140(1), 73–94 (1995)
Hennessy, M.C.B., Regan, T.: A process algebra for timed systems. Inform. and Comp. 117(2), 221–239 (1995)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
Jenner, L., Vogler, W.: Fast asynchronous systems in dense time. TCS 254(1-2), 379–422 (2001)
Lüttgen, G., Vogler, W.: A faster-than relation for asynchronous processes. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 262–276. Springer, Heidelberg (2001); Full version to appear in Inform. and Comp. under the title Bisimulation on Speed: Worst–Case Efficiency
Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)
Moller, F., Tofts, C.: A temporal calculus of communicating systems. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 401–415. Springer, Heidelberg (1990)
Moller, F., Tofts, C.: Relating processes with respect to speed. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol. 527, pp. 424–438. Springer, Heidelberg (1991)
Natarajan, V., Cleaveland, R.: An algebraic theory of process efficiency. In: LICS 1996, pp. 63–72. IEEE Computer Society Press, Los Alamitos (1996)
Schneider, S.: An operational semantics for timed CSP. Inform. and Comp. 116(2), 193–213 (1995)
Vogler, W.: Faster asynchronous systems. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 299–312. Springer, Heidelberg (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lüttgen, G., Vogler, W. (2004). Bisimulation on Speed: Lower Time Bounds. In: Walukiewicz, I. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2004. Lecture Notes in Computer Science, vol 2987. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24727-2_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-24727-2_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21298-0
Online ISBN: 978-3-540-24727-2
eBook Packages: Springer Book Archive