Knowledge-based programs


Title: Knowledge-based programs
Author: Peter Gammie
Submission date: 2011-05-17
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.
Change history: [2012-03-06]: Add some more views and revive the code generation.
  author  = {Peter Gammie},
  title   = {Knowledge-based programs},
  journal = {Archive of Formal Proofs},
  month   = may,
  year    = 2011,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Transitive-Closure, Trie
Used by: LTL_to_DRA
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.