Skip to Main content Skip to Navigation
Conference papers

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 [25 references]  Display  Hide  Download
Contributor : Meghyn Bienvenu <>
Submitted on : Wednesday, October 10, 2018 - 4:26:34 PM
Last modification on : Friday, March 13, 2020 - 4:14:04 PM


Files produced by the author(s)


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



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⟩



Record views


Files downloads