Strategy logic (SL) is a powerful temporal logic that enables strategic
reasoning in multi-agent systems. SL supports explicit (first-order)
quantification over strategies and provides a logical framework to express many
important properties such as Nash equilibria, dominant strategies, etc. While
in SL the same strategy can be used in multiple strategy profiles, each such
profile is evaluated w.r.t. a path-property, i.e., a property that considers
the single path resulting from a particular strategic interaction. In this
paper, we present Hyper Strategy Logic (HyperSL), a strategy logic where the
outcome of multiple strategy profiles can be compared w.r.t. a hyperproperty,
i.e., a property that relates multiple paths. We show that HyperSL can capture
important properties that cannot be expressed in SL, including
non-interference, quantitative Nash equilibria, optimal adversarial planning,
and reasoning under imperfect information. On the algorithmic side, we identify
an expressive fragment of HyperSL with decidable model checking and present a
model-checking algorithm. We contribute a prototype implementation of our
algorithm and report on encouraging experimental results.

提出了 Hyper Strategy Logic（HyperSL）作为多路径比较的战略逻辑，并给出了该逻辑的模型检查算法和实现。

超级策略逻辑

Hyper Strategy Logic

Discounting is an important dimension in multi-agent systems as long as we
want to reason about strategies and time. It is a key aspect in economics as it
captures the intuition that the far-away future is not as important as the near
future. Traditional verification techniques allow to check whether there is a
winning strategy for a group of agents but they do not take into account the
fact that satisfying a goal sooner is different from satisfying it after a long
wait. In this paper, we augment Strategy Logic with future discounting over a
set of discounted functions D, denoted SLdisc[D]. We consider "until" operators
with discounting functions: the satisfaction value of a specification in
SLdisc[D] is a value in [0, 1], where the longer it takes to fulfill
requirements, the smaller the satisfaction value is. We motivate our approach
with classical examples from Game Theory and study the complexity of
model-checking SLdisc[D]-formulas.

本文将未来折扣引入策略逻辑中，并研究了 SLdisc [D]-formula 的模型检查。

策略逻辑中的折扣

Discounting in Strategy Logic

We introduce an extension of Strategy Logic for the imperfect-information
setting, called SLii, and study its model-checking problem. As this logic
naturally captures multi-player games with imperfect information, this problem
is undecidable; but we introduce a syntactical class of "hierarchical
instances" for which, intuitively, as one goes down the syntactic tree of the
formula, strategy quantifications are concerned with finer observations of the
model, and we prove that model-checking SLii restricted to hierarchical
instances is decidable. To establish this result we go through QCTL, an
intermediary, "low-level" logic much more adapted to automata techniques. QCTL
is an extension of CTL with second-order quantification over atomic
propositions. We extend it to the imperfect information setting by
parameterising second-order quantifiers with observations. While the
model-checking problem of QCTLii is, in general, undecidable, we identify a
syntactic fragment of hierarchical formulas and prove, using an
automata-theoretic approach, that it is decidable. We apply our result to solve
complex strategic problems in the imperfect-information setting. We first show
that the existence of Nash equilibria for deterministic strategies is decidable
in games with hierarchical information. We also introduce distributed rational
synthesis, a generalisation of rational synthesis to the imperfect-information
setting. Because it can easily be expressed in our logic, our main result
provides solution to this problem in the case of hierarchical information.

研究不完美信息领域中策略逻辑的 SLii 扩展，并研究其模型检查问题，证明其限制为分层实例的模型检查是可判定的，应用此结果解决了分层信息下确定性策略的纳什均衡存在性可判定问题和分布式合理综合问题。

有限信息下的策略逻辑

Strategy Logic with Imperfect Information

In open systems verification, to formally check for reliability, one needs an
appropriate formalism to model the interaction between agents and express the
correctness of the system no matter how the environment behaves. An important
contribution in this context is given by modal logics for strategic ability, in
the setting of multi-agent games, such as ATL, ATL\star, and the like.
Recently, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, which
we denote here by CHP-SL, with the aim of getting a powerful framework for
reasoning explicitly about strategies. CHP-SL is obtained by using first-order
quantifications over strategies and has been investigated in the very specific
setting of two-agents turned-based games, where a non-elementary model-checking
algorithm has been provided. While CHP-SL is a very expressive logic, we claim
that it does not fully capture the strategic aspects of multi-agent systems. In
this paper, we introduce and study a more general strategy logic, denoted SL,
for reasoning about strategies in multi-agent concurrent games. We prove that
SL includes CHP-SL, while maintaining a decidable model-checking problem. In
particular, the algorithm we propose is computationally not harder than the
best one known for CHP-SL. Moreover, we prove that such a problem for SL is
NonElementarySpace-hard. This negative result has spurred us to investigate
here syntactic fragments of SL, strictly subsuming ATL\star, with the hope of
obtaining an elementary model-checking problem. Among the others, we study the
sublogics SL[NG], SL[BG], and SL[1G]. They encompass formulas in a special
prenex normal form having, respectively, nested temporal goals, Boolean
combinations of goals and, a single goal at a time. About these logics, we
prove that the model-checking problem for SL[1G] is 2ExpTime-complete, thus not
harder than the one for ATL\star.

介绍了一种更广泛的策略逻辑，用于在多代理并发游戏中推理策略，证明了其包括 CHP-SL，同时维护可决策模型检查问题。