Actions you can handle: Dependent types for AI plans

Alasdair Hill; Ekaterina Komendantskaya; Matthew L. Daggitt; Ronald P. A. Petrick

doi:10.1145/3471875.3472990

Actions you can handle: Dependent types for AI plans

Alasdair Hill, Ekaterina Komendantskaya, Matthew L. Daggitt, Ronald P. A. Petrick

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

Abstract

Verification of AI is a challenge that has engineering, algorithmic and programming language components. For example, AI planners are deployed to model actions of autonomous agents. They comprise a number of searching algorithms that, given a set of specified properties, find a sequence of actions that satisfy these properties. Although AI planners are mature tools from the algorithmic and engineering points of view, they have limitations as programming languages. Decidable and efficient automated search entails restrictions on the syntax of the language, prohibiting use of higher-order properties or recursion. This paper proposes a methodology for embedding plans produced by AI planners into the dependently-typed language Agda, which enables users to reason about and verify more general and abstract properties of plans, and also provides a more holistic programming language infrastructure for modelling plan execution.

Original language	English
Title of host publication	TyDe 2021: Proceedings of the 6th ACM SIGPLAN International Workshop on Type-Driven Development
Editors	Hsiang-Shang Ko, Dominic Orchard
Publisher	Association for Computing Machinery
Pages	1-13
Number of pages	13
ISBN (Electronic)	9781450386166
DOIs	https://doi.org/10.1145/3471875.3472990
Publication status	Published - 18 Aug 2021
Event	6th ACM SIGPLAN International Workshop on Type-Driven Development 2021 - Virtual, Online, Korea, Republic of Duration: 22 Aug 2021 → …

Conference

Conference	6th ACM SIGPLAN International Workshop on Type-Driven Development 2021
Abbreviated title	TyDe 2021
Country/Territory	Korea, Republic of
City	Virtual, Online
Period	22/08/21 → …

Keywords

AI Planners
Dependent Types
Verification

ASJC Scopus subject areas

Computer Science Applications
Software

Access to Document

10.1145/3471875.3472990

Cite this

@inproceedings{cc448c848f494026ace6f765f56580fb,

title = "Actions you can handle: Dependent types for AI plans",

abstract = "Verification of AI is a challenge that has engineering, algorithmic and programming language components. For example, AI planners are deployed to model actions of autonomous agents. They comprise a number of searching algorithms that, given a set of specified properties, find a sequence of actions that satisfy these properties. Although AI planners are mature tools from the algorithmic and engineering points of view, they have limitations as programming languages. Decidable and efficient automated search entails restrictions on the syntax of the language, prohibiting use of higher-order properties or recursion. This paper proposes a methodology for embedding plans produced by AI planners into the dependently-typed language Agda, which enables users to reason about and verify more general and abstract properties of plans, and also provides a more holistic programming language infrastructure for modelling plan execution.",

keywords = "AI Planners, Dependent Types, Verification",

author = "Alasdair Hill and Ekaterina Komendantskaya and Daggitt, {Matthew L.} and Petrick, {Ronald P. A.}",

note = "Funding Information: The first author acknowledges support of the EPSRC Doctoral Training scheme; the second and third author acknowledge generous support of the EPSRC grant AISEC: AI Secure and Explainable by Construction, EP/T026952/1, https: //www.macs.hw.ac.uk/aisec/. The authors also thank the TyDe{\textquoteright}21 reviewers for their valuable input, which lead to substantial clarification and simplifaction of some of the code accompanying this paper. Publisher Copyright: {\textcopyright} 2021 ACM.; 6th ACM SIGPLAN International Workshop on Type-Driven Development 2021, TyDe 2021 ; Conference date: 22-08-2021",

year = "2021",

month = aug,

day = "18",

doi = "10.1145/3471875.3472990",

language = "English",

pages = "1--13",

editor = "Hsiang-Shang Ko and Dominic Orchard",

booktitle = "TyDe 2021: Proceedings of the 6th ACM SIGPLAN International Workshop on Type-Driven Development",

publisher = "Association for Computing Machinery",

address = "United States",

}

