Temporal planning as refinement-based model checking

Alexander Heinz; Martin Wehrle; Sergiy Bogomolov; Daniele Magazzeni; Marius Greitschus; Andreas Podelski

Temporal planning as refinement-based model checking

Alexander Heinz, Martin Wehrle, Sergiy Bogomolov, Daniele Magazzeni, Marius Greitschus, Andreas Podelski

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

5 Citations (Scopus)

Abstract

Planning as model checking based on source-to-source compilations has found increasing attention. Previously proposed approaches for temporal and hybrid planning are based on static translations, in the sense that the resulting model checking problems are uniquely defined by the given input planning problems. As a drawback, the translations can become too large to be efficiently solvable. In this paper, we address propositional temporal planning, lifting static translations to a more flexible framework. Our framework is based on a refinement cycle that allows for adaptively computing suitable translations of increasing size. Our experiments on temporal IPC domains show that the resulting translations to timed automata often become succinct, resulting in promising performance when applied with the directed model checker MCTA.

Original language	English
Title of host publication	Proceedings of the 29th International Conference on Automated Planning and Scheduling, ICAPS 2019
Editors	J. Benton, Nir Lipovetzky, Eva Onaindia, David E. Smith, Siddharth Srivastava
Publisher	AAAI Press
Pages	195-199
Number of pages	5
ISBN (Electronic)	9781577358077
Publication status	Published - 2019
Event	29th International Conference on Automated Planning and Scheduling, ICAPS 2019 - Berkeley, United States Duration: 11 Jul 2019 → 15 Jul 2019

Publication series

Name	Proceedings International Conference on Automated Planning and Scheduling, ICAPS
ISSN (Print)	2334-0835
ISSN (Electronic)	2334-0843

Conference

Conference	29th International Conference on Automated Planning and Scheduling, ICAPS 2019
Country/Territory	United States
City	Berkeley
Period	11/07/19 → 15/07/19

Cite this

Heinz, A., Wehrle, M., Bogomolov, S., Magazzeni, D., Greitschus, M., & Podelski, A. (2019). Temporal planning as refinement-based model checking. In J. Benton, N. Lipovetzky, E. Onaindia, D. E. Smith, & S. Srivastava (Eds.), Proceedings of the 29th International Conference on Automated Planning and Scheduling, ICAPS 2019 (pp. 195-199). (Proceedings International Conference on Automated Planning and Scheduling, ICAPS). AAAI Press.

Heinz, Alexander ; Wehrle, Martin ; Bogomolov, Sergiy et al. / Temporal planning as refinement-based model checking. Proceedings of the 29th International Conference on Automated Planning and Scheduling, ICAPS 2019. editor / J. Benton ; Nir Lipovetzky ; Eva Onaindia ; David E. Smith ; Siddharth Srivastava. AAAI Press, 2019. pp. 195-199 (Proceedings International Conference on Automated Planning and Scheduling, ICAPS).

@inproceedings{e19aeac6e60c4a61b3181142c53d351c,

title = "Temporal planning as refinement-based model checking",

abstract = "Planning as model checking based on source-to-source compilations has found increasing attention. Previously proposed approaches for temporal and hybrid planning are based on static translations, in the sense that the resulting model checking problems are uniquely defined by the given input planning problems. As a drawback, the translations can become too large to be efficiently solvable. In this paper, we address propositional temporal planning, lifting static translations to a more flexible framework. Our framework is based on a refinement cycle that allows for adaptively computing suitable translations of increasing size. Our experiments on temporal IPC domains show that the resulting translations to timed automata often become succinct, resulting in promising performance when applied with the directed model checker MCTA.",

author = "Alexander Heinz and Martin Wehrle and Sergiy Bogomolov and Daniele Magazzeni and Marius Greitschus and Andreas Podelski",

note = "Publisher Copyright: {\textcopyright} 2019, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.; 29th International Conference on Automated Planning and Scheduling, ICAPS 2019 ; Conference date: 11-07-2019 Through 15-07-2019",

year = "2019",

language = "English",

series = "Proceedings International Conference on Automated Planning and Scheduling, ICAPS",

publisher = "AAAI Press",

pages = "195--199",

editor = "J. Benton and Nir Lipovetzky and Eva Onaindia and Smith, {David E.} and Siddharth Srivastava",

booktitle = "Proceedings of the 29th International Conference on Automated Planning and Scheduling, ICAPS 2019",

}

