{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,2]],"date-time":"2026-05-02T06:49:46Z","timestamp":1777704586880,"version":"3.51.4"},"reference-count":32,"publisher":"SAGE Publications","issue":"5","license":[{"start":{"date-parts":[[2018,8,21]],"date-time":"2018-08-21T00:00:00Z","timestamp":1534809600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Journal of Intelligent &amp; Fuzzy Systems"],"published-print":{"date-parts":[[2018,11,20]]},"abstract":"<jats:p>\n                    The purpose of the current article is to introduce a propositional linear time temporal logic of common knowledge. This logic can be utilized for reasoning when the agents should commonly know the information that may change over time. This is the main advantage of our logic over the existing temporal logics of knowledge in the literature. We provide a language, as well as appropriate semantics for our logic. We also introduce a resolution-based proof method for this logic by adopting the approach proposed by Dixon et al. [\n                    <jats:xref ref-type=\"bibr\">11<\/jats:xref>\n                    ,\n                    <jats:xref ref-type=\"bibr\">14<\/jats:xref>\n                    ]. This resolution system is based upon a\n                    <jats:italic>separated normal form<\/jats:italic>\n                    . We prove that our resolution system is sound and complete. More importantly, to justify our approach, we apply our resolution method to specify and verify the anonymity properties of Chaum\u2019s dining cryptographers protocol [\n                    <jats:xref ref-type=\"bibr\">4<\/jats:xref>\n                    ].\n                  <\/jats:p>","DOI":"10.3233\/jifs-17988","type":"journal-article","created":{"date-parts":[[2018,8,24]],"date-time":"2018-08-24T13:54:14Z","timestamp":1535118854000},"page":"5507-5522","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":0,"title":["Temporal logic of common knowledge and its resolution-based proof method"],"prefix":"10.1177","volume":"35","author":[{"given":"Hadi","family":"Farahani","sequence":"first","affiliation":[{"name":"Department of Computer Science, Faculty of Mathematical Sciences, Shahid Beheshti University, G.C., Evin, Tehran, Iran"}]},{"given":"Saman","family":"Moshiri","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Faculty of Mathematical Sciences, Shahid Beheshti University, G.C., Evin, Tehran, Iran"}]}],"member":"179","published-online":{"date-parts":[[2018,8,21]]},"reference":[{"key":"e_1_3_1_2_2","first-page":"17","article-title":"Towards GCM re-configuration extending specification by norms, pp","author":"Basso A.","year":"2007","unstructured":"BassoA. and BolotovA., Towards GCM re-configuration extending specification by norms, pp, In Making Grids Work: Proceedings of the CoreGRID Workshop on Programming Models Grid and P2P System Architecture Grid Systems, Tools and Environments, (Towards GCM re-configuration extending specification by norms), 2007, pp. 17\u201329.","journal-title":"In Making Grids Work: Proceedings of the CoreGRID Workshop on Programming Models Grid and P2P System Architecture Grid Systems, Tools and Environments, (Towards GCM re-configuration extending specification by norms)"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jet.2014.11.002"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00199-016-0993-0"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00206326"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/210197.210200"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5643-5_3"},{"key":"e_1_3_1_8_2","article-title":"A Lazy Approach to Temporal Epistemic Logic Model Checking, AAMAS \u201916","author":"Cimatti A.","year":"2016","unstructured":"CimattiA., GarioM. and TonettaS., A Lazy Approach to Temporal Epistemic Logic Model Checking, AAMAS \u201916, Proceedings of the 2016 International Conference on Autonomous Agents and Multiagent Systems, International Foundation for Autonomous Agents and Multiagent Systems, 2016.","journal-title":"Proceedings of the 2016 International Conference on Autonomous Agents and Multiagent Systems, International Foundation for Autonomous Agents and Multiagent Systems"},{"key":"e_1_3_1_9_2","volume-title":"Model Checking","author":"Clarke E.","year":"2000","unstructured":"ClarkeE., GrumbergO., PeledD.A., Model Checking, MIT Press, 2000."},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/1119439.1119443"},{"key":"e_1_3_1_11_2","doi-asserted-by":"crossref","unstructured":"van DitmarschH. W.van der Hoekand B.Kooi Dynamic Epistemic Logic Springer 2008.","DOI":"10.1007\/978-1-4020-5839-4"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.11.043"},{"key":"e_1_3_1_13_2","first-page":"43","volume-title":"Proceedings of the Third International Conference on Temporal Logic (ICTL)","author":"Dixon C.","year":"2000","unstructured":"DixonC., FisherM., Clausal Resolution for Logics of Time and Knowledge with Synchrony and Perfect Recall, In Proceedings of the Third International Conference on Temporal Logic (ICTL), Leipzig, Germany, 2000, pp. 43\u201352."},{"key":"e_1_3_1_14_2","first-page":"69","volume-title":"Proceedings of TIME-00 the Seventh International Workshop on Temporal Representation and Reasoning","author":"Dixon C.","year":"2000","unstructured":"DixonC., FisherM., Resolution-Based Proof for Multi-Modal Temporal Logics of Knowledge, In Proceedings of TIME-00 the Seventh International Workshop on Temporal Representation and Reasoning, Nova Scotia, Canada, 2000, pp. 69\u201378."},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/8.3.345"},{"key":"e_1_3_1_16_2","volume-title":"Proceedings of the Twelfth International Joint Conference on Artificial Intelligence","author":"Fisher M.","year":"1991","unstructured":"FisherM., A Resolution Method for Temporal Logic, In Proceedings of the Twelfth International Joint Conference on Artificial Intelligence, Sydney, Australia, Morgan Kaufman Publisher, 1991."},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/7.4.429"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/371282.371311"},{"key":"e_1_3_1_19_2","unstructured":"GarioM.E.G. A formal foundation of FDI design via temporal epistemic logic ICT International Doctoral School Ph.D. thesis 2016."},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40573-5_5"},{"key":"e_1_3_1_21_2","volume-title":"Design and Validation of Computer Protocols","author":"Holzmann G.","year":"1991","unstructured":"HolzmannG., Design and Validation of Computer Protocols, Englewood Cliffs, New Jersey, Prentice-Hall, 1991."},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2003.1214882"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2004.10.005"},{"key":"e_1_3_1_24_2","first-page":"91","volume-title":"2nd International Conference on Temporal Logic","author":"Kupferman O.","year":"1997","unstructured":"KupfermanO. and VardiM.Y., Synthesis with Incomplete Information, In 2nd International Conference on Temporal Logic Manchester, 1997, pp. 91\u2013106."},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.aasri.2013.10.036"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11104-9_141"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/ext074"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.06.007"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jalgor.2007.04.001"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/168588.168600"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/2529993"}],"container-title":["Journal of Intelligent &amp; Fuzzy Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JIFS-17988","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/JIFS-17988","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JIFS-17988","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T09:41:33Z","timestamp":1777455693000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/JIFS-17988"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,8,21]]},"references-count":32,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2018,11,20]]}},"alternative-id":["10.3233\/JIFS-17988"],"URL":"https:\/\/doi.org\/10.3233\/jifs-17988","relation":{},"ISSN":["1064-1246","1875-8967"],"issn-type":[{"value":"1064-1246","type":"print"},{"value":"1875-8967","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,8,21]]}}}