A Logic for Knowledge, Correctness, and Real Time

1. Hintikka, J.: Knowledge and Belief, An Introduction to the Logic of the Two Notions. Cornell University Press, Ithaca (1962)

   Google Scholar 

2. Aumann, R.J.: Agreeing to disagree. Annals of Statistics 4, 1236–1239 (1976)

   Article  MathSciNet  Google Scholar 

3. Fagin, R., Vardi, M.Y.: Knowledge and implicit knowledge in a distributed environment: Preliminary report. In: Halpern, J.Y. (ed.) TARK: Theoretical Aspects of Reasoning about Knowledge, pp. 187–206. Morgan Kaufmann, San Francisco (1986)

   Chapter  Google Scholar 

4. Halpern, J., Moses, Y.: A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence 54, 319–379 (1992)

   Article  MathSciNet  Google Scholar 

5. van der Hoek, W.: Sytems for knowledge and belief. Journal of Logic and Computation 3, 173–195 (1993)

   Article  MathSciNet  Google Scholar 

6. Halpern, J.Y., Vardi, M.Y.: The complexity of reasoning about knowledge and time. In: ACM Symposium on Theory of Computing (STOC 1986), Baltimore, USA, pp. 304–315. ACM Press, New York (1986)

   Google Scholar 

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

   Article  MathSciNet  Google Scholar 

8. van der Meyden, R., Wong, K.: Complete axiomatizations for reasoning about knowledge and branching time. Studia Logica 75, 93–123 (2003)

   Article  MathSciNet  Google Scholar 

9. Marek, W., Truszczyński, M.: Autoepistemic logic. Journal of the ACM 38, 587–618 (1991)

   Article  MathSciNet  Google Scholar 

10. Moore, R.: Possible-world semantics autoepistemic logic. In: Proceedings of Workshop on Non-Monotonic Reasoning, pp. 344–354. The AAAI Press, Menlo Park (1984)

    Google Scholar 

11. Baltag, A., Moss, L.S., Solecki, S.: The logic of public announcement, common knowledge, and private suspicions. In: Gilboa, I. (ed.) Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge (TARK 1998), pp. 125–132. Morgan Kaufmann, San Francisco (1998)

    Google Scholar 

12. Lomuscio, A., Ryan, M.: An algorithmic approach to knowledge evolution. Artificial Intelligence for Engineering Design, Analysis and Manufacturing (AIEDAM) 13 (1999)

    Google Scholar 

13. Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Knowledge-based programs. Distributed Computing 10, 199–225 (1997)

    Article  Google Scholar 

14. Lomuscio, A., van der Meyden, R., Ryan, M.: Knowledge in multi-agent systems: Initial configurations and broadcast. ACM Transactions of Computational Logic 1 (2000)

    Google Scholar 

15. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1991)

    MATH  Google Scholar 

16. Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)

    Book  Google Scholar 

17. Manna, Z., Pnueli, A.: Completing the temporal picture. In: Selected papers of the 16th international colloquium on Automata, languages, and programming, pp. 97–130. Elsevier Science, Amsterdam (1991)

    MATH  Google Scholar 

18. Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)

    MATH  Google Scholar 

19. Halpern, J., Meyden, R., Vardi, M.Y.: Complete axiomatisations for reasoning about knowledge and time. SIAM Journal on Computing 33, 674–703 (2003)

    Article  Google Scholar 

20. van der Meyden, R.: Axioms for knowledge and time in distributed systems with perfect recall. In: Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, Paris, France, pp. 448–457. IEEE Computer Society Press, Los Alamitos (1994)

    Chapter  Google Scholar 

21. Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Informatica 20, 207–226 (1983)

    Article  MathSciNet  Google Scholar 

22. Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 996–1071. Elsevier Science Publishers, Amsterdam (1990)

    Google Scholar 

23. Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences 30, 1–24 (1985)

    Article  MathSciNet  Google Scholar 

24. Lomuscio, A., Sergot, M.: Deontic interpreted systems. Studia Logica 75, 63–92 (2003)

    Article  MathSciNet  Google Scholar 

25. Lomuscio, A., Sergot, M.: Violation, error recovery, and enforcement in the bit transmission problem. Journal of Applied Logic 1(2), 93–116 (2004)

    Article  MathSciNet  Google Scholar 

26. Alur, R., Dill, D.: Automata for modelling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

27. Dill, D.: Timing assumptions and verification of finite state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

28. Behrmann, G., Larsen, K., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 341–353. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

29. Wang, F.: Efficient data structure of fully symbolic verification of real-time software systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 157–171. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

30. Penczek, W., Woźna, B., Zbrzezny, A.: SAT-based bounded model checking for the universal fragment of TCTL. Technical Report 947, ICS PAS, Ordona 21, 01-237 Warsaw (2002)

    Google Scholar 

31. Penczek, W., Woźna, B., Zbrzezny, A.: Towards bounded model checking for the universal fragment of TCTL. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 265–288. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

32. Seshia, S., Bryant, R.: Unbounded, fully symbolic model checking of timed automata using boolean methods. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 154–166. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

33. Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design 18, 25–68 (2001)

    Article  Google Scholar 

34. Alur, R., Courcoubetis, C., Dill, D.: Model checking in dense real-time. Information and Computation 104, 2–34 (1993)

    Article  MathSciNet  Google Scholar 

35. Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press, Cambridge (2001)

    Book  Google Scholar 

36. Kang, I., Lee, I.: An efficient state space generation for the analysis of real-time systems. In: Proceedings of International Symposium on Software Testing and Analysis (1996)

    Google Scholar 

37. Anderson, S., Kuster-Filipe, J.: Guaranteeing temporal validity with a real-time logic of knowledge. In: Proceedings of the 1st International Workshop on Data Distribution for Real-Time Systems (DDRTS 2003), ICDCS 2003 Workshop, Providence, Rhode Island, USA, pp. 178–183 (2003)

    Google Scholar 

38. Brafman, R.I., Latombe, J.C., Moses, Y., Shoham, Y.: Application of a logic of knowledge to motion planning under uncertainty. Journal of the ACM 44, 633–668 (1997)

    Article  MathSciNet  Google Scholar 

39. Moses, Y., Bloom, B.: Knowledge, timed precedence and clocks. In: Proceedings of the 13th ACM symposium on Principles of Distributed Computing, pp. 274–303. ACM Press, New York (1994)

    Google Scholar 

40. Woźna, B., Lomuscio, A., Penczek, W.: Verification of deontic and epistemic properties of multiagent systems and its application to the bit transmission problem with faults. In: Proceedings of the 2nd Workshop on Logic and Communication in Multi-Agent Systems, LCMAS 2004 (2004)

    Google Scholar 

41. Lomuscio, A., Woźna, B., Penczek, W.: Bounded model checking for knowledge over real time. In: Proceedings of the International Workshop on Concurrency, Specification and Programming (CS&P 2004). Informatik-Berichte, vol. 170, pp. 398–414 (2004)

    Google Scholar 

42. Raimondi, F., Lomuscio, A.: Automatic verification of deontic interpreted systems by model checking via OBDD’s. In: Proceedings of the Sixteenth European Conference on Artificial Intelligence, ECAI 2004 (2004)

    Google Scholar 

Download references