Paper Info
Title
Synthesis from LTL specifications with mean-payoff objectives
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 qualitativeLTL synthesis setting to a quantitative setting. The alphabet of actions is extended with a weight function ranging over the integer 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 LTL$_\textsf{MP}$ synthesis and the LTL$_\textsf{MP}$ realizability problem asks to check whether such a system exists. By reduction to two-player mean-payoff parity games, we first show that LTL$_\textsf{MP}$ realizability is not more difficult than LTL realizability: it is 2ExpTime-Complete. While infinite memory strategies are required to realize LTL$_\textsf{MP}$ specifications in general, we show that ε-optimality can be obtained with finite-memory strategies, for any ε0. To obtain efficient algorithms 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.
Year
DOI
Venue
2013
10.1007/978-3-642-36742-7_12
tools and algorithms for construction and analysis of systems
Keywords
DocType
Volume
latter problem,ltl realizability,safety game,reactive system,classical ltl synthesis problem,ltl specification,realizability problem,mean-payoff objective,ltl formula,finite-memory strategy,qualitativeltl synthesis
Conference
abs/1210.3539
ISSN
Citations 
PageRank 
0302-9743
15
0.57
References 
Authors
20
4
Name
Order
Citations
PageRank
Aaron Bohy1743.21
Véronique Bruyère242943.59
Emmanuel Filiot321724.98
Jean-François Raskin41735100.15