AAAI Publications, Sixteenth International Conference on Principles of Knowledge Representation and Reasoning

Font Size: 
Finite LTL Synthesis with Environment Assumptions and Quality Measures
Alberto Camacho, Meghyn Bienvenu, Sheila A. McIlraith

Last modified: 2018-09-24


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.


Synthesis; Linear Temporal Logic; LTL; Quality

Full Text: PDF