## AI helps you reading Science

## AI Insight

AI extracts a summary of this paper

Weibo:

# Finite-memory strategy synthesis for robust multidimensional mean-payoff objectives

CSL-LICS, (2014)

EI

Full Text

Weibo

Keywords

Abstract

Two-player games on graphs provide the mathematical foundation for the study of reactive systems. In the quantitative framework, an objective assigns a value to every play, and the goal of player 1 is to minimize the value of the objective. In this framework, there are two relevant synthesis problems to consider: the quantitative analysis...More

Code:

Data:

Introduction

- In the classical framework of boolean formal verification, a program may only violate or satisfy a given specification, and in the framework of synthesis, the task is to automatically construct a program that satisfies the specification.
- When a one-player solution f is given, the boolean analysis problem amounts to determining whether there is a finite-memory strategy σ such that for every strongly-connected component (SCC) S ∈ Gσ it holds that f (CONVEX (S)) ≤ ν.

Highlights

- In the classical framework of boolean formal verification, a program may only violate or satisfy a given specification, and in the framework of synthesis, the task is to automatically construct a program that satisfies the specification
- From the perspective of synthesis, these problems are most important when player 1 is restricted to finite-memory strategies
- We prove computability for the quantitative synthesis problem, and we show that the boolean analysis problem is inter-reducible with Hilbert’s tenth problem over rationals (H10 (Q)), which is a fundamental long-standing open question in computer science and mathematics
- Theorem 3 The boolean analysis problem for mean-payoff expression games is inter-reducible with H10 (Q), and it is H10 (Q)-hard even for sum-free LimInfAvg-only expressions
- Theorem 4 When both players are restricted to finite-memory strategies: (i) the quantitative analysis problem for mean-payoff expression games is computable; (ii) the boolean analysis problem for mean-payoff expression games is inter-reducible with H10 (Q), and it is H10 (Q)-hard even for sum-free LimInfAvg-only expressions
- From the theoretical point of view, the negative result is a bit surprising since it suggests that the boolean analysis is harder than the optimization problem, and in computer science typically there is a naive reduction from optimization problems to the corresponding decision problems

Results

- If f satisfies Property 4, the problem of determining whether there is a player-1 finite-memory strategy σ such that f (CONVEX (Gσ)) ≤ ν is decidable.
- The one-player solution function of mean-payoff expressions satisfies Properties 1-3 and the theorem follows.
- The authors show that the solution for one-player mean-payoff expression games satisfies Property 4 if and only if H10 (Q) is decidable.
- The authors rely on Lemma 4 and show that player 1 has a winning strategy if and only if there is a finite path π1 that visits only the self-loops of b2 and a path π2 that visits only the self-loops of a2 such that every vector in v ∈ CONVEX (Avg(π1), Avg(π2)) satisfies the winning condition, i.e., if v = (v1, v2, v3, v4, v5), max(v1, min(v2, v3), min(v4, v5)) ≤ 0.
- Theorem 4 When both players are restricted to finite-memory strategies: (i) the quantitative analysis problem for mean-payoff expression games is computable; (ii) the boolean analysis problem for mean-payoff expression games is inter-reducible with H10 (Q), and it is H10 (Q)-hard even for sum-free LimInfAvg-only expressions.
- When both players are restricted to finite-memory strategies, the outcome of a play is an periodic path, and the authors may assume that all the atomic expressions are of the form of LimInfAvg (because for periodic paths the authors have LimInfAvg(π) = LimSupAvg(π)).
- The authors note that while the boolean analysis for sum-free LimInfAvg-only expressions is H10 (Q)-hard when player 1 is restricted to a finite-memory strategy, the lemma shows that the problem is decidable when both players may use arbitrary strategies.
- Lemma 9 (Theorem 5 in [16]) When both players may use arbitrary strategies, the boolean analysis of sum-free LimInfAvg-only expression games is decidable.

Conclusion

- In this work the authors studied the synthesis of finite-memory strategies for games with robust multidimensional mean-payoff objectives, and the authors obtained two main results.
- From a practical point of view, the positive result is the most interesting, since for the first time a recipe is given for computing ǫ-optimal finite-memory strategies for a robust class of quantitative objectives.

Related work

