Revisiting Satisfiability and Model-Checking for CTLK with Synchrony and Perfect Recall

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

   Article  MATH  Google Scholar 

2. Dickhöfer, M., Wilke, T.: Timed alternating tree automata: The automata-theoretic solution to the TCTL model checking problem. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 281–290. Springer, Heidelberg (1999)

   Chapter  Google Scholar 

3. Elgaard, J., Klarlund, N., Møller, A.: Mona 1.x: New techniques for ws1s and ws2s. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 516–520. Springer, Heidelberg (1998)

   Chapter  Google Scholar 

4. Elgot, C.C., Rabin, M.O.: Decidability and undecidability of extensions of second (first) order theory of (generalized) successor. Journal of Symbolic Logic 31(2), 169–181 (1966)

   Article  MATH  Google Scholar 

5. Fagin, R., Halpern, J., Vardi, M.: Reasoning about knowledge. The MIT Press, Cambridge (2004)

   MATH  Google Scholar 

6. Halpern, J.Y., Vardi, M.Y.: The complexity of reasoning about knowledge and time: Extended abstract. In: Proceedings of STOC 1986, pp. 304–315 (1986), https://www.cs.rice.edu/~vardi/papers/stoc86r1.pdf.gz

7. Halpern, J.Y., Vardi, M.Y.: The complexity of reasoning about knowledge and time. I. Lower bounds. Journal of Computer System Sciences 38(1), 195–237 (1989)

   Article  MathSciNet  MATH  Google Scholar 

8. Kacprzak, M., Lomuscio, A., Niewiadomski, A., Penczek, W., Raimondi, F., Szreter, M.: Comparing BDD and SAT based techniques for model checking Chaum’s Dining Cryptographers Protocol. Fundamenta Informaticae 72(1-3), 215–234 (2006)

   MathSciNet  MATH  Google Scholar 

9. Lind, D., Marcus, B.: An Introduction to Symbolic Dynamics and Coding. Cambridge University Press, Cambridge (1995)

   Book  MATH  Google Scholar 

10. Lomuscio, A., Raimondi, F.: The complexity of model checking concurrent programs against CTLK specifications. In: Baldoni, M., Endriss, U. (eds.) DALT 2006. LNCS, vol. 4327, pp. 29–42. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

11. Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams. Journal of Applied Logic 5(2), 235–251 (2005)

    Article  MathSciNet  MATH  Google Scholar 

12. Shilov, N.V., Garanina, N.O.: Model checking knowledge and fixpoints. In: Proceedings of FICS 2002, Extended version available as Preprint 98, pp. 25–39. Ershov Institute of Informatics, Novosibirsk (2002)

    Google Scholar 

13. Thomas, W.: Infinite trees and automaton-definable relations over ω-words. Theoretical Computer Science 103(1), 143–159 (1992)

    Article  MathSciNet  MATH  Google Scholar 

14. van Benthem, J., Pacuit, E.: The tree of knowledge in action: Towards a common perspective. In: Governatori, G., Hodkinson, I.M., Venema, Y. (eds.) Proceedings of AiML 2006, pp. 87–106. College Publications (2006)

    Google Scholar 

15. van der Meyden, R.: Common knowledge and update in finite environments. Information and Computation 140(2), 115–157 (1998)

    Article  MathSciNet  MATH  Google Scholar 

16. van der Meyden, R., Shilov, N.V.: Model checking knowledge and time in systems with perfect recall (extended abstract). In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 432–445. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

17. van der Meyden, R., Su, K.: Symbolic model checking the knowledge of the dining cryptographers. In: Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW-17 2004), p. 280. IEEE Computer Society Press, Los Alamitos (2004)

    Chapter  Google Scholar 

Download references