Characteristic formulae for timed automata
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 34 (2000) no. 6, pp. 565-584.
@article{ITA_2000__34_6_565_0,
     author = {Aceto, Luca and Ing\'olfsd\'ottir, Anna and Pedersen, Mikkel Lykke and Poulsen, Jan},
     title = {Characteristic formulae for timed automata},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {565--584},
     publisher = {EDP-Sciences},
     volume = {34},
     number = {6},
     year = {2000},
     mrnumber = {1844719},
     zbl = {0974.68121},
     language = {en},
     url = {http://www.numdam.org/item/ITA_2000__34_6_565_0/}
}
TY  - JOUR
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
SP  - 565
EP  - 584
VL  - 34
IS  - 6
PB  - EDP-Sciences
UR  - http://www.numdam.org/item/ITA_2000__34_6_565_0/
LA  - en
ID  - ITA_2000__34_6_565_0
ER  - 
%0 Journal Article
%A Aceto, Luca
%A Ingólfsdóttir, Anna
%A Pedersen, Mikkel Lykke
%A Poulsen, Jan
%T Characteristic formulae for timed automata
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2000
%P 565-584
%V 34
%N 6
%I EDP-Sciences
%U http://www.numdam.org/item/ITA_2000__34_6_565_0/
%G en
%F ITA_2000__34_6_565_0
Aceto, Luca; Ingólfsdóttir, Anna; Pedersen, Mikkel Lykke; Poulsen, Jan. Characteristic formulae for timed automata. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 34 (2000) no. 6, pp. 565-584. http://www.numdam.org/item/ITA_2000__34_6_565_0/

[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. | MR | Zbl

[2] R. Alur and D. L. Dill, A theory of timed automata. Theoret. Comput. Sci. 126 (1994) 183-235. (Fundamental Study). | MR | Zbl

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

[4] J. Baeten and J. Klop, in Proc. CONCUR 90, Amsterdam. Springer-Verlag, Lecture Notes in Comput. Sci. 458 (1990). | MR | Zbl

[5] B. Bloom, S. Istrail and A. R. Meyer, Bisimulation can't be traced. J. Assoc. Comput. Mach. 42 (1995) 232-268. | MR | Zbl

[6] M. Browne, E. Clarke and O. Grümberg, Characterizing finite Kripke structures in propositional temporal logic. Theoret. Comput. Sci. 59 (1988) 115-131. | MR | Zbl

[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. | MR | Zbl

[8] E. Clarke, O. Grümberg and D. Peled, Model Checking. MIT Press (2000).

[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. | MR | Zbl

[10] R. Cleaveland, A linear-time model-checking algorithm for the alternation-free modal μ-calculus. Formal Methods in Systems Design 2 (1993) 121-147. | Zbl

[11] J. Engelfriet, Determinacy → (observation equivalence = trace equivalence). Theoret. Comput. Sci. 36 (1985) 21-25. | MR | Zbl

[12] R. J. V. Glabbeek, The linear time - branching time spectrum, in Baeten and Klop [4], pp. 278-297.

[13] S. Graf and J. Sifakis, A modal characterization of observational congruence on finite terms of CCS. Inform. and Control 68 (1986) 125-145. | MR | Zbl

[14] M. Hennessy and R. Milner, Algebraic laws for nondeterminism and concurrency. J. Assoc. Comput. Mach. 32 (1985) 137-161. | MR | Zbl

[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] R. Keller, Formal verification of parallel programs. Comm. ACM 19 (1976) 371-384. | MR | Zbl

[17] D. Kozen, Results on the propositional mu-calculus. Theoret. Comput. Sci. 27 (1983) 333-354. | MR | Zbl

[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] 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. | MR | Zbl

[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. | MR | Zbl

[21] K. G. Larsen and A. Skou, Bisimulation through probabilistic testing. Inform. and Comput. 94 (1991) 1-28. | MR | Zbl

[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] R. Milner, Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989). | Zbl

[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] 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. | Zbl

[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] B. Steffen and A. Ingólfsdóttir, Characteristic formulae for processes with divergence. Inform. and Comput 110 (1994) 149-163. | MR | Zbl

[28] A. Tarski, A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5 (1955) 285-309. | MR | Zbl

[29] Y. Wang, Real-time behaviour of asynchronous agents, in Baeten and Klop [4], pp. 502-520. | MR