- The class of mean-payoff expressions was introduced in [6], and the decidability of the model checking problems (which correspond to one-player games) was established. A simpler and more efficient algorithm for mean-payoff expression games was given in [15]. Mean-payoff games on multidimensional graphs were first studied in [9]. In these games the objective of player 1 was to satisfy a conjunctive condition (in the terms of this paper, the objective was a maximum of multiple onedimensional objectives). In [16], decidability for an objective that is formed by the min and max operators was established. But the proof can not be extended to include the numerical complement operator, and it does not scale for the case that player 1 is restricted to finite-memory strategies.

Reference

- R. Alur, A. Degorre, O. Maler, and G. Weiss. On omega-languages defined by mean-payoff conditions. FOSSACS, 2009.
- A. Ben-Israel. Motzkins transposition theorem, and the related theorems of farkas, gordan and stiemke. Encyclopaedia of Mathematics, 2001.
- U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman. Temporal specifications with accumulative values. In LICS, 2011.
- T. Brazdil, V. Brozek, K. Chatterjee, V. Forejt, and A. Kucera. Two views on multiple mean-payoff objectives in markov decision processes. In LICS, 2011.
- T. Brazdil, K. Chatterjee, A. Kucera, and P. Novotny. Efficient controller synthesis for consumption games with multiple resource types. In CAV, 2012.
- K. Chatterjee, L. Doyen, H. Edelsbrunner, T. A. Henzinger, and P. Rannou. Mean-payoff automaton expressions. In CONCUR, 2010.
- K. Chatterjee, L. Doyen, and T. A. Henzinger. Expressiveness and closure properties for quantitative languages. LICS, 2009.
- K. Chatterjee, L. Doyen, and T. A. Henzinger. Quantitative languages. ACM Trans. Comput. Log., 2010.
- K. Chatterjee, L. Doyen, T. A. Henzinger, and J.-F. Raskin. Generalized mean-payoff and energy games. In
- K. Chatterjee, M. Randour, and J.-F. Raskin. Strategy synthesis for multi-dimensional quantitative objectives. In CONCUR, 2012.
- M. Droste and G. Rahonis. Weighted automata and weighted logics on infinite words. In Developments in Language Theory, 2006.
- E. Kopczynski. Half-positional determinacy of infinite games. ICALP, 2006.
- A. Tarski. A decision method for elementary algebra and geometry. 1951.
- Y. Velner. The complexity of mean-payoff automaton expression. CoRR, 2011.
- Y. Velner. The complexity of mean-payoff automaton expression. ICALP, 2012.
- Y. Velner and A. Rabinovich. Church synthesis problem for noisy input. In FOSSACS, 2011.
- 0. We replace qi
- 0. We replace pi
- 0. In addition, we add n constraints q1
- 2. For every non-negative rationals m, n: max(min(x1, x2), min(x3, x4)) ≤ 0.
- 2. The weight of dimension 2 + i is −1 and for j ∈ {1,..., n} − {i} the weight of dimensions j is 0. Intuitively, this assures that player 1 will visit edge i at least once.
- 3. If the j-th type-1 equation is m∈I αmqm ≤ 0, then if i ∈ I, then the weight in dimension 2 + n + j is −αm. Otherwise, we assign zero for this dimension. Intuitively, this enforce player 1 to visits edge i for qi times in such way that m∈I αmqm ≤ 0.
- 4. If the j-th type-3 equation is qmpr = qkpl, then the weights of the four dimensions 2 + n + t1 + 4j, 2 + n + t1 + 4j + 1, 2 + n + t1 + 4j + 2, 2 + n + t1 + 4j + 3 are: – If i = m, then the weights are (−1, 0, 1, 0) – If i = k, then the weights are (0, 1, 0, −1) – Otherwise, the weights are (0, 0, 0, 0)
- 2. If the j-th type-2 equation is m∈I αmpm ≤ 0, then if i ∈ I, then the weight in dimension 2 + n + j is −αm. Otherwise, we assign zero for this dimension. Intuitively, this enforce player 1 to visits edge i for pi times in such way that m∈I αmpm ≤ 0.
- 3. If the j-th type-3 equation is qmpr = qkpl, then the weights of the four dimensions 2 + n + t1 + 4j, 2 + n + t1 + 4j + 1, 2 + n + t1 + 4j + 2, 2 + n + t1 + 4j + 3 are: – If i = m, then the weights are (1, 0, −1, 0) – If i = k, then the weights are (0, −1, 0, 1) – Otherwise, the weights are (0, 0, 0, 0)
- 0. We construct the vector v1 ∈ QSI(Gτ1 )

Tags

Comments

数据免责声明

页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果，我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问，可以通过电子邮件方式联系我们：report@aminer.cn