# Bisimulation on speed: Lower time bounds

RAIRO - Theoretical Informatics and Applications (2010)

- Volume: 39, Issue: 3, page 587-618
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topLüttgen, Gerald, and Vogler, Walter. "Bisimulation on speed: Lower time bounds." RAIRO - Theoretical Informatics and Applications 39.3 (2010): 587-618. <http://eudml.org/doc/92779>.

@article{Lüttgen2010,

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.
},

author = {Lüttgen, Gerald, Vogler, Walter},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {Asynchronous systems; timed process algebra; lower time bounds;
faster-than relation; Moller-Tofts preorder; bisimulation.; MT-preorder; faster-than preorder; axiomatization; precongruence},

language = {eng},

month = {3},

number = {3},

pages = {587-618},

publisher = {EDP Sciences},

title = {Bisimulation on speed: Lower time bounds},

url = {http://eudml.org/doc/92779},

volume = {39},

year = {2010},

}

TY - JOUR

AU - Lüttgen, Gerald

AU - Vogler, Walter

TI - Bisimulation on speed: Lower time bounds

JO - RAIRO - Theoretical Informatics and Applications

DA - 2010/3//

PB - EDP Sciences

VL - 39

IS - 3

SP - 587

EP - 618

AB -
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.

LA - eng

KW - Asynchronous systems; timed process algebra; lower time bounds;
faster-than relation; Moller-Tofts preorder; bisimulation.; MT-preorder; faster-than preorder; axiomatization; precongruence

UR - http://eudml.org/doc/92779

ER -

## References

top- 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. Zbl0974.68121
- L. Aceto and D. Murphy, Timing and causality in process algebra. Acta Inform.33 (1996) 317–350. Zbl0858.68036
- R. Alur and D. Dill, A theory of timed automata. TCS126 (1994) 183–235. Zbl0803.68071
- S. Arun-Kumar and M.C.B. Hennessy, An efficiency preorder for processes. Acta Inform.29 (1992) 737–760. Zbl0790.68039
- S. Arun-Kumar and V. Natarajan, Conformance: A precongruence close to bisimilarity, in STRICT '95, Workshops in Comp., Springer-Verlag (1995) 55–68.
- E. Badouel and P. Darondeau, On guarded recursion. TCS82 (1991) 403–408. Zbl0728.68079
- 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. Zbl1006.68100
- J.A. Bergstra, A. Ponse and S.A. Smolka, editors, Handbook of Process Algebra. Elsevier Science (2001). Zbl0971.00006
- 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.
- R. Cleaveland and S. Sims, The NCSU Concurrency Workbench, in CAV '96, Springer-Verlag. Lect. Notes Comput. Sci.1102 (1996) 394–397.
- F. Corradini, R. Gorrieri, and M. Roccetti, Performance preorder and competitive equivalence. Acta Inform.34 (1997) 805–835. Zbl0878.68081
- F. Corradini, W. Vogler and L. Jenner, Comparing the worst-case efficiency of asynchronous systems with PAFAS. Acta Inform.38 (2002) 735–792. Zbl1034.68047
- R. De Nicola and M.C.B. Hennessy, Testing equivalences for processes. TCS34 (1984) 83–133. Zbl0985.68518
- R. Gorrieri, M. Roccetti and E. Stancampiano, A theory of processes with durational actions. TCS140 (1995) 73–94. Zbl0874.68113
- M.C.B. Hennessy and T. Regan, A process algebra for timed systems. Inform. Comp.117 (1995) 221–239. Zbl0826.68068
- C.A.R. Hoare, Communicating Sequential Processes. Prentice Hall (1985). Zbl0637.68007
- L. Jenner and W. Vogler, Comparing the efficiency of asynchronous systems, in ARTS '99, Springer-Verlag. Lect. Notes Comput. Sci.1601 (1999) 172–191.
- L. Jenner and W. Vogler, Fast asynchronous systems in dense time. TCS254 (2001) 379–422. Zbl0974.68128
- G. Lüttgen and W. Vogler, Bisimulation on speed: Lower time bounds, in FOSSACS 2004, Springer-Verlag. Lect. Notes Comput. Sci. (2004). Zbl1126.68505
- R. Milner, Communication and Concurrency. Prentice Hall (1989).
- F. Moller and C. Tofts, A temporal calculus of communicating systems, in CONCUR '90, Springer-Verlag. Lect. Notes Comput. Sci.458 (1990) 401–415.
- F. Moller and C. Tofts, Relating processes with respect to speed, in CONCUR '91, Springer-Verlag. Lect. Notes Comput. Sci.527 (1991) 424–438.
- V. Natarajan and R. Cleaveland, An algebraic theory of process efficiency, in LICS '96, IEEE, Computer Society Press (1996) 63–72.
- S. Schneider, An operational semantics for timed CSP. Inform. Comp.116 (1995) 193–213. Zbl0827.68069
- W. Vogler, Faster asynchronous systems. Inform. Comput.184 (2003) 311–342. Zbl1054.68097

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.