Characteristic formulae for timed automata

 Access to full text

 Full (PDF)

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