MCK Publications
Papers on MCK, epistemic model checking, and algorithms for epistemic logic.
(Additional papers on other aspects of epistemic logic are available
here)
2019
- On the specification and verification of atomic swap smart contracts (extended abstract), R. van der Meyden, Proc. IEEE International Conference on Blockchain and Cryptocurrency, 2019 (Full version: arXiv:1811.06099)
2016
- Optimizing Epistemic Model Checking Using Conditional Independence, Ron Van Der Meyden, arXiv:160.03935,extended version of paper at TARK2017.
2015
- The complexity of approximations for epistemic synthesis, Xiaowei Huang and Ron Van Der Meyden, 4th Workshop on Synthesis, San Francisco, Jul 2015.
- Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic, Ron Van Der Meyden and Manas Patra, arXiv:1511.03003, extended version of a paper at TARK 2015.
2014
- Symbolic Model Checking Epistemic Strategy Logic, X. Huang and R. van der Meyden, AAAI 2014, pp. 1426-1432.
- Symbolic Synthesis for Epistemic Specifications with Observational Semantics, X. Huang and R. van der Meyden, TACAS 2014, pp. 455-469.
2013
- Symbolic Synthesis of Knowledge-based Program Implementations with Synchronous Semantics, Xiaowei Huang and Ron van der Meyden, TARK2013, Jan 2013
2012
- Synthesizing Strategies for Epistemic Goals by Epistemic Model Checking: an application to Pursuit-Evasion Games, Xiaowei Huang and Ron van der Meyden, AAAI2012, Jan 2012
- Experiments on Epistemic Model Checking in Pursuit-Evasion Games, Xiaowei Huang and Ron van der Meyden, technical report, Jan 2012
2011
- Symbolic Model Checking of Probabilistic Knowledge, Xiaowei Huang, Cheng Luo, and Ron van der Meyden, TARK2011, July 2011
- Abstraction for Epistemic Model Checking of Dining-Cryptographers based Protocols, Omar I. Al-Bataineh and R. van der Meyden, arXiv:1010.2287 extended version of paper in TARK2011.
- Model Checking Knowledge in Pursuit-Evasion Games, X. Huang, P. Maupin and R. van der Meyden, IJCAI2011, July 2011
2010
- Improved bounded model checking for a fair branching-time temporal epistemic logic, Xiaowei Huang, Cheng Luo, and Ron van der Meyden, July 2010
- Abstraction for Epistemic Model Checking of Dining Cryptographers-based Protocols, Omar I. Al-Bataineh and R. van der Meyden, Oct 2010
- Epistemic Model Checking for Knowledge-Based Program Implementation: an Application to Anonymous Broadcast, O. Al-Bataineh and R. van der Meyden, SecureComm'10, 6th International ICST Conference on Security and Privacy in Communication Networks, Singapore, Sept 7-9 2010.
- The Complexity of Epistemic Model Checking: Clock Semantics and Branching Time, X. Huang and R. van der Meyden, ECAI- 2010 (Extended version)
- Improved Bounded Model Checking for a Fair Branching-Time Temporal Epistemic Logic (Extended Abstract), X. Huang and C. Luo and R. van der Meyden, Proc. AAMAS 2010, (Copyright IFAAMAS.)
2009
- Model Checking Games for a Fair Branching-Time Temporal Epistemic Logic, X. Huang and R. van der Meyden, Australasian Joint Conference on Artificial Intelligence, Melbourne, Dec 2009.
2007
- Preservation of Epistemic Properties in Security Protocol Implementations, R. van der Meyden and T. Wilke, in Proc. Conf on Theoretical Aspects of Rationality and Knowledge, Brussels, July 2007, pp 212-221.
- Model Checking Knowledge and Linear Time: PSPACE Cases, Kai Engelhardt, Peter Gammie, and Ron van der Meyden, in Proc Symposium on Logical Foundations of Computer Science, New York, June 2007, pp. 195-211.
2005
- Model Checking Russian Cards, H.P. van Ditmarsch, W. van der Hoek, R. van der Meyden, J. Ruan, Electronic Notes in Theoretical Computer Science Volume 149, Issue 2 , 14 February 2006, Pages 105-123 Proceedings of the Third Workshop on Model Checking and Artificial Intelligence (MoChArt 2005) August 27, 2005 - San Francisco, CA, USA.
- Synthesis of Distributed Systems from Knowledge-based Specifications, R. van der Meyden, T. Wilke, CONCUR 2005 - Concurrency Theory, 16th International Conference, San Francisco, Aug 2005, pp. 562-576 An extended version of this paper appears as UNSW CSE technical report 0504.
2004
- A knowledge based analysis of cache coherence, K. Baukus and R. van der Meyden, International Conference on Formal Engineering Methods, Seattle, Nov 2004, LNCS No. 3308, pp. 99-114.
- MCK: Model Checking the Logic of Knowledge, P. Gammie and R. van der Meyden, 16th International conference on Computer Aided Verification, CAV 2004, pp. 479- 483. (Copyright Springer-Verlag)
- Symbolic Model Checking the Knowledge of the Dining Cryptographers, R. van der Meyden and K. Su, 17th IEEE Computer Security Foundations Workshop, Asilomar, June 2004, pp. 280-291
1999
- Model Checking Knowledge and Time in Systems with Perfect Recall, R. van der Meyden and N. Shilov, Proc. Conf. on Foundations of Software Technology and Theoretical Computer Science, Madras, Dec 1999. Springer LNCS No. 1738, pp. 432-445. (Copyright Springer-Verlag)
1998
- Synthesis from Knowledge-Based Specifications, R. van der Meyden and M. Y. Vardi, Proc. CONCUR'98, 9th International Conf. on Concurrency Theory, Springer LNCS No. 1466, Nice, Sept 98, pp. 34-49. (Copyright Springer-Verlag)
1996
- Finite State Implementations of Knowledge-Based Programs, R. van der Meyden, in Proc. Conf. on Foundations of Software Technology and Theoretical Computer Science, Hyderabad India, Dec 1996, Springer LNCS No. 1180, pp. 262-273.
- Knowledge-Based Programs: on the Complexity of Perfect Recall in Finite Environments (Extended Abstract), R. van der Meyden, Proceedings of the Conference on Theoretical Aspects of Reasoning about Knowledge, Renesse, Netherlands, March 1996, pp. 31-50.
- Constructing Finite State Implementations of Knowledge Based Programs with Perfect Recall, R. van der Meyden, in Intelligent Agent Systems: Theoretical and Practical Issues (Based on a Workshop Held at PRICAI'96, Cairns, Australia, Aug 1996) , Springer LNAI No. 1209, 1997, pp. 135-152.
1994
- Common Knowledge and Update in Finite Environments, R. van der Meyden, Information and Computation Vol 140, No. 2, Feb 1998, pp. 115-157. A preliminary version of this paper appeared in Proceedings of the Conference on Theoretical Aspects of Reasoning about Knowledge, Pacific Grove CA, March 1994.)