@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},
volume = {34},
year = {2000},
pages = {565-584},
mrnumber = {1844719},
zbl = {0974.68121},
language = {en},
url = {http://dml.mathdoc.fr/item/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) pp. 565-584. http://gdmltest.u-ga.fr/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 1731230 | Zbl 0955.68079
[2] and , A theory of timed automata. Theoret. Comput. Sci. 126 (1994) 183-235. (Fundamental Study). | MR 1271580 | Zbl 0803.68071
[3] and , An efficiency preorder for processes. Acta Inform. 29 (1992) 737-760. | MR 1202066 | Zbl 0790.68039
[4] and , in Proc. CONCUR 90, Amsterdam. Springer-Verlag, Lecture Notes in Comput. Sci. 458 (1990). | MR 1082153 | Zbl 0746.68005
[5] , and , Bisimulation can't be traced. J. Assoc. Comput. Mach. 42 (1995) 232-268. | MR 1370372 | Zbl 0886.68027
[6] , and , Characterizing finite Kripke structures in propositional temporal logic. Theoret. Comput. Sci. 59 (1988) 115-131. | MR 968903 | Zbl 0677.03011
[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 663750 | Zbl 0546.68014
[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 1129901 | Zbl 0769.68024
[10] , A linear-time model-checking algorithm for the alternation-free modal μ-calculus. Formal Methods in Systems Design 2 (1993) 121-147. | Zbl 0772.68038
[11] , Determinacy → (observation equivalence = trace equivalence). Theoret. Comput. Sci. 36 (1985) 21-25. | MR 792638 | Zbl 0571.68018
[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 840349 | Zbl 0591.68031
[14] and , Algebraic laws for nondeterminism and concurrency. J. Assoc. Comput. Mach. 32 (1985) 137-161. | MR 832336 | Zbl 0629.68021
[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 426487 | Zbl 0329.68016
[17] , Results on the propositional mu-calculus. Theoret. Comput. Sci. 27 (1983) 333-354. | MR 731069 | Zbl 0553.03007
[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 1467280 | Zbl 1193.03069
[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 1798628 | Zbl 0961.68090
[21] and , Bisimulation through probabilistic testing. Inform. and Comput. 94 (1991) 1-28. | MR 1123153 | Zbl 0756.68035
[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 0683.68008
[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 0457.68049
[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 1271233 | Zbl 0804.68097
[28] , A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5 (1955) 285-309. | MR 74376 | Zbl 0064.26004
[29] , Real-time behaviour of asynchronous agents, in Baeten and Klop [4], pp. 502-520. | MR 1082181