Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments
作者： Peter Gammie
DOI: 10.1007/978-3-642-22863-6_9
关键词: Correctness 、 Theoretical computer science 、 Programming language 、 HOL 、 Knowledge-based systems 、 Code generation 、 Mathematical proof 、 Automated theorem proving 、 Automata theory 、 Executable 、 Computer science
摘要: Knowledge-based programs (KBPs) are a formalism for directly relating agents' knowledge and behaviour. Here we present general scheme compiling KBPs to executable automata with proof of correctness in Isabelle/HOL. We develop the algorithm top-down, using Isabelle's locale mechanism structure these proofs, show that two classic examples can be synthesised code generator.
springer.com
peteg.org 
ru.nl 参考文章(22)
Ron van der Meyden, Finite State Implementations of Knowledge-Based Programs foundations of software technology and theoretical computer science. pp. 262- 273 ,(1996) , 10.1007/3-540-62034-6_55
Peter Gammie, Ron van der Meyden, MCK: Model Checking the Logic of Knowledge Computer Aided Verification. ,vol. 3114, pp. 479- 483 ,(2004) , 10.1007/978-3-540-27813-9_41
Florian Haftmann, Tobias Nipkow, Code generation via higher-order rewrite systems international symposium on functional and logic programming. pp. 103- 117 ,(2010) , 10.1007/978-3-642-12251-4_9
Kai Engelhardt, W. DeRoever, Data Refinement: Model-Oriented Proof Methods and their Comparison ,(1998)
Kevin Leyton-Brown, Yoav Shoham, Multiagent Systems: Algorithmic, Game-Theoretic, and Logical Foundations ,(2008)
Ron van der Meyden, Constructing Finite State Implementations of Knowledge-Based Programs with Perfect Recall PRICAI '96 Proceedings from the Workshop on Intelligent Agent Systems, Theoretical and Practical Issues. pp. 135- 151 ,(1996)
Clemens Ballarin, Interpretation of Locales in Isabelle: Theories and Proof Contexts Lecture Notes in Computer Science. pp. 31- 43 ,(2006) , 10.1007/11812289_4
Kai Engelhardt, Ron van der Meyden, Yoram Moses, A Program Refinement Framework Supporting Reasoning about Knowledge and Time foundations of software science and computation structure. pp. 114- 129 ,(2000) , 10.1007/3-540-46432-8_8
Peter Lammich, Andreas Lochbihler, The Isabelle Collections Framework Interactive Theorem Proving. pp. 339- 354 ,(2010) , 10.1007/978-3-642-14052-5_24
Alessio Lomuscio, Hongyang Qu, Franco Raimondi, MCMAS: A Model Checker for the Verification of Multi-Agent Systems Computer Aided Verification. pp. 682- 688 ,(2009) , 10.1007/978-3-642-02658-4_55