Verifying Belief-based Programs via Symbolic Dynamic Programming

Daxin Liu; Qinfei Huang; Vaishak Belle; Gerhard Lakemeyer

doi:10.3233/FAIA230429

Verifying Belief-based Programs via Symbolic Dynamic Programming

Daxin Liu^*, Qinfei Huang, Vaishak Belle, Gerhard Lakemeyer

^*Corresponding author for this work

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

Abstract / Description of output

Belief-based programming is a probabilistic extension of the Golog programming language family, where every action and sensing could be noisy and every test refers to the agent’s subjective beliefs. Such characteristics make it rather suitable for robot control in a partial-observable uncertain environment. Recently, efforts have been made in providing formal semantics for belief programs and investigating the hardness of verifying belief programs. Nevertheless, a general algorithm that actually conducts the verification is missing. In this paper, we propose an algorithm based on symbolic dynamic programming to verify belief programs, an approach that generalizes the dynamic programming technique for solving (partially observable) Markov decision processes, i.e. (PO)MDP, by exploiting the symbolic structure in the solution of first-order (PO)MDPs induced by belief program execution.

Original language	English
Title of host publication	Proceedings of the 26th European Conference on Artificial Intelligence
Publisher	IOS Press
Pages	1497-1504
Number of pages	8
Volume	372
ISBN (Electronic)	9781643684376
ISBN (Print)	9781643684369
DOIs	https://doi.org/10.3233/FAIA230429
Publication status	Published - 1 Oct 2023
Event	26th European Conference on Artificial Intelligence - ICE Kraków Congress Centre, Kraków, Poland Duration: 30 Sept 2023 → 5 Oct 2023 https://ecai2023.eu/

Publication series

Name	Frontiers in Artificial Intelligence and Applications
Publisher	IOS Press
Volume	372
ISSN (Print)	0922-6389
ISSN (Electronic)	1879-8314

Conference

Conference	26th European Conference on Artificial Intelligence
Abbreviated title	ECAI 2023
Country/Territory	Poland
City	Kraków
Period	30/09/23 → 5/10/23
Internet address	https://ecai2023.eu/

Keywords / Materials (for Non-textual outputs)

Knowledge representation
program verification
first-order POMDP
belief program

Access to Document

10.3233/FAIA230429Licence: Creative Commons: Attribution Non-Commercial (CC-BY-NC)

Verifying Belief-based_LIU_DOA15072023_AFV_CC BYAccepted author manuscript, 629 KBLicence: Creative Commons: Attribution (CC-BY)
Verifying Belief-based_LIU_DOA15072023_VOR_CC BY-NCFinal published version, 433 KBLicence: Creative Commons: Attribution Non-Commercial (CC-BY-NC)

https://ebooks.iospress.nl/volumearticle/64361Licence: Creative Commons: Attribution Non-Commercial (CC-BY-NC)

1 Finished

UKRI Trustworthy Autonomous Systems Node in Governance and Regulation
Ramamoorthy, R., Belle, V., Bundy, A., Jackson, P., Lascarides, A. & Rajan, A.
EPSRC
1/11/20 → 30/04/24
Project: Research

2 Conference contribution

First-order progression beyond local-effect and normal actions
Liu, D. & Claßen, J., 14 May 2024, (Accepted/In press) Proceedings of the 33rd International Joint Conference on Artificial Intelligence. IJCAI Organization
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Open Access
File
Progression with probabilities in the Situation Calculus: Representation and succinctness
Liu, D. & Belle, V., 6 May 2024, Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems. ACM, p. 1210-1218 9 p.
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Open Access
File

Cite this

@inproceedings{778703c0b6ca4ad7aa2b56d64c9de2e0,

title = "Verifying Belief-based Programs via Symbolic Dynamic Programming",

abstract = "Belief-based programming is a probabilistic extension of the Golog programming language family, where every action and sensing could be noisy and every test refers to the agent{\textquoteright}s subjective beliefs. Such characteristics make it rather suitable for robot control in a partial-observable uncertain environment. Recently, efforts have been made in providing formal semantics for belief programs and investigating the hardness of verifying belief programs. Nevertheless, a general algorithm that actually conducts the verification is missing. In this paper, we propose an algorithm based on symbolic dynamic programming to verify belief programs, an approach that generalizes the dynamic programming technique for solving (partially observable) Markov decision processes, i.e. (PO)MDP, by exploiting the symbolic structure in the solution of first-order (PO)MDPs induced by belief program execution. ",

keywords = "Knowledge representation, program verification, first-order POMDP, belief program",

author = "Daxin Liu and Qinfei Huang and Vaishak Belle and Gerhard Lakemeyer",

note = "This research was supported partly by a Royal Society University Research Fellowship, UK, partly by a grant from the UKRI Strategic Priorities Fund, UK to the UKRI Research Node on Trustworthy Autonomous Systems Governance and Regulation (EP/V026607/1, 2020–2024), partly by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) RTG 2236/2 {\textquoteleft}UnRAVeL{\textquoteright}, and partly by the EU ICT-48 2020 project TAILOR (No. 952215).; 26th European Conference on Artificial Intelligence, ECAI 2023 ; Conference date: 30-09-2023 Through 05-10-2023",

year = "2023",

month = oct,

day = "1",

doi = "10.3233/FAIA230429",

language = "English",

isbn = "9781643684369",

volume = "372",

series = "Frontiers in Artificial Intelligence and Applications",

publisher = "IOS Press",

pages = "1497--1504",

booktitle = "Proceedings of the 26th European Conference on Artificial Intelligence",

url = "https://ecai2023.eu/",

}

