Synthesizing controllers: On the correspondence between LTL synthesis and non-deterministic planning

6Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.
Get full text

Abstract

Linear Temporal Logic (LTL) synthesis can be understood as the problem of building a controller that defines a winning strategy, for a two-player game against the environment, where the objective is to satisfy a given LTL formula. It is an important problem with applications in software synthesis, including controller synthesis. In this paper we establish the correspondence between LTL synthesis and fully observable non-deterministic (FOND) planning. We study LTL interpreted over both finite and infinite traces. We also provide the first explicit compilation that translates an LTL synthesis problem to a FOND problem. Experiments with state-of-the-art LTL FOND and synthesis solvers show automated planning to be a viable and effective tool for highly structured LTL synthesis problems.

Cite

CITATION STYLE

APA

Camacho, A., Baier, J. A., Muise, C., & McIlraith, S. A. (2018). Synthesizing controllers: On the correspondence between LTL synthesis and non-deterministic planning. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10832 LNAI, pp. 45–59). Springer Verlag. https://doi.org/10.1007/978-3-319-89656-4_4

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free