Goal-constrained planning domain model verification of safety properties

Anas Shrinah; Kerstin I Eder

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 proceeding › Conference Contribution (Conference Proceeding)

49 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 language	English
Title of host publication	Goal-constrained planning domain model verification of safety properties
Editors	Sebastian Rudolph, Goreti Marreiros
Publisher	CEUR Workshop Proceedings
Volume	2655
Publication status	Published - 26 Aug 2020
Event	European Starting AI Researchers' Symposium 2020 - Santiago Compostela, Spain Duration: 29 Aug 2020 → 30 Aug 2020 Conference number: 9

Publication series

Name	European Starting AI Researchers' Symposium 2020
Publisher	CEUR Workshop Proceedings
Volume	2655
ISSN (Electronic)	1613-0073

Conference

Conference	European Starting AI Researchers' Symposium 2020
Abbreviated title	STAIRS 2020
Country/Territory	Spain
City	Santiago Compostela
Period	29/08/20 → 30/08/20

Access to Document

Full-text PDF (final published version)
This is the final published version of the article (version of record). It first appeared online via CEUR at http://ceur-ws.org/Vol-2655/. Please refer to any applicable terms of use of the publisher.
Final published version, 384 KBLicence: CC BY

http://ceur-ws.org/Vol-2655/

Handle.net

Persistent link

Cite this

@inproceedings{9c238bcf6ac24a7b8890735c6f034e5d,

title = "Goal-constrained planning domain model verification of safety properties",

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

author = "Anas Shrinah and Eder, {Kerstin I}",

year = "2020",

month = aug,

day = "26",

language = "English",

volume = "2655",

series = "European Starting AI Researchers' Symposium 2020",

publisher = "CEUR Workshop Proceedings",

editor = "Sebastian Rudolph and Goreti Marreiros",

booktitle = "Goal-constrained planning domain model verification of safety properties",

note = "European Starting AI Researchers' Symposium 2020, STAIRS 2020 ; Conference date: 29-08-2020 Through 30-08-2020",

}

Shrinah, A & Eder, KI 2020, Goal-constrained planning domain model verification of safety properties. in S Rudolph & G Marreiros (eds), Goal-constrained planning domain model verification of safety properties. vol. 2655, European Starting AI Researchers' Symposium 2020, vol. 2655, CEUR Workshop Proceedings, European Starting AI Researchers' Symposium 2020, Santiago Compostela, Spain, 29/08/20. <http://ceur-ws.org/Vol-2655/>

Goal-constrained planning domain model verification of safety properties. / Shrinah, Anas ; Eder, Kerstin I.

Goal-constrained planning domain model verification of safety properties. ed. / Sebastian Rudolph; Goreti Marreiros. Vol. 2655 CEUR Workshop Proceedings, 2020. (European Starting AI Researchers' Symposium 2020; Vol. 2655).

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

TY - GEN

T1 - Goal-constrained planning domain model verification of safety properties

AU - Shrinah, Anas

AU - Eder, Kerstin I

N1 - Conference code: 9

PY - 2020/8/26

Y1 - 2020/8/26

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

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

M3 - Conference Contribution (Conference Proceeding)

VL - 2655

T3 - European Starting AI Researchers' Symposium 2020

BT - Goal-constrained planning domain model verification of safety properties

A2 - Rudolph, Sebastian

A2 - Marreiros, Goreti

PB - CEUR Workshop Proceedings

T2 - European Starting AI Researchers' Symposium 2020

Y2 - 29 August 2020 through 30 August 2020

ER -

Goal-constrained planning domain model verification of safety properties

Abstract

Publication series

Conference

Access to Document

Handle.net

Fingerprint

Cite this