Verified synthesis of knowledge-based programs in finite synchronous environments

Peter Gammie

doi:10.1007/978-3-642-22863-6_9

Verified synthesis of knowledge-based programs in finite synchronous environments

Peter Gammie^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

1 Citation (Scopus)

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.

Original language	English
Title of host publication	Interactive Theorem Proving - Second International Conference, ITP 2011, Proceedings
Pages	87-102
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-22863-6_9
Publication status	Published - 2011
Event	2nd International Conference on Interactive Theorem Proving, ITP 2011 - Berg en Dal, Netherlands Duration: 22 Aug 2011 → 25 Aug 2011

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6898 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	2nd International Conference on Interactive Theorem Proving, ITP 2011
Country/Territory	Netherlands
City	Berg en Dal
Period	22/08/11 → 25/08/11

Access to Document

10.1007/978-3-642-22863-6_9

Cite this

Gammie, P. (2011). Verified synthesis of knowledge-based programs in finite synchronous environments. In Interactive Theorem Proving - Second International Conference, ITP 2011, Proceedings (pp. 87-102). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6898 LNCS). https://doi.org/10.1007/978-3-642-22863-6_9

@inproceedings{54dd5b0eac3c43d6aaf07769b6a31ece,

title = "Verified synthesis of knowledge-based programs in finite synchronous environments",

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.",

author = "Peter Gammie",

year = "2011",

doi = "10.1007/978-3-642-22863-6_9",

language = "English",

isbn = "9783642228629",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "87--102",

booktitle = "Interactive Theorem Proving - Second International Conference, ITP 2011, Proceedings",

note = "2nd International Conference on Interactive Theorem Proving, ITP 2011 ; Conference date: 22-08-2011 Through 25-08-2011",

}

Gammie, P 2011, Verified synthesis of knowledge-based programs in finite synchronous environments. in Interactive Theorem Proving - Second International Conference, ITP 2011, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6898 LNCS, pp. 87-102, 2nd International Conference on Interactive Theorem Proving, ITP 2011, Berg en Dal, Netherlands, 22/08/11. https://doi.org/10.1007/978-3-642-22863-6_9

Verified synthesis of knowledge-based programs in finite synchronous environments. / Gammie, Peter.
Interactive Theorem Proving - Second International Conference, ITP 2011, Proceedings. 2011. p. 87-102 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6898 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Verified synthesis of knowledge-based programs in finite synchronous environments

AU - Gammie, Peter

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=80052175000&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-22863-6_9

DO - 10.1007/978-3-642-22863-6_9

M3 - Conference contribution

SN - 9783642228629

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 87

EP - 102

BT - Interactive Theorem Proving - Second International Conference, ITP 2011, Proceedings

T2 - 2nd International Conference on Interactive Theorem Proving, ITP 2011

Y2 - 22 August 2011 through 25 August 2011

ER -

Verified synthesis of knowledge-based programs in finite synchronous environments

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this