随着程序语言的进步，从以前的汇编语言到现今的高度抽象化的程序语言，造就了越来越复杂的软件系统，因此我们亟需要自动化的方法来帮助我们分析这样的软件系统。软件系统其中的一支系统，反应系统（Reactive System），由于必须和环境不断的互动，因此环境的不确定性使得反应系统的行为更加的难以分析与预测。而赛局理论恰巧是探讨两个以上行为决策者的学科，所以直觉上赛局理论很适合拿来做这种系统的分析。

赛局理论自从在二十世纪初开始有系统的研究以来，已经在生物学，经济学，国际关系，政治学，军事理论等许多领域越来越受到重视并且有了很广泛的应用，而且赛局理论也渐渐的被应用在计算器科学中的许多领域，如人工智能（Artificial Intelligence ）、分布式系统（Distributed System）、反应系统（Reactive system）、优化求解（Optimization）和模型检验（Model checking）等问题。在本文中，我们将介绍数种用来分析反应系统的赛局，和它们所适用的情境。

在计算器科学里，我们可以用图形（Graph）的方式来表示一个系统。在图上，节点（vertex）代表系统的状态，边（edge）代表了从一个状态到另一个状态的转换。而用来表示反应系统时，节点可以更进一步的区分为系统的节点以及环境的节点，因此从系统的节点连出去的边就代表了受控制的行为，系统可以藉由选择其中一个边，而明确的知道系统的下一个状态；而从环境的节点连出去的边，代表不受控制的行为，所以在环境做出选择之前，并无法知道下一个系统状态是什么。

正规上来说，我们会定义一个双人玩的赛局图（Game graph）G＝（V1, V2, E1, E2）来模型化一个反应系统。在 G中V1代表玩家1的节点，V2代表玩家2的节点，

E1：V1×V2是从V1节点到V2节点的边，代表受玩家1所控制的选择，E2：V2×V1是从V2节点到V1节点的边，代表不受玩家1所控制的选择。由于反应系统是不断的和环境做互动，所以系统和环境之间形成的赛局，都是没有结束的赛局，也就是说V1和V2中的节点，一定至少会有一个向外的边。除了提供赛局图来当作赛局的比赛场所之外，赛局中还必须定义了怎样子叫做赢了一场赛局，也就是说每一个赛局都必须定义他的求解概念（solution concept）。注意：以下所介绍的赛局，皆为完全信息并且是回合制的赛局。

《图一 有限图上的一个赛局》

为了能更简洁的介绍各种赛局，我们先定义了以下几个术语：

接下来我们将介绍几种常见的赛局，和它们的求解概念。

无可避免型（Inevitable Condition）

这类的求解概念，在找寻是否存在一个玩家1的策略，不管玩家2怎么做，玩家1都可以到达系统中的某些状态。这类的赛局，在侦测死结（deadlock），无作用的程序代码（dead code）等等，都非常的有用。属于这一类的赛局有：

可到达赛局（Reachability game）

可到达赛局定义为RGame＝(G, v0, R)，v0V1∪V2代表赛局的起始点；RV1∪V2代表某些特定的节点，只要玩家1可以引导比赛进入R的其中一个节点，玩家1就算赢了这一场比赛。在文献上，可到达赛局具有两个非常漂亮的性质：

重复型（Recurrence Condition）

这类的求解概念，在找寻是否存在一个玩家1的策略，不管玩家2怎么做，玩家1都可以不断的重复某些状态。这类的赛局，在侦测系统是否保有公平性（Fairness）的特质时非常的有用，譬如操作系统的排程等等。属于这一类的赛局有：

Buchi赛局（Buchi game）

Buchi赛局定义为BGame＝（G, v0, F），v0V1∪V2代表赛局的起始点，FV1∪V2代表某些特定的节点，只要在比赛里，F其中至少一个节点无限次的出现在比赛中，那么玩家1就算赢了这一场赛局，否则就算玩家2赢了这一场赛局。

同样的在文献上也证明了Buchi赛局拥有确定性和存在无记忆策略的性质。

对称性赛局（Parity game）

对称性赛局定义为PGame＝（G, v0, p），v0V1∪V2代表赛局的起始点；p是优先权函数，给每一个节点都指派一个优先权，正规地来说，p：V1∪V2→[d], d  N。在对称性赛局中，只要在比赛中，无限次出现的优先权中，最小的数字是偶数的话，就代表了玩家1赢得这一场比赛，如果是奇数的话，那就是玩家2赢得这一场比赛。

