Bisimulation on speed : lower time bounds
Lüttgen, Gerald ; Vogler, Walter
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 39 (2005), p. 587-618 / Harvested from Numdam

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.

Publié le : 2005-01-01
DOI : https://doi.org/10.1051/ita:2005030
Classification:  68Q85
@article{ITA_2005__39_3_587_0,
     author = {L\"uttgen, Gerald and Vogler, Walter},
     title = {Bisimulation on speed : lower time bounds},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     volume = {39},
     year = {2005},
     pages = {587-618},
     doi = {10.1051/ita:2005030},
     mrnumber = {2157048},
     zbl = {1077.68064},
     language = {en},
     url = {http://dml.mathdoc.fr/item/ITA_2005__39_3_587_0}
}
Lüttgen, Gerald; Vogler, Walter. Bisimulation on speed : lower time bounds. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 39 (2005) pp. 587-618. doi : 10.1051/ita:2005030. http://gdmltest.u-ga.fr/item/ITA_2005__39_3_587_0/

[1] L. Aceto, A. Ingólfsdóttir, M.L. Pedersen, and J. Poulsen, Characteristic formulae for timed automata. RAIRO-Theor. Inform. Appl. 34 (2000) 565-584. | Numdam | Zbl 0974.68121

[2] L. Aceto and D. Murphy, Timing and causality in process algebra. Acta Inform. 33 (1996) 317-350. | Zbl 0858.68036

[3] R. Alur and D. Dill, A theory of timed automata. TCS 126 (1994) 183-235. | Zbl 0803.68071

[4] S. Arun-Kumar and M.C.B. Hennessy, An efficiency preorder for processes. Acta Inform. 29 (1992) 737-760. | Zbl 0790.68039

[5] S. Arun-Kumar and V. Natarajan, Conformance: A precongruence close to bisimilarity, in STRICT '95, Workshops in Comp., Springer-Verlag (1995) 55-68.

[6] E. Badouel and P. Darondeau, On guarded recursion. TCS 82 (1991) 403-408. | Zbl 0728.68079

[7] J.C.M. Baeten and C.A. Middelburg, Process algebra with timing: Real time and discrete time, in Bergstra et al. [8], Chap. 10, 627-684. | Zbl 1006.68100

[8] J.A. Bergstra, A. Ponse and S.A. Smolka, editors, Handbook of Process Algebra. Elsevier Science (2001). | MR 1843380 | Zbl 0971.00006

[9] R. Cleaveland, G. Lüttgen and M. Mendler, An algebraic theory of multiple clocks, in CONCUR '97, Springer-Verlag. Lect. Notes Comput. Sci. 1243 (1997) 166-180.

[10] R. Cleaveland and S. Sims, The NCSU Concurrency Workbench, in CAV '96, Springer-Verlag. Lect. Notes Comput. Sci. 1102 (1996) 394-397.

[11] F. Corradini, R. Gorrieri, and M. Roccetti, Performance preorder and competitive equivalence. Acta Inform. 34 (1997) 805-835. | Zbl 0878.68081

[12] F. Corradini, W. Vogler and L. Jenner, Comparing the worst-case efficiency of asynchronous systems with PAFAS. Acta Inform. 38 (2002) 735-792. | Zbl 1034.68047

[13] R. De Nicola and M.C.B. Hennessy, Testing equivalences for processes. TCS 34 (1984) 83-133. | Zbl 0985.68518

[14] R. Gorrieri, M. Roccetti and E. Stancampiano, A theory of processes with durational actions. TCS 140 (1995) 73-94. | Zbl 0874.68113

[15] M.C.B. Hennessy and T. Regan, A process algebra for timed systems. Inform. Comp. 117 (1995) 221-239. | Zbl 0826.68068

[16] C.A.R. Hoare, Communicating Sequential Processes. Prentice Hall (1985). | MR 805324 | Zbl 0637.68007

[17] L. Jenner and W. Vogler, Comparing the efficiency of asynchronous systems, in ARTS '99, Springer-Verlag. Lect. Notes Comput. Sci. 1601 (1999) 172-191.

[18] L. Jenner and W. Vogler, Fast asynchronous systems in dense time. TCS 254 (2001) 379-422. | Zbl 0974.68128

[19] G. Lüttgen and W. Vogler, Bisimulation on speed: Lower time bounds, in FOSSACS 2004, Springer-Verlag. Lect. Notes Comput. Sci. (2004). | MR 2147119 | Zbl 1126.68505

[20] R. Milner, Communication and Concurrency. Prentice Hall (1989). | Zbl 0683.68008

[21] F. Moller and C. Tofts, A temporal calculus of communicating systems, in CONCUR '90, Springer-Verlag. Lect. Notes Comput. Sci. 458 (1990) 401-415.

[22] F. Moller and C. Tofts, Relating processes with respect to speed, in CONCUR '91, Springer-Verlag. Lect. Notes Comput. Sci. 527 (1991) 424-438.

[23] V. Natarajan and R. Cleaveland, An algebraic theory of process efficiency, in LICS '96, IEEE, Computer Society Press (1996) 63-72.

[24] S. Schneider, An operational semantics for timed CSP. Inform. Comp. 116 (1995) 193-213. | Zbl 0827.68069

[25] W. Vogler, Faster asynchronous systems. Inform. Comput. 184 (2003) 311-342. | Zbl 1054.68097