Liu, D, Huang, Q, Belle, V & Lakemeyer, G 2023, Verifying Belief-based Programs via Symbolic Dynamic Programming. in Proceedings of the 26th European Conference on Artificial Intelligence. vol. 372, Frontiers in Artificial Intelligence and Applications, vol. 372, IOS Press, pp. 1497-1504, 26th European Conference on Artificial Intelligence, Kraków, Poland, 30/09/23. https://doi.org/10.3233/FAIA230429

Verifying Belief-based Programs via Symbolic Dynamic Programming. / Liu, Daxin; Huang, Qinfei; Belle, Vaishak et al.
Proceedings of the 26th European Conference on Artificial Intelligence. Vol. 372 IOS Press, 2023. p. 1497-1504 (Frontiers in Artificial Intelligence and Applications; Vol. 372).

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

TY - GEN

T1 - Verifying Belief-based Programs via Symbolic Dynamic Programming

AU - Liu, Daxin

AU - Huang, Qinfei

AU - Belle, Vaishak

AU - Lakemeyer, Gerhard

N1 - This research was supported partly by a Royal Society University Research Fellowship, UK, partly by a grant from the UKRI Strategic Priorities Fund, UK to the UKRI Research Node on Trustworthy Autonomous Systems Governance and Regulation (EP/V026607/1, 2020–2024), partly by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) RTG 2236/2 ‘UnRAVeL’, and partly by the EU ICT-48 2020 project TAILOR (No. 952215).

PY - 2023/10/1

Y1 - 2023/10/1

N2 - Belief-based programming is a probabilistic extension of the Golog programming language family, where every action and sensing could be noisy and every test refers to the agent’s subjective beliefs. Such characteristics make it rather suitable for robot control in a partial-observable uncertain environment. Recently, efforts have been made in providing formal semantics for belief programs and investigating the hardness of verifying belief programs. Nevertheless, a general algorithm that actually conducts the verification is missing. In this paper, we propose an algorithm based on symbolic dynamic programming to verify belief programs, an approach that generalizes the dynamic programming technique for solving (partially observable) Markov decision processes, i.e. (PO)MDP, by exploiting the symbolic structure in the solution of first-order (PO)MDPs induced by belief program execution.

AB - Belief-based programming is a probabilistic extension of the Golog programming language family, where every action and sensing could be noisy and every test refers to the agent’s subjective beliefs. Such characteristics make it rather suitable for robot control in a partial-observable uncertain environment. Recently, efforts have been made in providing formal semantics for belief programs and investigating the hardness of verifying belief programs. Nevertheless, a general algorithm that actually conducts the verification is missing. In this paper, we propose an algorithm based on symbolic dynamic programming to verify belief programs, an approach that generalizes the dynamic programming technique for solving (partially observable) Markov decision processes, i.e. (PO)MDP, by exploiting the symbolic structure in the solution of first-order (PO)MDPs induced by belief program execution.

KW - Knowledge representation

KW - program verification

KW - first-order POMDP

KW - belief program

U2 - 10.3233/FAIA230429

DO - 10.3233/FAIA230429

M3 - Conference contribution

SN - 9781643684369

VL - 372

T3 - Frontiers in Artificial Intelligence and Applications

SP - 1497

EP - 1504

BT - Proceedings of the 26th European Conference on Artificial Intelligence

PB - IOS Press

T2 - 26th European Conference on Artificial Intelligence

Y2 - 30 September 2023 through 5 October 2023

ER -

Verifying Belief-based Programs via Symbolic Dynamic Programming

Abstract / Description of output

Publication series

Conference

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Projects

UKRI Trustworthy Autonomous Systems Node in Governance and Regulation

Research output

First-order progression beyond local-effect and normal actions

Progression with probabilities in the Situation Calculus: Representation and succinctness

Cite this