同样的在文献上也证明了对称性赛局拥有确定性和存在无记忆策略的性质。

权重型（Weighted Condition）

这类的赛局追求的不在是谁胜谁负，而是尽可能的最大化自己的利益，最小化对方的所得。通常在各个状态或是状态转换时，都需要消耗一定量的系统资源，因此这类的求解概念，常被用来分析一个系统是否能够对资源做有效的配置，譬如嵌入式系统功率的消耗和网络路由器的缓冲区大小等等。属于这一类的赛局有：

平均收益赛局（Mean payoff game）

平均收益赛局定义为MGame＝（G, v0, r），v0 V1∪V2代表赛局的起始点；r是报酬函数，给每一个节点都指派一个报酬，正规地来说，r：V1∪V2→R。在一场比赛中，玩家1会获得在比赛中每一手节点的平均报酬，而玩家1所获得的即是玩家2所失去的，因此再平均收益赛局里，玩家1的目标是提高平均收益，而玩家2的目标是降低平均收益。

在平均收益赛局里，确定性是定义为存在一个数字C，使得玩家1最少都还有C的平均报酬，并且玩家2最多就只输C这么多的平均报酬。

同样的在文献上也证明了平均收益赛局拥有确定性和存在无记忆策略的性质。

涵盖率赛局（Coverage game）

涵盖率赛局定义为CGame＝（G, v0, r），v0 V1∪V2代表赛局的起始点；r是涵盖率的映像函数，给每一个节点都指派一个涵盖率，正规地来说，r：V1∪V2→R。在一场比赛中，玩家1所获得的涵盖率是在比赛中所有节点的涵盖率总合，而玩家2所获得的涵盖率即是图上所有节点涵盖率的总和扣掉玩家1所得到的涵盖率。因此再涵盖率赛局里，玩家1的目标是提高比赛中总共可以涵盖的涵盖率，而玩家2的目标是避免涵盖率的增加。

在文献上已经证实了涵盖率赛局中，求取玩家1所能够获得的最大的涵盖率是属于PSPACE-complete的问题。这种赛局，非常适合用来产生测试计划，和作为测试案例质量的指针。

混合型

综合其他类型特色的赛局，就形成了混合型的赛局，这类的赛局，通常都比较复杂，也需要更多的计算，但好处是可以更精准的分析出一个系统是否能够同时满足多种需求。属于这一类的赛局有：

平均收益对称赛局（Mean-payoff parity game）

平均收益对称赛局定义为MPGame＝（G, v0, p, r），v0 V1∪V2代表赛局的起始点；p是优先权函数，给每一个节点都指派一个优先权，正规地来说，p：V1∪V2→[d], d  N；r是报酬函数，给每一个节点都指派一个报酬，正规地来说，r：V1∪V2→R。在一场比赛中，如果无限次出现的优先权中，最小的数字是偶数的话，那玩家1可以获得在比赛中每一手节点的平均报酬，否则玩家1的平均报酬将是负的无限大；而玩家1所获得的即是玩家2所失去的，因此再平均收益对称赛局里，玩家1的目标同样是提高平均收益，而玩家2的目标同样也是降低平均收益。

《图二 平均收益对称赛局》

以图二为例，如果玩家1的策略为当节点1被拜访过的次数mod k为0的话，就选择节点3作为下一步，否则就选择节点2作为下一步。如此一来，无限次出现的优先权为偶数，故玩家1可以赢得{(k-1)×10+2}/k的平均收益。

在文献上，平均收益对称赛局已经被证明拥有确定性的性质，但是只存在需要无限记忆空间的优化策略。

结语

在文献上，平均收益对称赛局已经被证明拥有确定性的性质，但是只存在需要无限记忆空间的优化策略。

本文整理了数种文献上曾经探讨过的赛局和它们所要解决的问题，并且指出各种赛局在软件系统的分析上可能的应用，显示出赛局理论在计算器科学中渐渐地引起注意，扮演举足轻重的角色。

＜参考数据：

本文整理了数种文献上曾经探讨过的赛局和它们所要解决的问题，并且指出各种赛局在软件系统的分析上可能的应用，显示出赛局理论在计算器科学中渐渐地引起注意，扮演举足轻重的角色。

Gradel Erich, Thomas Wolfgang and Wilke Thomas, LNCS, Vol.?2500, 2002.

[2] Mean-Payoff Parity Games

K. Chatterjee, T. A. Henzinger and M. Jurdzinski

, LICS 2005.＞