Synthesis from LTL specifications with mean-payoff objectives

DOI10.1007/978-3-642-36742-7_12zbMATH Open1381.68149arXiv1210.3539OpenAlexW1782528461MaRDI QIDQ5326323FDOQ5326323

Authors: Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Jean-François Raskin 

Publication date: 5 August 2013

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Abstract: The classical LTL synthesis problem is purely qualitative: the given LTL specification is realized or not by a reactive system. LTL is not expressive enough to formalize the correctness of reactive systems with respect to some quantitative aspects. This paper extends the qualitative LTL synthesis setting to a quantitative setting. The alphabet of actions is extended with a weight function ranging over the rational numbers. The value of an infinite word is the mean-payoff of the weights of its letters. The synthesis problem then amounts to automatically construct (if possible) a reactive system whose executions all satisfy a given LTL formula and have mean-payoff values greater than or equal to some given threshold. The latter problem is called LTLMP synthesis and the LTLMP realizability problem asks to check whether such a system exists. We first show that LTLMP realizability is not more difficult than LTL realizability: it is 2ExpTime-Complete. This is done by reduction to two-player mean-payoff parity games. While infinite memory strategies are required to realize LTLMP specifications in general, we show that epsilon-optimality can be obtained with finite memory strategies, for any epsilon > 0. To obtain an efficient algorithm in practice, we define a Safraless procedure to decide whether there exists a finite-memory strategy that realizes a given specification for some given threshold. This procedure is based on a reduction to two-player energy safety games which are in turn reduced to safety games. Finally, we show that those safety games can be solved efficiently by exploiting the structure of their state spaces and by using antichains as a symbolic data-structure. All our results extend to multi-dimensional weights. We have implemented an antichain-based procedure and we report on some promising experimental results.

Full work available at URL: https://arxiv.org/abs/1210.3539

Recommendations

• Better Quality in Synthesis through Quantitative Objectives
• Safraless LTL synthesis considering maximal realizability
• Compositional algorithms for LTL synthesis
• Tools and Algorithms for the Construction and Analysis of Systems
• Antichains and compositional algorithms for LTL synthesis

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cited In (25)

• An Antichain Algorithm for LTL Realizability
• Synthesis from component libraries with costs
• Title not available (Why is that?)
• Average-energy games
• Fairness, assumptions, and guarantees for extended bounded response \textsf{LTL+P} synthesis
• A Hybrid Algorithm for LTL Games
• Hyperplane separation technique for multidimensional mean-payoff games
• Looking at mean-payoff and total-payoff through windows
• Antichains and compositional algorithms for LTL synthesis
• Semantic labelling and learning for parity game solving in LTL synthesis
• Program repair without regret
• Synthesis for multi-weighted games with branching-time winning conditions
• Minimizing expected cost under hard Boolean constraints, with applications to quantitative synthesis
• Synthesis with privacy against an observer
• Solving mean-payoff games via quasi dominions
• Safraless LTL synthesis considering maximal realizability
• Latticed-LTL synthesis in the presence of noisy inputs
• Solving mean-payoff games via quasi dominions
• Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes
• Maximum realizability for linear temporal logic specifications
• Qualitative analysis of concurrent mean-payoff games
• Tools and Algorithms for the Construction and Analysis of Systems
• Model checking and synthesis for branching multi-weighted logics
• Latticed-LTL synthesis in the presence of noisy inputs
• Quantitative fair simulation games

This page was built for publication: Synthesis from LTL specifications with mean-payoff objectives

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5326323)