Characteristic formulae for timed automata
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Volume 34 (2000) no. 6, p. 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},
     publisher = {EDP-Sciences},
     volume = {34},
     number = {6},
     year = {2000},
     pages = {565-584},
     zbl = {0974.68121},
     mrnumber = {1844719},
     language = {en},
     url = {http://www.numdam.org/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, Volume 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 1731230 | Zbl 0955.68079

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

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

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

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

[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 968903 | Zbl 0677.03011

[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 663750 | Zbl 0546.68014

[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 1129901 | Zbl 0769.68024

[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 0772.68038

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

[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 840349 | Zbl 0591.68031

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

[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 426487 | Zbl 0329.68016

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

[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 1467280 | Zbl 1193.03069

[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 1798628 | Zbl 0961.68090

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

[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 0683.68008

[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 0457.68049

[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 1271233 | Zbl 0804.68097

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

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