Skip to main content
SpringerLink
Log in
Book cover

International Conference on Interactive Theorem Proving

ITP 2011: Interactive Theorem Proving pp 87–102Cite as

Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments

  • Conference paper

  • 666 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6898))

Abstract

Knowledge-based programs (KBPs) are a formalism for directly relating agents’ knowledge and behaviour. Here we present a general scheme for compiling KBPs to executable automata with a proof of correctness in Isabelle/HOL. We develop the algorithm top-down, using Isabelle’s locale mechanism to structure these proofs, and show that two classic examples can be synthesised using Isabelle’s code generator.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Al-Bataineh, O., van der Meyden, R.: Epistemic model checking for knowledge-based program implementation: an application to anonymous broadcast. In: Secure Comm. (2010)

    Google Scholar 

  2. Ballarin, C.: Interpretation of locales in isabelle: Theories and proof contexts. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol. 4108, pp. 31–43. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  3. Berghofer, S., Reiter, M.: Formalizing the logic-automaton connection. In: Klein, G., Nipkow, T., Paulson, L. (eds.) The Archive of Formal Proofs (December 2009) Formal proof development, http://afp.sf.net/entries/Presburger-Automata.shtml

  4. Bickford, M., Constable, R.C., Halpern, J.Y., Petride, S.: Knowledge-based synthesis of distributed systems using event structures. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 449–465. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Chellas, B.: Modal Logic: an introduction. Cambridge University Press, Cambridge (1980)

    Book  MATH  Google Scholar 

  6. van Eijck, D.J.N., Orzan, S.M.: Modelling the epistemics of communication with functional programming. In: TFP. Tallinn University (2005)

    Google Scholar 

  7. Engelhardt, K., van der Meyden, R., Moses, Y.: A program refinement framework supporting reasoning about knowledge and time. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol. 1784, p. 114. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

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

    MATH  Google Scholar 

  9. Gammie, P.: KBPs. In: Klein, G., Nipkow, T., Paulson, L. (eds.) The Archive of Formal Proofs (May 2011) Formal proof development, http://afp.sf.net/entries/KBPs.shtml

  10. Gammie, P., van der Meyden, R.: MCK: Model checking the logic of knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 479–483. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  11. Gries, D.: Describing an Algorithm by Hopcroft. Acta Informatica 2 (1973)

    Google Scholar 

  12. Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103–117. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  13. Kacprzak, M., Nabialek, W., Niewiadomski, A., Penczek, W., Pólrola, A., Szreter, M., Wozna, B., Zbrzezny, A.: VerICS 2007 - a model checker for knowledge and real-time. Fundamenta Informaticae 85(1-4) (2008)

    Google Scholar 

  14. Kaliszyk, C., Urban, C.: Quotients revisited for Isabelle/HOL. In: SAC. ACM, New York (2011)

    Google Scholar 

  15. Lammich, P., Lochbihler, A.: The isabelle collections framework. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 339–354. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  16. Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: A model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682–688. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  17. van der Meyden, R.: Constructing finite state implementations of knowledge-based programs with perfect recall. In: Cavedon, L., Rao, A.S., Wobcke, W. (eds.) PRICAI-WS 1996. LNCS, vol. 1209. Springer, Heidelberg (1997)

    Google Scholar 

  18. van der Meyden, R.: Finite state implementations of knowledge-based programs. In: Chandru, V., Vinay, V. (eds.) FSTTCS 1996. LNCS, vol. 1180. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  19. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  20. de Roever, W.P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, Cambridge (1998)

    Book  MATH  Google Scholar 

  21. Shoham, Y., Leyton-Brown, K.: Multiagent Systems: Algorithmic, Game-Theoretic, and Logical Foundations. Cambridge University Press, New York (2008)

    Book  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. The Australian National University, Canberra, ACT, 0200, Australia

    Peter Gammie

  2. National ICT, Australia

    Peter Gammie

Authors
  1. Peter Gammie
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculteit Informatica, Open Universiteit, Postbus 2960, Heerlen, 6401 DL, The Netherlands

    Marko van Eekelen

  2. FNWI/ICIS/IS, Radboud Universiteit Nijmegen, Postbus 9010, 6500 GL, Nijmegen, The Netherlands

    Herman Geuvers  & Freek Wiedijk  & 

  3. Faculteit Informatica, Open Universiteit, Postbus 2960, 6401 DL, Heerlen, The Netherlands

    Julien Schmaltz

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gammie, P. (2011). Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds) Interactive Theorem Proving. ITP 2011. Lecture Notes in Computer Science, vol 6898. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22863-6_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22863-6_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22862-9

  • Online ISBN: 978-3-642-22863-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation