AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
We study for the first time the strategy synthesis problems for games with robust quantitative objectives, namely, games with mean-payoff expression objectives

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

CSL-LICS, (2014)

Cited by: 4|Views141
EI

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:

0
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.
    Google ScholarLocate open access versionFindings
  • A. Ben-Israel. Motzkins transposition theorem, and the related theorems of farkas, gordan and stiemke. Encyclopaedia of Mathematics, 2001.
    Google ScholarLocate open access versionFindings
  • U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman. Temporal specifications with accumulative values. In LICS, 2011.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • T. Brazdil, K. Chatterjee, A. Kucera, and P. Novotny. Efficient controller synthesis for consumption games with multiple resource types. In CAV, 2012.
    Google ScholarLocate open access versionFindings
  • K. Chatterjee, L. Doyen, H. Edelsbrunner, T. A. Henzinger, and P. Rannou. Mean-payoff automaton expressions. In CONCUR, 2010.
    Google ScholarLocate open access versionFindings
  • K. Chatterjee, L. Doyen, and T. A. Henzinger. Expressiveness and closure properties for quantitative languages. LICS, 2009.
    Google ScholarLocate open access versionFindings
  • K. Chatterjee, L. Doyen, and T. A. Henzinger. Quantitative languages. ACM Trans. Comput. Log., 2010.
    Google ScholarLocate open access versionFindings
  • K. Chatterjee, L. Doyen, T. A. Henzinger, and J.-F. Raskin. Generalized mean-payoff and energy games. In
    Google ScholarLocate open access versionFindings
  • K. Chatterjee, M. Randour, and J.-F. Raskin. Strategy synthesis for multi-dimensional quantitative objectives. In CONCUR, 2012.
    Google ScholarLocate open access versionFindings
  • M. Droste and G. Rahonis. Weighted automata and weighted logics on infinite words. In Developments in Language Theory, 2006.
    Google ScholarLocate open access versionFindings
  • E. Kopczynski. Half-positional determinacy of infinite games. ICALP, 2006.
    Google ScholarLocate open access versionFindings
  • A. Tarski. A decision method for elementary algebra and geometry. 1951.
    Google ScholarFindings
  • Y. Velner. The complexity of mean-payoff automaton expression. CoRR, 2011.
    Google ScholarLocate open access versionFindings
  • Y. Velner. The complexity of mean-payoff automaton expression. ICALP, 2012.
    Google ScholarLocate open access versionFindings
  • Y. Velner and A. Rabinovich. Church synthesis problem for noisy input. In FOSSACS, 2011.
    Google ScholarLocate open access versionFindings
  • 0. We replace qi
    Google ScholarFindings
  • 0. We replace pi
    Google ScholarFindings
  • 0. In addition, we add n constraints q1
    Google ScholarFindings
  • 2. For every non-negative rationals m, n: max(min(x1, x2), min(x3, x4)) ≤ 0.
    Google ScholarFindings
  • 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.
    Google ScholarFindings
  • 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.
    Google ScholarFindings
  • 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)
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarFindings
  • 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)
    Google ScholarFindings
  • 0. We construct the vector v1 ∈ QSI(Gτ1 )
    Google ScholarFindings
Author
Your rating :
0

 

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