Alloy与其在博弈论中的应用 11级逻辑学 陈希

目录 1、Alloy应用介绍 2、博弈论基本模型介绍 3、逻辑与博弈论的关系 4、Alloy在博弈论上实现的工作 5、开题报告

一、Alloy The design was done by the Software Design Group at MIT lead by Professor Daniel Jackson. In 1997 they produced the first Alloy prototype, which was then a rather limited object modelling language. Over the years Alloy has developed into a full structural modelling language capable of expressing complex structural constraints and behaviour. Alloy has gradually improved in performance and scalability and been applied to many fields including scheduling, cryptography and instant messaging.

Alloy The logic that Alloy provides for modeling is first-order logic with the transitive closure operator. An Alloy model consists of a set of sets, relations, and functions in a model, and a set of constraints, which are logical formulas. Inspired by the Z specification language and Tarski’ s relational calculus.

Alloy The Alloy Analyzer, the main analysis tool for Alloy models, provides finite scope analysis: a user is required to fix the size of the sets in the model to constant numbers and then, the Alloy Analyzer translates the model to a propositional CNF formula, which is then handed to a SAT solver for consistency checking. The Alloy Analyzer relies on recent advances in SAT( boolean satisfiability) technology. As solvers get faster, so Alloy’s analysis gets faster and scales to larger problems. Using the best solvers of today, the analyzer can examine spaces that are several hundred bits wide

基本组成要素 The logic provides the building blocks of the language. All structures are represented as relations, and structural properties are expressed with a few simple but powerful operators. The language adds a small amount of syntax to the logic for structuring descriptions. The analysis is a form of constraint solving. Simulation involves finding instances of states or executions that satisfy a given property. Checking involves finding a counterexample—an instance that violates a given property.

Logic: The set operators + union & intersection - difference in subset = equality Name = {(G0), (A0), (A1)} Alias = {(A0), (A1)} Group = {(G0)} Alias + Group = {(G0), (A0), (A1)} Alias & Group = {(G0)} Name - Group = {(A0) , (A1)}

Logic: Relational Operators -> arrow (product) :p -> q is a binary relation . dot (join): operator is composition ~ transpose ^ transitive closure * reflexive-transitive closure <: domain restriction :> range restriction Name = {(N0), (N1)} Addr = {(D0), (D1)} Book = {(B0)} Name -> Addr = {(N0, D0), (N0, D1), (N1, D0), (N1, D1)} {(N0, A0)} . {(A0, D0)} = {(N0, D0)} {(N0, D0)} . {(N0, D0)} = {}

Logic: Relational Operators address = {(N0, D0), (N1, D0), (N2, D2)} ~address = {(D0, N0), (D0, N1), (D2, N2)} address ={(G0, A0), (G0, G1), (A0, D0), (G1, D0), (G1, A1), (A1, D1), (A2, D2)} ^address ={(G0, A0), (G0, G1), (A0, D0), (G1, D0), (G1, A1), (A1, D1), (A2, D2), (G0, D0), (G0, A1), (G1, D1),(G0, D1)} address = {(G0, A0), (G0, G1), (A0, D0),(G1, D0)} Group = {(G0), (G1)} ， Addr = {(D0), (D1), (D2)} Group <: address = {(G0, A0), (G0, G1), (G1, D0)} address :> Addr = {(A0, D0), (G1, D0)}

Logic: Logical Operators not ! negation and && conjunction or || disjunction implies => implication else , alternative iff <=> bi-implication

Logic: Quantification all x: e | F F holds for every x in e; some x: e | F F holds for some x in e; no x: e | F F holds for no x in e; lone x: e | F F holds for at most one x in e; one x: e | F F holds for exactly one x in e.

Logic: Cardinality Constraints + plus - minus = equals < less than > greater than =< less than or equal to >= greater than or equal to

Language A fact records a constraint that is assumed always to hold. A function defines a reusable expression. we can now use grandpas (p) to refer to p’s grandpas. A predicate defines a reusable constraint. we can now use ownGrandpa (p) to say that p is his own grandpa. An assertion is a constraint that is intended to follow from the facts of the model.

Commands and Scope A run command tells the tool to search for an instance of a predicate. A check command tells it to search for a counterexample of an assertion.

Language: Signatures and Fields Sig A { } introduces a set named A A set can be introduced as a subset of another set : sig A1 extends A {} An abstract signature has no elements except those belonging to its extensions. abstract sig A {} Sig A1 extends A {} Sig A2 extends A {} A = A1 + A2

Analysis run a predicate or check an assertion, the analyzer searches for an instance of an analysis constraint In the case of a predicate, the analysis constraint is the predicate’s constraint conjoined with the facts of the model— An instance is an example: a scenario in which both the facts and the predicate hold. In the case of an assertion, the analysis constraint is the negation of the assertion’s constraint conjoined with the facts of the model. An instance is a counterexample

Analysis Every analysis involves solving a constraint: either finding an instance (for a run command) or finding a counterexample (for a check). However, it is more of a compiler, because, rather than solving the constraint directly, it translates the constraint into a boolean formula and solves it using an off-the-shelf SAT solver. SAT stands for “ satisfiability ”: a solution to a boolean formula is an assignment of values to the formula’s boolean variables that “satisfies” the formula.

Alloy 实例展示 1、过河问题 2、握手问题

Alloy 与Haskell比较 语言方面：两种语言都简洁易懂，语义清晰，易于用形式化语言描述。 运行方面：Alloy Analyzer是自动分析工具，依赖于现在的前言技术SAT( boolean satisfiability) technology，分析速度快。Haskell 运行有限，不利于做大模型推广。 操作方面：Alloy提供可视化操作界面。 国际研究应用方面：Alloy应用范围更广，调度软件设计的模型检测，基于时态逻辑的模型检测，基于Alloy的模态逻辑教学软件， Haskell在动态认知逻辑的应用。

二、博弈论 研究多个个体或团队之间在特定条件制约下的对局里利用相关方的策略，而实施对应策略的学科。 迄今为止，共有6届的诺贝尔经济学奖与博弈论的研究有关，作为一门工具学科能够在经济学中如此广泛运用并得到学界垂青实为罕见。

