Finite LTL Synthesis with Environment Assumptions and Quality Measures

Alberto Camacho 1 Meghyn Bienvenu 2 Sheila Mcilraith 1
2 GRAPHIK - Graphs for Inferences on Knowledge
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier, CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : In this paper, we investigate the problem of synthesizing strategies for linear temporal logic (LTL) specifications that are interpreted over finite traces - a problem that is central to the automated construction of controllers, robot programs, and business processes. We study a natural variant of the finite LTL synthesis problem in which strategy guarantees are predicated on specified environment behavior. We further explore a quantitative extension of LTL that supports specification of quality measures, utilizing it to synthesize high-quality strategies. We propose new notions of optimality and associated algorithms that yield strategies that best satisfy specified quality measures. Our algorithms utilize an automata-game approach, positioning them well for future implementation via existing state-of-the-art techniques.
Document type :
Conference papers
Complete list of metadatas

Cited literature [5 references]  Display  Hide  Download

https://hal-lirmm.ccsd.cnrs.fr/lirmm-01892548
Contributor : Meghyn Bienvenu <>
Submitted on : Wednesday, October 10, 2018 - 4:26:34 PM
Last modification on : Thursday, October 11, 2018 - 1:19:40 AM

File

CamBieMci-KR18-long.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : lirmm-01892548, version 1
  • ARXIV : 1808.10831

Collections

Citation

Alberto Camacho, Meghyn Bienvenu, Sheila Mcilraith. Finite LTL Synthesis with Environment Assumptions and Quality Measures. KR: Knowledge Representation and Reasoning, Oct 2018, Tempe, United States. ⟨lirmm-01892548⟩

Share

Metrics

Record views

232

Files downloads

26