Heinz, A, Wehrle, M, Bogomolov, S, Magazzeni, D, Greitschus, M & Podelski, A 2019, Temporal planning as refinement-based model checking. in J Benton, N Lipovetzky, E Onaindia, DE Smith & S Srivastava (eds), Proceedings of the 29th International Conference on Automated Planning and Scheduling, ICAPS 2019. Proceedings International Conference on Automated Planning and Scheduling, ICAPS, AAAI Press, pp. 195-199, 29th International Conference on Automated Planning and Scheduling, ICAPS 2019, Berkeley, United States, 11/07/19.

Temporal planning as refinement-based model checking. / Heinz, Alexander; Wehrle, Martin; Bogomolov, Sergiy et al.
Proceedings of the 29th International Conference on Automated Planning and Scheduling, ICAPS 2019. ed. / J. Benton; Nir Lipovetzky; Eva Onaindia; David E. Smith; Siddharth Srivastava. AAAI Press, 2019. p. 195-199 (Proceedings International Conference on Automated Planning and Scheduling, ICAPS).

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

TY - GEN

T1 - Temporal planning as refinement-based model checking

AU - Heinz, Alexander

AU - Wehrle, Martin

AU - Bogomolov, Sergiy

AU - Magazzeni, Daniele

AU - Greitschus, Marius

AU - Podelski, Andreas

PY - 2019

Y1 - 2019

N2 - Planning as model checking based on source-to-source compilations has found increasing attention. Previously proposed approaches for temporal and hybrid planning are based on static translations, in the sense that the resulting model checking problems are uniquely defined by the given input planning problems. As a drawback, the translations can become too large to be efficiently solvable. In this paper, we address propositional temporal planning, lifting static translations to a more flexible framework. Our framework is based on a refinement cycle that allows for adaptively computing suitable translations of increasing size. Our experiments on temporal IPC domains show that the resulting translations to timed automata often become succinct, resulting in promising performance when applied with the directed model checker MCTA.

AB - Planning as model checking based on source-to-source compilations has found increasing attention. Previously proposed approaches for temporal and hybrid planning are based on static translations, in the sense that the resulting model checking problems are uniquely defined by the given input planning problems. As a drawback, the translations can become too large to be efficiently solvable. In this paper, we address propositional temporal planning, lifting static translations to a more flexible framework. Our framework is based on a refinement cycle that allows for adaptively computing suitable translations of increasing size. Our experiments on temporal IPC domains show that the resulting translations to timed automata often become succinct, resulting in promising performance when applied with the directed model checker MCTA.

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

M3 - Conference Paper

T3 - Proceedings International Conference on Automated Planning and Scheduling, ICAPS

SP - 195

EP - 199

BT - Proceedings of the 29th International Conference on Automated Planning and Scheduling, ICAPS 2019

A2 - Benton, J.

A2 - Lipovetzky, Nir

A2 - Onaindia, Eva

A2 - Smith, David E.

A2 - Srivastava, Siddharth

PB - AAAI Press

T2 - 29th International Conference on Automated Planning and Scheduling, ICAPS 2019

Y2 - 11 July 2019 through 15 July 2019

ER -

Heinz A, Wehrle M, Bogomolov S, Magazzeni D, Greitschus M, Podelski A. Temporal planning as refinement-based model checking. In Benton J, Lipovetzky N, Onaindia E, Smith DE, Srivastava S, editors, Proceedings of the 29th International Conference on Automated Planning and Scheduling, ICAPS 2019. AAAI Press. 2019. p. 195-199. (Proceedings International Conference on Automated Planning and Scheduling, ICAPS).

Temporal planning as refinement-based model checking

Abstract

Publication series

Conference

Other files and links

Fingerprint

Cite this