@article{DBLP:journals/tocl/LomuscioMR00,
  author    = {A. Lomuscio and
               R. van der Meyden and
               M. Ryan},
  title     = {Knowledge in multiagent systems: initial configurations
               and broadcast},
  journal   = {ACM Trans. Comput. Log.},
  volume    = {1},
  number    = {2},
  year      = {2000},
  pages     = {247-284},
  ee        = {http://doi.acm.org/10.1145/359496.359527},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/scp/BouajjaniFHR92,
  author    = {A. Bouajjani and
               J.-C. Fernandez and
               N. Halbwachs and
               P. Raymond},
  title     = {Minimal State Graph Generation},
  journal   = {Sci. Comput. Program.},
  volume    = {18},
  number    = {3},
  year      = {1992},
  pages     = {247-269},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@incollection{Hopcroft:1971,
 key = "Hopcroft 1971",
 author = "J. E. Hopcroft",
 title = "An $n \log n$ algorithm for minimizing the states in a finite automaton",
 booktitle = "The Theory of Machines and Computation",
 editor = "Z. Kohavi",
 publisher = "Academic Press",
 address = "New York",
 year = 1971,
 pages = "189-196"
}

@article{PaigeTarjan:1987,
 author = {Paige, R. and Tarjan, R. E.},
 title = {Three partition refinement algorithms},
 journal = {SIAM J. Comput.},
 volume = {16},
 number = {6},
 year = {1987},
 issn = {0097-5397},
 pages = {973--989},
 doi = {https://doi.org/10.1137/0216062},
 publisher = {Society for Industrial and Applied Mathematics},
 address = {Philadelphia, PA, USA}
}

@inproceedings{Ron:1997,
 author = {R. van der Meyden},
 title = {Constructing {F}inite {S}tate {I}mplementations of {K}nowledge-{B}ased {P}rograms with {P}erfect {R}ecall},
 booktitle = {PRICAI '96: Proceedings from the Workshop on Intelligent Agent Systems, Theoretical and Practical Issues},
 year = 1997,
 pages = {135--151},
 publisher = {Springer-Verlag},
}

@article{DBLP:journals/toplas/Sangiorgi09,
  author    = {Davide Sangiorgi},
  title     = {On the origins of bisimulation and coinduction},
  journal   = {ACM Trans. Program. Lang. Syst.},
  volume    = {31},
  number    = {4},
  year      = {2009},
  ee        = {http://doi.acm.org/10.1145/1516507.1516510},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

% pages =        {114--129},
@InProceedings{EvdMM2000:FOSSACS,
 author =       {Engelhardt, K. and van der Meyden, R. and Moses, Y.},
 title =        {A Program Refinement Framework Supporting Reasoning
                 about Knowledge and Time},
 booktitle =    {FOSSACS},
 year =         2000,
 editor =       {Jerzy Tiuryn},
 volume =       1784,
 series =       {LNCS},
 month =        mar,
 publisher =    "Springer"
}

@inproceedings{DBLP:conf/lpar/BickfordCHP04,
  author    = {M. Bickford and
               R. L. Constable and
               J. Y. Halpern and
               S. Petride},
  title     = {Knowledge-Based Synthesis of Distributed Systems Using Event
               Structures},
  booktitle = {LPAR},
  year      = {2004},
  pages     = {449-465},
  ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3452{\&}spage=449},
  crossref  = {DBLP:conf/lpar/2004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/lpar/2004,
  editor    = {F. Baader and
               A. Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning,
               11th International Conference, LPAR 2004, Montevideo, Uruguay,
               March 14-18, 2005, Proceedings},
  booktitle = {LPAR},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {3452},
  year      = {2005},
  isbn      = {3-540-25236-3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@incollection{Gammie:2011,
  author =       {P. Gammie},
  title =        "{KBPs}",
  booktitle =    {The Archive of Formal Proofs},
  editor =       {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  publisher =    {\url{http://isa-afp.org/entries/KBPs.shtml}},
  month =        Feb,
  year =         2011,
  note =         "{F}ormal proof development",
  ISSN =         {2150-914x}
}

@InProceedings{Quotients:2011,
  author =       "Kaliszyk, C. and Urban, C.",
  title =        "Quotients Revisited for {I}sabelle/{HOL}",
  booktitle = "SAC",
  year =      2011,
  publisher = "ACM"}

%  pages     = {313-328},
@article{DBLP:journals/fuin/KacprzakNNPPSWZ08,
  author    = {M. Kacprzak and
               W. Nabialek and
               A. Niewiadomski and
               W. Penczek and
               A. P{\'o}lrola and
               M. Szreter and
               B. Wozna and
               A. Zbrzezny},
  title     = "{VerICS} 2007 - a Model Checker for Knowledge and Real-Time",
  journal   = {Fundamenta Informaticae},
  volume    = {85},
  number    = {1-4},
  year      = {2008},
  ee        = {http://iospress.metapress.com/content/aju14j810h82w141/},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  booktitle = "SecureComm, 6th International ICST Conference on Security and Privacy in Communication Networks",
@InProceedings{Ron:2010,
  author =       "Al-Bataineh, O. and van der Meyden, R.",
  title =        "Epistemic Model Checking for Knowledge-Based Program Implementation: an Application to Anonymous Broadcast",
  booktitle = "SecureComm",
  year =      2010
}

%pages        = {44 - 59},
@inproceedings{vanEijck:DEMO:2005,
author       = {van Eijck, D. J. N. and Orzan, S.  M.},
title        = "Modelling the epistemics of communication with functional programming",
booktitle    = {TFP},
year         = {2005},
publisher    = {Tallinn University},
}

%  pages     = {682-688},
@inproceedings{DBLP:conf/cav/LomuscioQR09,
  author    = {A. Lomuscio and
               H. Qu and
               F. Raimondi},
  title     = "{MCMAS}: A Model Checker for the Verification of Multi-Agent
               Systems",
  booktitle = {CAV},
  year      = {2009},
  ee        = {https://doi.org/10.1007/978-3-642-02658-4_55},
  crossref  = {DBLP:conf/cav/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/cav/2009,
  editor    = {A. Bouajjani and
               O. Maler},
  title     = {Computer Aided Verification, 21st International Conference,
               CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5643},
  year      = {2009},
  isbn      = {978-3-642-02657-7},
  ee        = {https://doi.org/10.1007/978-3-642-02658-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  pages     = {479-483},
@inproceedings{DBLP:conf/cav/GammieM04,
  author    = {P. Gammie and
               R. van der Meyden},
  title     = {{MCK}: Model Checking the Logic of Knowledge},
  booktitle = {CAV},
  year      = {2004},
  crossref  = {DBLP:conf/cav/2004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/cav/2004,
  editor    = {R. Alur and
               D. Peled},
  title     = {Computer Aided Verification, 16th International Conference,
               CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {3114},
  year      = {2004},
  isbn      = {3-540-22342-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  pages     = {31-43},
@inproceedings{DBLP:conf/mkm/Ballarin06,
  author    = {C. Ballarin},
  title     = {Interpretation of Locales in {I}sabelle: Theories and Proof
               Contexts},
  booktitle = {MKM},
  year      = {2006},
  ee        = {https://doi.org/10.1007/11812289_4},
  crossref  = {DBLP:conf/mkm/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/mkm/2006,
  editor    = {J. M. Borwein and
               W. M. Farmer},
  title     = {Mathematical Knowledge Management, 5th International Conference,
               MKM 2006, Wokingham, UK, August 11-12, 2006, Proceedings},
  booktitle = {MKM},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4108},
  year      = {2006},
  isbn      = {3-540-37104-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{Shoham:2008,
 author = {Shoham, Y. and Leyton-Brown, K.},
 title = {Multiagent Systems: Algorithmic, Game-Theoretic, and Logical Foundations},
 year = {2008},
 isbn = {0521899435},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA}
}

%  pages     = {339-354},
@inproceedings{DBLP:conf/itp/LammichL10,
  author    = {P. Lammich and
               A. Lochbihler},
  title     = {The {I}sabelle {C}ollections {F}ramework},
  booktitle = {ITP},
  year      = {2010},
  ee        = {https://doi.org/10.1007/978-3-642-14052-5_24},
  crossref  = {DBLP:conf/itp/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/itp/2010,
  editor    = {M. Kaufmann and
               L. C. Paulson},
  title     = {Interactive Theorem Proving, First International Conference,
               ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
  booktitle = {ITP},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6172},
  year      = {2010},
  isbn      = {978-3-642-14051-8},
  ee        = {https://doi.org/10.1007/978-3-642-14052-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  pages     = {97-109},
@article{DBLP:journals/acta/Gries73,
  author    = {D. Gries},
  title     = "{D}escribing an {A}lgorithm by {H}opcroft",
  journal   = {Acta Informatica},
  volume    = {2},
  year      = {1973},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  booktitle =   {Functional and Logic Programming: 10th International Symposium: FLOPS 2010},
@inproceedings{Haftmann-Nipkow:2010:code,
  author =      {Florian Haftmann and Tobias Nipkow},
  title =       {Code Generation via Higher-Order Rewrite Systems},
  booktitle =   {FLOPS},
  year =        2010,
  publisher =   {Springer},
  series =      {LNCS},
  editor =      {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal},
  volume =      {6009}
}

@Book{Chellas:1980,
  author =    "B. Chellas",
  title =        "Modal Logic: an introduction",
  publisher =    "Cambridge University Press",
  year =         1980
}

@incollection{Berghofer-Reiter-AFP09,
  author =       {S. Berghofer and M. Reiter},
  title =        {Formalizing the Logic-Automaton Connection},
  booktitle =    {The Archive of Formal Proofs},
  editor =       {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  publisher =    {\url{http://isa-afp.org/entries/Presburger-Automata.shtml}},
  month =        Dec,
  year =         2009,
  note =         "{F}ormal proof development",
  ISSN =         {2150-914x}
}

%  pages     = {264-274},
@inproceedings{DBLP:conf/stoc/LeeY92,
  author    = {D. Lee and
               M. Yannakakis},
  title     = {Online Minimization of Transition Systems (Extended Abstract)},
  booktitle = {STOC},
  year      = {1992},
  crossref  = {DBLP:conf/stoc/STOC24},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/stoc/STOC24,
  title     = {Proceedings of the Twenty Fourth Annual ACM Symposium on
               Theory of Computing, 4-6 May 1992, Victoria, British Columbia,
               Canada},
  booktitle = {STOC},
  publisher = {ACM},
  year      = {1992},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  pages     = {115-157},
@article{DBLP:journals/iandc/Meyden98,
  author    = {R. van der Meyden},
  title     = {Common Knowledge and Update in Finite Environments},
  journal   = {Information and Computation},
  volume    = {140},
  number    = {2},
  year      = {1998},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Book{Nipkow-Paulson-Wenzel:2002,
  author = {T. Nipkow and L. C. Paulson and M. Wenzel},
  title  = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  publisher = {Springer},
  series = {LNCS},
  volume = 2283,
  year  = 2002
}

% pages = {262--273},
@inproceedings{Ron:1996,
 author = {R. van der Meyden},
 title = "Finite State Implementations of Knowledge-Based Programs",
 booktitle = {FTTCS},
 year = {1996},
 publisher = {Springer},
}

@Book{FHMV:1995,
  author =  "R. Fagin and J. Y. Halpern and Y. Moses and Vardi, M. Y.",
  title =   "{R}easoning about {K}nowledge",
  publisher =   "The MIT Press",
  year =   1995
}

%  pages     = {199-225},
@article{DBLP:journals/dc/FaginHMV97,
  author    = {R. Fagin and
               J. Y. Halpern and
               Y. Moses and
               M. Y. Vardi},
  title     = {Knowledge-Based Programs},
  journal   = {Distributed Computing},
  volume    = {10},
  number    = {4},
  year      = {1997},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{EdR:cup98,
  author = {W.-P. de Roever and K. Engelhardt},
  title = {Data Refinement: Model-Oriented Proof Methods and
                  their Comparison},
  publisher = {Cambridge University Press},
  pages = 430,
  year = 1998,
  annote = {With the assistance of Jos Coenen, Karl-Heinz Buth,
                  Paul Gardiner, Yassine Lakhnech, and Frank
                  Stomp},
  annote = {$\pounds$45\,/\,US\$69.95\,/\,AU\$125},
  http = {http://www.informatik.uni-kiel.de/~bkmail1/}
}

@inproceedings{DBLP:conf/tphol/BerghoferR09,
  author    = {S. Berghofer and
               M. Reiter},
  title     = {Formalizing the Logic-Automaton Connection},
  booktitle = {TPHOLs},
  year      = {2009},
  pages     = {147-163},
  ee        = {https://doi.org/10.1007/978-3-642-03359-9_12},
  crossref  = {DBLP:conf/tphol/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

%  isbn      = {978-3-642-03358-2},
@proceedings{DBLP:conf/tphol/2009,
  editor    = {S. Berghofer and
               T. Nipkow and
               C. Urban and
               M. Wenzel},
  title     = {TPHOLs},
  booktitle = {TPHOLs},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5674},
  year      = {2009},
  ee        = {https://doi.org/10.1007/978-3-642-03359-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{Lenzen:1978,
  author       = "W. Lenzen",
  title        = "{R}ecent {W}ork in {E}pistemic {L}ogic",
  journal      = {Acta Philosophica Fennica},
  year         = 1978,
  volume       = 30,
  number       = 1,
}

@Book{Hintikka:1962,
  author       = "J. Hintikka",
  title        = "{Knowledge and Belief: An Introduction to the Logic of Two Notions}",
  publisher    = "{Cornell University Press}",
  year         = 1962,
}

@incollection{AFP:TRANCL,
  author =       {C. Sternagel and R. Thiemann},
  title =        {Executable Transitive Closures of Finite Relations},
  booktitle =    "{T}he {A}rchive of {F}ormal {P}roofs",
  editor =       {G. Klein and T. Nipkow and L. Paulson},
  publisher =    {\url{http://isa-afp.org/entries/KBPs.shtml}},
  month =        mar,
  year =         2011,
  note =         {Formal proof development},
  ISSN =         {2150-914x}
}