We study the following refinement relation between nondeterministic state-transition models: model B strategically dominates model A iff every deterministic refinement of A is language contained in some deterministic refinement of B. While language containment is trace inclusion, and the (fair) simulation preorder coincides with tree inclusion, strategic dominance falls strictly between the two and can be characterized as "strategy inclusion" between A and B: every strategy that resolves the nondeterminism of A is dominated by a strategy that resolves the nondeterminism of B. Strategic dominance can be checked in 2-ExpTime by a decidable first-order Presburger logic with quantification over words and strategies, called resolver logic. We give several other applications of resolver logic, including checking the co-safety, co-liveness, and history-determinism of boolean and quantitative automata, and checking the inclusion between hyperproperties that are specified by nondeterministic boolean and quantitative automata.

翻译：我们研究非确定性状态转移模型之间的如下精化关系：模型B策略支配模型A当且仅当A的每个确定性精化在语言上包含于B的某个确定性精化中。语言包含即迹包含，而（公平）模拟预序等价于树包含，策略支配则严格介于两者之间，可表征为A与B之间的“策略包含”：每个消解A非确定性的策略都被某个消解B非确定性的策略所支配。策略支配可通过一种可判定的、允许对词和策略进行量词化的一阶Presburger逻辑（称为解析器逻辑）在2-ExpTime内判定。我们给出了解析器逻辑的其他若干应用，包括检验布尔与定量自动机的共安全性、共活性及历史确定性，以及检验由非确定性布尔与定量自动机指定的超属性之间的包含关系。