Using temporal logics of knowledge for specification and verification - A case study

被引：0
作者：
Department of Computer Science, University of Liverpool, Liverpool L69 7ZF, United Kingdom [1 ]
机构：
[1] Department of Computer Science, University of Liverpool
来源：
J. Appl. Logic | 2006年 / 1卷 / 50-78期
基金：
英国工程与自然科学研究理事会;
关键词：
Automated deduction; Resolution; Specification and verification; Temporal and epistemic logics;
D O I：
10.1016/j.jal.2005.08.003
中图分类号：
学科分类号：
摘要：
Temporal logics of knowledge are useful for reasoning about situations where the knowledge of an agent or component is important, and where change in this knowledge may occur over time. Here we use temporal logics of knowledge to reason about the game Cluedo. We show how to specify Cluedo using temporal logics of knowledge and prove statements about the knowledge of the players using a clausal resolution calculus for this logic. We discuss the advantages and disadvantages of using this logic to specify and verify the game Cluedo and describe related implementations. © 2005 Elsevier B.V. All rights reserved.
引用
收藏
页码：50 / 78
页数：28
相关论文
共 37 条
  • [1] Fisher M., Wooldridge M., On the formal specification and verification of multi-agent systems, Internat. J. Cooperative Inform. Syst., 6, 1, pp. 37-65, (1997)
  • [2] Halpern J.Y., Using reasoning about knowledge to analyze distributed systems, Annu. Rev. Comput. Sci., 2, pp. 37-68, (1987)
  • [3] Meyer J.-J.C., Van Der Hoek W., Epistemic Logic for Computer Science and Artificial Intelligence, Cambridge Tracts in Theoretical Computer Science, 41, (1995)
  • [4] Syverson P., Adding time to a logic of authentication, Proceedings of the First ACM Conference on Computer and Communications Security, pp. 97-101, (1993)
  • [5] Glasgow J., MacEwen G., Panangaden P., A logic to reason about security, ACM Trans. Comput. Syst., 10, 3, pp. 226-264, (1992)
  • [6] Fagin R., Halpern J.Y., Moses Y., Vardi M.Y., Reasoning about Knowledge, (1995)
  • [7] Dixon C., Fisher M., Wooldridge M., Resolution for temporal logics of knowledge, J. Logic Comput., 8, 3, pp. 345-372, (1998)
  • [8] Dixon C., Fisher M., Resolution-based proof for multi-modal temporal logics of knowledge, Proceedings of TIME-00 the Seventh International Workshop on Temporal Representation and Reasoning, Cape Breton, Nova Scotia, Canada, pp. 69-78, (2000)
  • [9] Halpern J.Y., Vardi M.Y., The complexity of reasoning about knowledge and time. i lower bounds, J. Comput. System Sci., 38, pp. 195-237, (1989)
  • [10] Gabbay D., Pnueli A., Shelah S., Stavi J., The temporal analysis of fairness, Proceedings of the Seventh ACM Symposium on the Principles of Programming Languages, pp. 163-173, (1980)
1234