A temporal logic with mean-payoff constraints

Abstract

In the quantitative verification and synthesis of reactive systems, the states or transitions of a system are associated with payoffs, and a quantitative property of a behavior of the system is often characterized by the mean payoff for the behavior. This paper proposes an extension of LTL thatdescribes mean-payoff constraints. For each step of a behavior of a system, the payment depends on a system transition and a temporal property of the behavior. A mean-payoff constraint is a threshold condition for the limit supremum or limit infimum of the mean payoffs of a behavior. This extension allows us to describe specifications reflecting qualitative and quantitative requirements on long-run average of costs and the frequencies of satisfaction of temporal properties. Moreover, we develop an algorithm for the emptiness problems of multi-dimensional payoff automata with Büchi acceptance conditions and multi-threshold mean-payoff acceptance conditions. The emptiness problems are decided by solving linear constraint satisfaction problems, and the decision problems of our logic are reduced to the emptiness problems. Consequently, we obtain exponential-time algorithms for the model- and satisfiability-checking of the logic. Some optimization problems of the logic can also be reduced to linear programming problems. © 2012 Springer-Verlag.