Goal-constrained planning domain model verification of safety properties

Anas Shrinah*, Kerstin I Eder*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

9 Downloads (Pure)

Abstract

The verification of planning domain models is crucial to ensure the safety, integrity and correctness of planning-based automated systems. This task is usually performed using model checking techniques. However, unconstrained application of model checkers to verify planning domain models can result in false positives, i.e. counterexamples that are unreachable by a sound planner when using the domain under verification during a planning task. In this paper, we discuss the downside of unconstrained planning domain model verification. We then introduce the notion of a valid planning counterexample, and demonstrate how model checkers, as well as state trajectory constraints planning techniques, should be used to verify planning domain models so that invalid planning counterexamples are not returned.
Original languageEnglish
Title of host publicationGoal-constrained planning domain model verification of safety properties
EditorsSebastian Rudolph, Goreti Marreiros
PublisherCEUR Workshop Proceedings
Volume2655
Publication statusPublished - 26 Aug 2020
EventEuropean Starting AI Researchers' Symposium 2020 - Santiago Compostela, Spain
Duration: 29 Aug 202030 Aug 2020
Conference number: 9

Publication series

NameEuropean Starting AI Researchers' Symposium 2020
PublisherCEUR Workshop Proceedings
Volume2655
ISSN (Electronic)1613-0073

Conference

ConferenceEuropean Starting AI Researchers' Symposium 2020
Abbreviated titleSTAIRS 2020
CountrySpain
CitySantiago Compostela
Period29/08/2030/08/20

Fingerprint Dive into the research topics of 'Goal-constrained planning domain model verification of safety properties'. Together they form a unique fingerprint.

Cite this