Bisimulation on speed : lower time bounds

Gerald Lüttgen; Walter Vogler

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2005)

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

Abstract

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

How to cite

top

Lüttgen, Gerald, and Vogler, Walter. "Bisimulation on speed : lower time bounds." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 39.3 (2005): 587-618. <http://eudml.org/doc/245836>.

@article{Lüttgen2005,
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 - Informatique Théorique et 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},
number = {3},
pages = {587-618},
publisher = {EDP-Sciences},
title = {Bisimulation on speed : lower time bounds},
url = {http://eudml.org/doc/245836},
volume = {39},
year = {2005},
}

TY - JOUR
AU - Lüttgen, Gerald
AU - Vogler, Walter
TI - Bisimulation on speed : lower time bounds
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 2005
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/245836
ER -

References

top
  1. [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. Zbl0974.68121
  2. [2] L. Aceto and D. Murphy, Timing and causality in process algebra. Acta Inform. 33 (1996) 317–350. Zbl0858.68036
  3. [3] R. Alur and D. Dill, A theory of timed automata. TCS 126 (1994) 183–235. Zbl0803.68071
  4. [4] S. Arun-Kumar and M.C.B. Hennessy, An efficiency preorder for processes. Acta Inform. 29 (1992) 737–760. Zbl0790.68039
  5. [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. [6] E. Badouel and P. Darondeau, On guarded recursion. TCS 82 (1991) 403–408. Zbl0728.68079
  7. [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. Zbl1006.68100
  8. [8] J.A. Bergstra, A. Ponse and S.A. Smolka, editors, Handbook of Process Algebra. Elsevier Science (2001). Zbl0971.00006MR1843380
  9. [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. [10] R. Cleaveland and S. Sims, The NCSU Concurrency Workbench, in CAV ’96, Springer-Verlag. Lect. Notes Comput. Sci. 1102 (1996) 394–397. 
  11. [11] F. Corradini, R. Gorrieri, and M. Roccetti, Performance preorder and competitive equivalence. Acta Inform. 34 (1997) 805–835. Zbl0878.68081
  12. [12] 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
  13. [13] R. De Nicola and M.C.B. Hennessy, Testing equivalences for processes. TCS 34 (1984) 83–133. Zbl0985.68518
  14. [14] R. Gorrieri, M. Roccetti and E. Stancampiano, A theory of processes with durational actions. TCS 140 (1995) 73–94. Zbl0874.68113
  15. [15] M.C.B. Hennessy and T. Regan, A process algebra for timed systems. Inform. Comp. 117 (1995) 221–239. Zbl0826.68068
  16. [16] C.A.R. Hoare, Communicating Sequential Processes. Prentice Hall (1985). Zbl0637.68007MR805324
  17. [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. [18] L. Jenner and W. Vogler, Fast asynchronous systems in dense time. TCS 254 (2001) 379–422. Zbl0974.68128
  19. [19] G. Lüttgen and W. Vogler, Bisimulation on speed: Lower time bounds, in FOSSACS 2004, Springer-Verlag. Lect. Notes Comput. Sci. (2004). Zbl1126.68505MR2147119
  20. [20] R. Milner, Communication and Concurrency. Prentice Hall (1989). Zbl0683.68008
  21. [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. [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. [23] V. Natarajan and R. Cleaveland, An algebraic theory of process efficiency, in LICS ’96, IEEE, Computer Society Press (1996) 63–72. 
  24. [24] S. Schneider, An operational semantics for timed CSP. Inform. Comp. 116 (1995) 193–213. Zbl0827.68069
  25. [25] W. Vogler, Faster asynchronous systems. Inform. Comput. 184 (2003) 311–342. Zbl1054.68097

NotesEmbed ?

top

You must be logged in to post comments.

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.