博弈论要素 博弈的参与者(Player):指参与博弈的决策主体。 行动(Action):是参与者在博弈的某个时点的决策变量。 行动次序(Oder of play): 博弈行动的先后次序。 信息(hiformation):参与者在博弈中的知识,特别是有关其他参与者的特征和行动的知识。 策略(Strategy):指参与者在给定信息集的情况下的行动战略。 收益(Pay off）:指在特定的策略组合下,参与者在可能的每一结果上的得失。 均衡(Equlibrium):参与者选取的最佳策略所组成的策略组合

博弈分类 静态 动态 纳什均衡 完全信息 不完全信息 （纳什1950） 子博弈精炼纳什均衡 （泽尔腾1965） 贝叶斯纳什均衡 （海萨尼1967） 精炼贝叶斯 纳什均衡 （泽尔腾1975） 静态博弈：参与人同时选择行动或虽非同时但后行动者并不知道前行动者采取了什么具体行动。 动态博弈：参与人的行动有先后顺序，且后行动者能够观察到先行动者所选择的行动。 完全信息：每一个参与人对所有其他参与人的特征、战略空间及支付函数有准确的知识。否则，就是不完全信息。

静态完全信息博弈 智猪博弈 按 等待 5,1 4,4 9，-1 0,0 大猪 小猪 纳什均衡 ：给定对方策略不变，单方面改变策略并不能使得情况好转。 纯策略纳什均衡：（大猪按，小猪等待）

纳什均衡存在性定理： 每一个有限博弈至少存在一个纳什均衡 （有限博弈指的是博弈有有限个参与人且每个参与人有有限个纯战略）

完全信息动态博弈 默许 打击 不进入 0,3 进入 1,2 -1，-1 产商1 不进入 进入 产商2 打击 （0,3） 默许 （1，2） （-1，-1） 纳什均衡（不进入，打击），（进入，默许） 子博弈精炼纳什均衡（进入，默许）

动态博弈解释 在纳什均衡中，参与人在选择自己的战略时，把其他人的战略当作是给定的，不考虑自己的选择如何影响对手的战略。这个假设在静态博弈时成立的，因为参与人同时行动。但对动态博弈而言，一个人行动在先，一个人行动在后，后者会根据前者的选择而调整自己的选择，前者自然会理性地预期到这一点。从而把纳什均衡中包含的不可置信的威胁战略剔除出去。

重复博弈 纳什均衡（坦白，坦白） 重复博弈触发机制纳什均衡：一开始都选择抵赖，直到有一方选择了坦白，然后就永远选择坦白。 坦白 抵赖 -8, -8 0,-10 -10，0 -1, -1

重复博弈 令u为贴现因子，囚徒1在某阶段首先选择了坦白，那么他之后的得益是： 0+u（-8）+u2（-8）+···=-8u/(1-u) 若囚徒i选择抵赖，那么他之后的得益是 -1+u（-1）+u（-1）+···=-1/(1-u) 当u≥1/8,给定囚徒2坚持触发战略没有首先选择坦白，囚徒i不会选择首先坦白。 给定囚徒1首先选择了坦白，囚徒2会选择一直坦白。 触发战略是一个纳什均衡。

不完全信息静态博弈

不完全信息静态博弈 贝叶斯纳什均衡： 囚犯2的类型i选择坦白的概率为1。 囚犯2的类型ii选择不坦白的概率为1。 囚犯1认为囚犯2属于i类型的概率为u， 给定囚犯2的行动策略，则有： [-10u+0(1-u)]>[-5u-1(1-u)] => u<1/6 当u<1/6,囚犯1选择不坦白 当u>1/6,囚犯1选择坦白

不完全信息动态博弈 产商1 L R M 2 （1,3） B U B U (0,1) (2,1) (0,2) (0,0) 纳什均衡（L，B），（M，U） 精炼贝叶斯纳什均衡（M，U；P=1）

不完全信息动态博弈 假设参与人2认为参与人1选择M，R的概率为P，1-P。给定这个信念，参与人2选择U的效用为2-P，选择B的效用为1-P。无论P为何值，参与人2一定会选U。给定参与人1知道参与人2将选择U，参与人最优选择是 M，因此当参与人2观测到参与人1没有选择L时，他知道参与人1一定选择了M，即P=1。

三、博弈论与逻辑学的关系 一方面，逻辑学中有一些概念本身就具有博弈的性质和结构， 博弈论为逻辑学提供了系统解释的直观背景及新的解决思路。 另一方面，逻辑学可以帮助澄清博弈论中可能的博弈结构，并分析参与者在博弈过程中的思考机制，并用形式化的语言提供精致的结构来描述博弈论中的策略均衡。

博弈论与逻辑学的关系 用博弈术语的方法描述逻辑运算，用博弈方法解决逻辑问题，即逻辑的博弈化。 利用逻辑知识来研究博弈理论，即博弈的逻辑化。

逻辑的博弈化 辛提卡的“赋值博弈” 赋值博弈基本的方法是把对一阶公式的赋值看作是证实者和证伪者相对于某一论域的博弈，逻辑中的联结词正好对应于博弈中参与者的各种行为。 一个逻辑公式是析取式，对应博弈证实者的选择行为，他可以选择其中的一个选言支，博弈继续进行。合取式则对应证伪者的选择行为。否定式对应于博弈双方的角色调换。存在量词对应于证实者从论域中挑选一个对象。全称量词对应于证伪者的挑选行为。 博弈论语义学成为分析一阶逻辑公式有效性的重要工具。

逻辑的博弈化  博弈论语义学将博弈论与语义学结合起来，通过博弈过程来刻画人们对命题语义的理解过程，最终以确定语句的真值。辛梯卡首先给出一个个体域，任何指派都可以在这个集合中找到。博弈论语义学的核心是将量词短语看成加诸对象的变元，将句子看成语句函项，然后在给定的个体域中选择某个对象改变将对象加诸变元的指派，从而将命题的值变为选定的对象，达到消除量词，找到原子句的目的。在方法上，辛梯卡选择了博弈论，他将人们对句子的理解过程比喻为一个两人博弈，两个玩家分别为“证实者”和“证伪者”，对于一个句子，根据规则，博弈双方轮流将该句子约化，直至最后使得约化的句子不再包含变量和连接词，即原子句，此时双方就可以通过直接检查当前指派来一决输赢。如果这个原子句为真，则证实者取胜，证伪者失败，反之亦然。①运用博弈论语义学，我们能够从大量的语言信息中得到最基本、最简化的语句，从而能够轻松地判定这些语言信息的真假。

博弈的逻辑化 流派： 1、结合动态逻辑研究博弈逻辑。代表人物为帕里克、波利、 约翰·范·本瑟姆。 1、结合动态逻辑研究博弈逻辑。代表人物为帕里克、波利、 约翰·范·本瑟姆。 2、结合模态逻辑系统建立博弈逻辑系统。代表人物金子守。 但由于主要是从静态角度出发，没有考虑动态的因素，没有成为当今世界博弈逻辑研究的主流。 与博弈论的联系： 博弈论注重定量模型化分析，通常以构建数学模型以求得对局的精确解，博弈逻辑侧重研究人们采取行动的推理过程，寻求参与人的合理的策略选择，注重用形式化的语言刻画博弈和各种逻辑方法的综合运用。

四、Alloy在博弈论上的应用展示