From timed automata to logic — and back

1. R. Alur, C. Courcoubetis, and D. Dill. Model-checking for Real-Time Systems. In Proceedings of Logic in Computer Science, pages 414–425. IEEE Computer Society Press, 1990.

   Google Scholar 

2. R. Alur and D. Dill. Automata for Modelling Real-Time Systems. Theoretical Computer Science, 126(2):183–236, April 1994.

   Article  Google Scholar 

3. H.R. Andersen. Model checking and boolean graphs. In Proceedings of ESOP'92, volume 582 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 1992. Springer.

   Google Scholar 

4. A. Arnold and P. Crubille. A linear algorithm to solve fixed-point equations on transition systems. Information Processing Letters, 29, 1988.

   Google Scholar 

5. M. C. Browne, E. M. Clarke, and O. Grümberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59:115–131, 1988.

   Article  Google Scholar 

6. Karlis Cerans. Decidability of bisimulation equivalences for parallel timer processes. In Proc. of CAV'92, volume 663 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 1992. Springer Verlag.

   Google Scholar 

7. E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using Branching Time Temporal Logic. In Proc. Workshop on Logics of Programs, volume 131 of Lecture Notes in Computer Science, pages 52–71, Berlin, 1981. Springer Verlag.

   Google Scholar 

8. E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite state concurrent system using temporal logic. ACM Trans. on Programming Languages and Systems, 8(2):244–263, 1986.

   Google Scholar 

9. R. Cleaveland and B. Steffen. Computing behavioural relations, logically. In Proceedings of 18th International Colloquium on Automata, Languages and Programming, volume 510 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 1991. Springer.

   Google Scholar 

10. E.A. Emerson and C.L Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of Logic in Computer Science, pages 267–278. IEEE Computer Society Press, 1986.

    Google Scholar 

11. F.Moller and C. Tofts. Relating Processes with Respect to Speed. Technical Report ECS-LFCS-91-143, Department of Computer Science, University of Edinburgh, 1991.

    Google Scholar 

12. S. Graf and J. Sifakis. A Modal Characterization of Observational Congruence on Finite Terms of CCS. Information and Control, 68:125–145, 1986.

    Article  Google Scholar 

13. T. A. Henzinger, Z. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In Logic in Computer Science, 1992.

    Google Scholar 

14. U. Holmer, K.G. Larsen, and W. Yi. Decidability of bisimulation equivalence between regular timed processes. In Proceedings of CAV'91, volume 575 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 1992.

    Google Scholar 

15. G.E. Hughes and M.J. Cresswell. An Introduction to Modal Logic. Methuen and Co., 1968.

    Google Scholar 

16. A. Ingolfsdottir and B. Steffen. Characteristic formulae. Information and Computation, 110(1), 1994. To appear.

    Google Scholar 

17. D. Kozen. Results on the propositional mu-calculus. In Proc. of International Colloquium on Algorithms, Languages and Programming 1982, volume 140 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 1982.

    Google Scholar 

18. F. Laroussinie, K. G. Larsen, and C. Weise. From Timed Automata to Logic — and Back. Technical Report RS-95-2, BRICS, 1995. Accessible through WWW: http://www.brics.aau.dk/BRICS.

    Google Scholar 

19. K.G. Larsen and Y. Wang. Time Abstracted Bisimulation: Implicit Specifications and Decidability. In Proceedings of MFPS'93, 1993.

    Google Scholar 

20. R. Milner. Communication and Concurrency, prentice, Englewood Cliffs, 1989.

    Google Scholar 

21. D. Park. Concurrency and automata on infinite sequences. In Proceedings of 5th GI Conference, volume 104 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 1981. Springer.

    Google Scholar 

22. J. P. Queille and J. Sifakis. Specification and verification of concurrent programs in CESAR. In Proc. 5th Internat. Symp. on Programming, volume 137 of Lecture Notes in Computer Science, pages 195–220, Berlin, 1982. Springer Verlag.

    Google Scholar 

23. A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Math., 5, 1955.

    Google Scholar 

24. Liu Xinxin. Specification and Decomposition in Concurrency. PhD thesis, Aalborg University, 1992. R 92-2005.

    Google Scholar 

Download references