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. [11, 14]. This resolution system is based upon a separated normal form. 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’s dining cryptographers protocol [4].
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–29.
2.
BlumeaL., EasleyD., KleinbergJ., KleinbergR. and TardosOE., Introduction to computer science and economic theory, Journal of Economic Theory156 (2015), 1–13.
3.
BoukourasA. and KoufopoulosK., Efficient allocations in economies with asymmetric information when the realized frequency of types is common knowledge, Journal of Economic Theory64 (2017), 75–98.
4.
ChaumD., The dining cryptographers problem: Unconditional sender and receiver untraceability, Journal of Cryptology1 (1988), 65–75.
5.
ChomickiJ., Efficient checking of temporal integrity constraints using bounded history encoding, ACM Transactions on Database Systems20(2) (1995), 149–186.
6.
ChomickiJ. and TomanD., Temporal logic in information systems, Logics for Databases and Information Systems (1998), 31–70.
7.
CimattiA., GarioM. and TonettaS., A Lazy Approach to Temporal Epistemic Logic Model Checking, AAMAS ’16, Proceedings of the 2016 International Conference on Autonomous Agents and Multiagent Systems, International Foundation for Autonomous Agents and Multiagent Systems, 2016.
8.
ClarkeE., GrumbergO., PeledD.A., Model Checking, MIT Press, 2000.
9.
DegtyarevA., FisherM. and KonevB., Monodic temporal resolution, ACM Transactions on Computational Logic7(1) (2006).
10.
van DitmarschH., W.van der Hoekand B.Kooi, Dynamic Epistemic Logic, Springer, 2008.
11.
DixonC., Fernandez GagoM.C., FisherM. and van der HoekW., Temporal logics of knowledge and their applications in security, Electronic Notes in Theoretical Computer Science186 (2007), 27–42.
12.
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–52.
13.
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–78.
14.
DixonC., FisherM. and WooldridgeM., Resolution for temporal logics of knowledge, Journal of Logic and Computation8(3) (1998), 345–372.
15.
FisherM., A Resolution Method for Temporal Logic, In Proceedings of the Twelfth International Joint Conference on Artificial Intelligence, Sydney, Australia, Morgan Kaufman Publisher, 1991.
16.
FisherM., A normal form for temporal logic and its application in theorem proving and execution, Journal of Logic and Computation7(4) (1997).
17.
FisherM., DixonC. and PeimM., Clausal temporal resolution, ACM Transactions on Computational Logic2(1) (2001), 12–56.
18.
GarioM.E.G., A formal foundation of FDI design via temporal epistemic logic, ICT International Doctoral School, Ph.D. thesis, 2016.
19.
GottliebJ., Common Knowledge and Voter Coordination, Experimental Evidence from Mali, Springer International Publishing Switzerland, 2016.
20.
HolzmannG., Design and Validation of Computer Protocols, Englewood Cliffs, New Jersey, Prentice-Hall, 1991.
21.
KonevB., DegtyarevA., DixonC., FisherM. and HustadtU., Towards the Implementation of First-Order Temporal Resolution: The Expanding Domain Case, In Proceedings of TIME-International Conference on Temporal Logic2003, pp. 72–82.
22.
KonevB., DegtyarevA., DixonC., FisherM. and HustadtU., Mechanising first-order temporal resolution, Information and Computation199(1-2) (2005), 55–86.
23.
KupfermanO. and VardiM.Y., Synthesis with Incomplete Information, In 2nd International Conference on Temporal LogicManchester, 1997, pp. 91–106.
24.
LiuY.F., HuangQ.M., ZhangJ.H., YangX.H., LiY., WangY., WangJ.M., ZhangH. and GuanJ.J., Application of Information System of Varieties of Common Knowledge in PVP, AASRI Conference on Intelligent Systems and Control, AASRI Proceding 42013, pp236–242.
25.
MannaZ., PnueliA., The Temporal Logic of Reactive and Concurrent Systems, Specification, Springer-Verlag, 1992.
26.
MatsuhisaT., Common-Knowledge and Cooperation Management I, Proceedings of the 4th International Conference on Computer Engineering and Networks, Lecture Notes in Electrical Engineering 355, Springer International Publishing Switzerland, 2015.
27.
NalonC., ZhangL., DixonC. and HustadtU., A resolution-based calculus for coalition logic, Journal of Logic and Computation24(4) (2014), 883–917.
28.
NalonC. and KutzO., Towards resolution-based reasoning for connected logics, Electronic Notes in Theoretical Computer Science305 (2014), 85–102.
29.
NalonC. and DixonC., Clausal resolution for normal modal logics, Journal of Algorithms62(3-4) (2007), 117–134.
30.
OlivaS., On the Complexity of Resolution-based Proof Systems, The Departament de Llenguatges i Sistemes Informàtics Universitat Politècnica de Catalunya, Ph.D. Thesis, 2013.
31.
PnueliA. and RosnerR., On the Synthesis of a Reactive Module, In Proceedings of the 16th ACM Symposium on the Principles of Programming Languages (1989), pp. 179–190.
32.
SyversonP., Adding Time to a Logic of Authentication, In Proceeding of the ACM Conference on Computer and Communication Security and Privacy1993, pp. 97–101.
33.
ZhangL., HustadtU. and DixonC., A resolution calculus for the branching-time temporal logic CTL, ACM Transactions on Computational Logic15(1) (2014), Article 10.
