@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] and , 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] and , A theory of timed automata. Theoret. Comput. Sci. 126 (1994) 183-235. (Fundamental Study). | MR | Zbl
[3] and , An efficiency preorder for processes. Acta Inform. 29 (1992) 737-760. | MR | Zbl
[4] and , in Proc. CONCUR 90, Amsterdam. Springer-Verlag, Lecture Notes in Comput. Sci. 458 (1990). | MR | Zbl
[5] , and , Bisimulation can't be traced. J. Assoc. Comput. Mach. 42 (1995) 232-268. | MR | Zbl
[6] , and , Characterizing finite Kripke structures in propositional temporal logic. Theoret. Comput. Sci. 59 (1988) 115-131. | MR | Zbl
[7] and , 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] , and , Model Checking. MIT Press (2000).
[9] and , 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] , A linear-time model-checking algorithm for the alternation-free modal μ-calculus. Formal Methods in Systems Design 2 (1993) 121-147. | Zbl
[11] , Determinacy → (observation equivalence = trace equivalence). Theoret. Comput. Sci. 36 (1985) 21-25. | MR | Zbl
[12] , The linear time - branching time spectrum, in Baeten and Klop [4], pp. 278-297.
[13] and , A modal characterization of observational congruence on finite terms of CCS. Inform. and Control 68 (1986) 125-145. | MR | Zbl
[14] and , Algebraic laws for nondeterminism and concurrency. J. Assoc. Comput. Mach. 32 (1985) 137-161. | MR | Zbl
[15] , and , Fra Hennessy-Milner logik til CCS-processer. Master's thesis, Department of Computer Science, Aalborg University (1987).
[16] , Formal verification of parallel programs. Comm. ACM 19 (1976) 371-384. | MR | Zbl
[17] , Results on the propositional mu-calculus. Theoret. Comput. Sci. 27 (1983) 333-354. | MR | Zbl
[18] and , 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] , and , 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] and , 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] and , Bisimulation through probabilistic testing. Inform. and Comput. 94 (1991) 1-28. | MR | Zbl
[22] , 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] , Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989). | Zbl
[24] and , 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] , 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] and , Model-checking characteristic formulae - a method for proving timed behavioural relations. Master's thesis, Department of Computer Science, Aalborg University (1999).
[27] and , Characteristic formulae for processes with divergence. Inform. and Comput 110 (1994) 149-163. | MR | Zbl
[28] , A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5 (1955) 285-309. | MR | Zbl
[29] , Real-time behaviour of asynchronous agents, in Baeten and Klop [4], pp. 502-520. | MR