Hill, A, Komendantskaya, E, Daggitt, ML & Petrick, RPA 2021, Actions you can handle: Dependent types for AI plans. in H-S Ko & D Orchard (eds), TyDe 2021: Proceedings of the 6th ACM SIGPLAN International Workshop on Type-Driven Development. Association for Computing Machinery, pp. 1-13, 6th ACM SIGPLAN International Workshop on Type-Driven Development 2021, Virtual, Online, Korea, Republic of, 22/08/21. https://doi.org/10.1145/3471875.3472990

Actions you can handle: Dependent types for AI plans. / Hill, Alasdair; Komendantskaya, Ekaterina; Daggitt, Matthew L. et al.
TyDe 2021: Proceedings of the 6th ACM SIGPLAN International Workshop on Type-Driven Development. ed. / Hsiang-Shang Ko; Dominic Orchard. Association for Computing Machinery, 2021. p. 1-13.

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

TY - GEN

T1 - Actions you can handle

T2 - 6th ACM SIGPLAN International Workshop on Type-Driven Development 2021

AU - Hill, Alasdair

AU - Komendantskaya, Ekaterina

AU - Daggitt, Matthew L.

AU - Petrick, Ronald P. A.

N1 - Funding Information: The first author acknowledges support of the EPSRC Doctoral Training scheme; the second and third author acknowledge generous support of the EPSRC grant AISEC: AI Secure and Explainable by Construction, EP/T026952/1, https: //www.macs.hw.ac.uk/aisec/. The authors also thank the TyDe’21 reviewers for their valuable input, which lead to substantial clarification and simplifaction of some of the code accompanying this paper. Publisher Copyright: © 2021 ACM.

PY - 2021/8/18

Y1 - 2021/8/18

N2 - Verification of AI is a challenge that has engineering, algorithmic and programming language components. For example, AI planners are deployed to model actions of autonomous agents. They comprise a number of searching algorithms that, given a set of specified properties, find a sequence of actions that satisfy these properties. Although AI planners are mature tools from the algorithmic and engineering points of view, they have limitations as programming languages. Decidable and efficient automated search entails restrictions on the syntax of the language, prohibiting use of higher-order properties or recursion. This paper proposes a methodology for embedding plans produced by AI planners into the dependently-typed language Agda, which enables users to reason about and verify more general and abstract properties of plans, and also provides a more holistic programming language infrastructure for modelling plan execution.

AB - Verification of AI is a challenge that has engineering, algorithmic and programming language components. For example, AI planners are deployed to model actions of autonomous agents. They comprise a number of searching algorithms that, given a set of specified properties, find a sequence of actions that satisfy these properties. Although AI planners are mature tools from the algorithmic and engineering points of view, they have limitations as programming languages. Decidable and efficient automated search entails restrictions on the syntax of the language, prohibiting use of higher-order properties or recursion. This paper proposes a methodology for embedding plans produced by AI planners into the dependently-typed language Agda, which enables users to reason about and verify more general and abstract properties of plans, and also provides a more holistic programming language infrastructure for modelling plan execution.

KW - AI Planners

KW - Dependent Types

KW - Verification

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

U2 - 10.1145/3471875.3472990

DO - 10.1145/3471875.3472990

M3 - Conference contribution

AN - SCOPUS:85113876893

SP - 1

EP - 13

BT - TyDe 2021: Proceedings of the 6th ACM SIGPLAN International Workshop on Type-Driven Development

A2 - Ko, Hsiang-Shang

A2 - Orchard, Dominic

PB - Association for Computing Machinery

Y2 - 22 August 2021

ER -

Actions you can handle: Dependent types for AI plans

Abstract

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this