Characteristic formulae for timed automata

Luca Aceto; Anna Ingólfsdóttir; Mikkel Lykke Pedersen; Jan Poulsen

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

  • Volume: 34, Issue: 6, page 565-584
  • ISSN: 0988-3754

How to cite


Aceto, Luca, et al. "Characteristic formulae for timed automata." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 34.6 (2000): 565-584. <>.

author = {Aceto, Luca, Ingólfsdóttir, Anna, Pedersen, Mikkel Lykke, Poulsen, Jan},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {real-time logic; timed bisimulation equivalence},
language = {eng},
number = {6},
pages = {565-584},
publisher = {EDP-Sciences},
title = {Characteristic formulae for timed automata},
url = {},
volume = {34},
year = {2000},

AU - Aceto, Luca
AU - Ingólfsdóttir, Anna
AU - Pedersen, Mikkel Lykke
AU - Poulsen, Jan
TI - Characteristic formulae for timed automata
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 2000
PB - EDP-Sciences
VL - 34
IS - 6
SP - 565
EP - 584
LA - eng
KW - real-time logic; timed bisimulation equivalence
UR -
ER -


  1. [1] L. Aceto and F. Laroussinie, Is your model checker on time? On the complexity of model checking for timed modal logics. Springer-Verlag, Berlin, Math. Foundations of Comput. Sci. 1999 (Szklarska Poreba) (1999) 125-136. Zbl0955.68079MR1731230
  2. [2] R. Alur and D. L. Dill, A theory of timed automata. Theoret. Comput. Sci. 126 (1994) 183-235. (Fundamental Study). Zbl0803.68071MR1271580
  3. [3] S. Arun-Kumar and M. Hennessy, An efficiency preorder for processes. Acta Inform. 29 (1992) 737-760. Zbl0790.68039MR1202066
  4. [4] J. Baeten and J. Klop, in Proc. CONCUR 90, Amsterdam. Springer-Verlag, Lecture Notes in Comput. Sci. 458 (1990). Zbl0746.68005MR1082153
  5. [5] B. Bloom, S. Istrail and A. R. Meyer, Bisimulation can't be traced. J. Assoc. Comput. Mach. 42 (1995) 232-268. Zbl0886.68027MR1370372
  6. [6] M. Browne, E. Clarke and O. Grümberg, Characterizing finite Kripke structures in propositional temporal logic. Theoret. Comput. Sci. 59 (1988) 115-131. Zbl0677.03011MR968903
  7. [7] E. Clarke and E. Emerson, Design and synthesis of synchronization skeletons using branching-time temporal logic, in Proc. of the Workshop on Logic of Programs, Yorktown Heights, edited by D. Kozen. Springer-Verlag, Lecture Notes in Comput. Sci. 131 (1981) 52-71. Zbl0546.68014MR663750
  8. [8] E. Clarke, O. Grümberg and D. Peled, Model Checking. MIT Press (2000). 
  9. [9] R. Cleaveland and B. Steffen, Computing behavioral relations, logically, in ICALP '91: Automata, Languages and Programming, edited by J. L. Albert, B. Monien and M.R. Artalejo. Springer-Verlag, Lecture Notes in Comput. Sci. 510 (1991) 127-138. Zbl0769.68024MR1129901
  10. [10] R. Cleaveland, A linear-time model-checking algorithm for the alternation-free modal μ-calculus. Formal Methods in Systems Design 2 (1993) 121-147. Zbl0772.68038
  11. [11] J. Engelfriet, Determinacy → (observation equivalence = trace equivalence). Theoret. Comput. Sci. 36 (1985) 21-25. Zbl0571.68018MR792638
  12. [12] R. J. V. Glabbeek, The linear time - branching time spectrum, in Baeten and Klop [4], pp. 278-297. 
  13. [13] S. Graf and J. Sifakis, A modal characterization of observational congruence on finite terms of CCS. Inform. and Control 68 (1986) 125-145. Zbl0591.68031MR840349
  14. [14] M. Hennessy and R. Milner, Algebraic laws for nondeterminism and concurrency. J. Assoc. Comput. Mach. 32 (1985) 137-161. Zbl0629.68021MR832336
  15. [15] A. Ingólfsdóttir, J. C. Godskesen and M. Zeeberg, Fra Hennessy-Milner logik til CCS-processer. Master's thesis, Department of Computer Science, Aalborg University (1987). 
  16. [16] R. Keller, Formal verification of parallel programs. Comm. ACM 19 (1976) 371-384. Zbl0329.68016MR426487
  17. [17] D. Kozen, Results on the propositional mu-calculus. Theoret. Comput. Sci. 27 (1983) 333-354. Zbl0553.03007MR731069
  18. [18] F. Laroussinie and K. G. Larsen, CMC: A tool for compositional model-checking of realtime systems, in Proc. IFIP Joint Int. Conf. Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE-PS TV'98). Kluwer Academic Publishers (1998) 439-456. 
  19. [19] F. Laroussinie, K. G. Larsen and C. Weise, From timed automata to logic - and back, in Proc. of the 20th Symposium on Mathematical Foundations of Computer Science. Springer-Verlag, Lecture Notes in Comput. Sci. 969 (1995) 529-540. Zbl1193.03069MR1467280
  20. [20] F. Laroussinie and P. Schnoebelen, The state explosion problem from trace to bisimulation equivalence, in Proc. of the 3rd International Conference on Foundations of Software Science and Computation Structures (FOSSACS'2000). Springer-Verlag, Lecture Notes in Comput. Sci. 1784 (2000) 192-207. Zbl0961.68090MR1798628
  21. [21] K. G. Larsen and A. Skou, Bisimulation through probabilistic testing. Inform. and Comput. 94 (1991) 1-28. Zbl0756.68035MR1123153
  22. [22] R. Milner, An algebraic definition of simulation between programs, in Proc. 2nd Joint Conference on Artificial Intelligence. William Kaufmann (1971) 481-489. Also available as Report No. CS-205, Computer Science Department, Stanford University. 
  23. [23] R. Milner, Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989). Zbl0683.68008
  24. [24] F. Moller and C. Tofts, Relating processes with respect to speed, in CONCUR '91: 2nd International Conference on Concurrency Theory, edited by J.C.M. Baeten and J. F. Groote. Springer-Verlag, Amsterdam, The Netherlands, Lecture Notes in Comput Sci. 527 (1991) 424-438. 
  25. [25] D. Park, Concurrency and automata on infinite sequences, in 5th GI Conference, Karlsruhe, Germany, edited by P. Deussen. Springer-Verlag, Lecture Notes in Comput Sci. 104 (1981) 167-183. Zbl0457.68049
  26. [26] M. L. Pedersen and J. Poulsen, Model-checking characteristic formulae - a method for proving timed behavioural relations. Master's thesis, Department of Computer Science, Aalborg University (1999). 
  27. [27] B. Steffen and A. Ingólfsdóttir, Characteristic formulae for processes with divergence. Inform. and Comput 110 (1994) 149-163. Zbl0804.68097MR1271233
  28. [28] A. Tarski, A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5 (1955) 285-309. Zbl0064.26004MR74376
  29. [29] Y. Wang, Real-time behaviour of asynchronous agents, in Baeten and Klop [4], pp. 502-520. MR1082181

NotesEmbed ?


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.