Alloy與其在博弈論中的應用

Alloy與其在博弈論中的應用11級邏輯學陳希目錄1、Alloy應用介紹2、博弈論基本模型介紹3、邏輯與博弈論的關(guān)系4、Alloy在博弈論上實現(xiàn)的工作

5、開題報告一、Alloy

ThedesignwasdonebytheSoftwareDesignGroupatMITleadbyProfessorDanielJackson.In1997theyproducedthefirstAlloyprototype,whichwasthenaratherlimitedobjectmodellinglanguage.OvertheyearsAlloyhasdevelopedintoafullstructuralmodellinglanguagecapableofexpressingcomplexstructuralconstraintsandbehaviour.

Alloyhasgraduallyimprovedinperformanceandscalabilityandbeenappliedtomanyfieldsincludingscheduling,cryptographyandinstantmessaging.Alloy

ThelogicthatAlloyprovidesformodelingisfirst-orderlogicwiththetransitiveclosureoperator.AnAlloymodelconsistsofasetofsets,relations,andfunctionsinamodel,andasetofconstraints,whicharelogicalformulas.

InspiredbytheZspecificationlanguageandTarski’srelationalcalculus.

AlloyTheAlloyAnalyzer,themainanalysistoolforAlloymodels,providesfinitescopeanalysis:auserisrequiredtofixthesizeofthesetsinthemodeltoconstantnumbersandthen,theAlloyAnalyzertranslatesthemodeltoapropositionalCNFformula,whichisthenhandedtoaSATsolverforconsistencychecking.TheAlloyAnalyzerreliesonrecentadvancesinSAT(boolean

satisfiability)technology.Assolversgetfaster,soAlloy’sanalysisgetsfasterandscalestolargerproblems.Usingthebestsolversoftoday,theanalyzercanexaminespacesthatareseveralhundredbitswide

基本組成要素Thelogicprovidesthebuildingblocksofthelanguage.Allstructuresarerepresentedasrelations,andstructuralpropertiesareexpressedwithafewsimplebutpowerfuloperators.Thelanguageaddsasmallamountofsyntaxtothelogicforstructuringdescriptions.Theanalysisisaformofconstraintsolving.Simulationinvolvesfindinginstancesofstatesorexecutionsthatsatisfyagivenproperty.Checkinginvolvesfindingacounterexample—aninstancethatviolatesagivenproperty.Logic:Thesetoperators+union&intersection-differenceinsubset=equalityName={(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?->?qisabinaryrelation.dot(join):operatoriscomposition~transpose^transitiveclosure*reflexive-transitiveclosure<:domainrestriction:>rangerestrictionName={(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 Operatorsaddress={(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 Operatorsnot!negationand&&conjunctionor||disjunctionimplies=>implicationelse,alternative

iff<=>bi-implication

Logic:Quantificationallx:e|FFholdsforeveryxine;somex:e|FFholdsforsomexine;nox:e|FFholdsfornoxine;lonex:e|FFholdsforatmostonexine;onex:e|FFholdsforexactlyonexine.Logic:Cardinality Constraints+plus-minus=equals<lessthan>greaterthan=<lessthanorequalto>=greaterthanorequaltoLanguageAfactrecordsaconstraintthatisassumedalwaystohold.Afunctiondefinesareusableexpression.wecannowusegrandpas(p)torefertop’sgrandpas.Apredicatedefinesareusableconstraint.wecannowuseownGrandpa(p)tosaythatpishisowngrandpa.Anassertionisaconstraintthatisintendedtofollowfromthefactsofthemodel.

CommandsandScopeAruncommandtellsthetooltosearchforaninstanceofapredicate.Acheckcommandtellsittosearchforacounterexampleofanassertion.Language:SignaturesandFieldsSigA{}introducesasetnamedAAsetcanbeintroducedasasubsetofanotherset:sigA1extendsA{}Anabstractsignaturehasnoelementsexceptthosebelongingtoitsextensions.abstractsigA{}SigA1extendsA{}SigA2extendsA{}A=A1+A2Analysisrunapredicateorcheckanassertion,theanalyzersearchesforaninstanceofananalysisconstraintInthecaseofapredicate,theanalysisconstraintisthepredicate’sconstraintconjoinedwiththefactsofthemodel—Aninstanceisanexample:ascenarioinwhichboththefactsandthepredicatehold.Inthecaseofanassertion,theanalysisconstraintisthenegationoftheassertion’sconstraintconjoinedwiththefactsofthemodel.AninstanceisacounterexampleAnalysisEveryanalysisinvolvessolvingaconstraint:eitherfindinganinstance(foraruncommand)orfindingacounterexample(foracheck).However,itismoreofacompiler,because,ratherthansolvingtheconstraintdirectly,ittranslatestheconstraintintoabooleanformulaandsolvesitusinganoff-the-shelfSATsolver.SATstandsfor“satisfiability”:asolutiontoabooleanformulaisanassignmentofvaluestotheformula’sbooleanvariablesthat“satisfies”theformula.Alloy實例展示1、過河問題2、握手問題Alloy與Haskell比較語言方面：兩種語言都簡潔易懂，語義清晰，易于用形式化語言描述。運行方面：AlloyAnalyzer是自動分析工具，依賴于現(xiàn)在的前言技術(shù)SAT(boolean

satisfiability)technology，分析速度快。Haskell運行有限，不利于做大模型推廣。操作方面：Alloy提供可視化操作界面。國際研究應用方面：Alloy應用范圍更廣，調(diào)度軟件設計的模型檢測，基于時態(tài)邏輯的模型檢測，基于Alloy的模態(tài)邏輯教學軟件，Haskell在動態(tài)認知邏輯的應用。二、博弈論研究多個個體或團隊之間在特定條件制約下的對局里利用相關(guān)方的策略，而實施對應策略的學科。迄今為止，共有6屆的諾貝爾經(jīng)濟學獎與博弈論的研究有關(guān)，作為一門工具學科能夠在經(jīng)濟學中如此廣泛運用并得到學界垂青實為罕見。

博弈論要素博弈的參與者(Player):指參與博弈的決策主體。行動(Action):是參與者在博弈的某個時點的決策變量。行動次序(Oderofplay):博弈行動的先后次序。信息(hiformation):參與者在博弈中的知識,特別是有關(guān)其他參與者的特征和行動的知識。策略(Strategy):指參與者在給定信息集的情況下的行動戰(zhàn)略。收益(Payoff）:指在特定的策略組合下,參與者在可能的每一結(jié)果上的得失。均衡(Equlibrium):參與者選取的最佳策略所組成的策略組合博弈分類靜態(tài)博弈：參與人同時選擇行動或雖非同時但后行動者并不知道前行動者采取了什么具體行動。動態(tài)博弈：參與人的行動有先后順序，且后行動者能夠觀察到先行動者所選擇的行動。完全信息：每一個參與人對所有其他參與人的特征、戰(zhàn)略空間及支付函數(shù)有準確的知識。否則，就是不完全信息。靜態(tài)動態(tài)完全信息

納什均衡（納什1950）子博弈精煉納什均衡（澤爾騰1965）不完全信息貝葉斯納什均衡（海薩尼1967）精煉貝葉斯納什均衡（澤爾騰1975）靜態(tài)完全信息博弈智豬博弈按等待按5,14,4等待9，-10,0

小豬大豬納什均衡：給定對方策略不變，單方面改變策略并不能使得情況好轉(zhuǎn)。純策略納什均衡：（大豬按，小豬等待）納什均衡存在性定理：每一個有限博弈至少存在一個納什均衡（有限博弈指的是博弈有有限個參與人且每個參與人有有限個純戰(zhàn)略）完全信息動態(tài)博弈

產(chǎn)商1產(chǎn)商2進入不進入默許打擊（0,3）（-1，-1）（1，2）默許打擊不進入0,30,3進入1,2-1，-1納什均衡（不進入，打擊），（進入，默許）子博弈精煉納什均衡（進入，默許）動態(tài)博弈解釋在納什均衡中，參與人在選擇自己的戰(zhàn)略時，把其他人的戰(zhàn)略當作是給定的，不考慮自己的選擇如何影響對手的戰(zhàn)略。這個假設在靜態(tài)博弈時成立的，因為參與人同時行動。但對動態(tài)博弈而言，一個人行動在先，一個人行動在后，后者會根據(jù)前者的選擇而調(diào)整自己的選擇，前者自然會理性地預期到這一點。從而把納什均衡中包含的不可置信的威脅戰(zhàn)略剔除出去。重復博弈納什均衡（坦白，坦白）重復博弈觸發(fā)機制納什均衡：一開始都選擇抵賴，直到有一方選擇了坦白，然后就永遠選擇坦白。坦白抵賴坦白-8,-80,-10抵賴-10，0-1,-1重復博弈令u為貼現(xiàn)因子，囚徒1在某階段首先選擇了坦白，那么他之后的得益是：0+u（-8）+u2（-8）+···=-8u/(1-u)若囚徒i選擇抵賴，那么他之后的得益是-1+u（-1）+u（-1）+···=-1/(1-u)當u≥1/8,給定囚徒2堅持觸發(fā)戰(zhàn)略沒有首先選擇坦白，囚徒i不會選擇首先坦白。給定囚徒1首先選擇了坦白，囚徒2會選擇一直坦白。觸發(fā)戰(zhàn)略是一個納什均衡。不完全信息靜態(tài)博弈不完全信息靜態(tài)博弈貝葉斯納什均衡：囚犯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選擇坦白不完全信息動態(tài)博弈

產(chǎn)商1（1,3）納什均衡（L，B），（M，U）精煉貝葉斯納什均衡（M，U；P=1）(2,1)(0,0)(0,2)(0,1)LRMUBUB2不完全信息動態(tài)博弈假設參與人2認為參與人1選擇M，R的概率為P，1-P。給定這個信念，參與人2選擇U的效用為2-P，選擇B的效用為1-P。無論P為何值，參與人2一定會選U。給定參與人1知道參與人2將選擇U，參與人最優(yōu)選擇是M，因此當參與人2觀測到參與人1沒有選擇L時，他知道參與人1一定選擇了M，即P=1。三、博弈論與邏輯學的關(guān)系一方面，邏輯學中有一些概念本身就具有博弈的性質(zhì)和結(jié)構(gòu)，博弈論為邏輯學提供了系統(tǒng)解釋的直觀背景及新的解決思路。另一方面，邏輯學可以幫助澄清博弈論中可能的博弈結(jié)構(gòu)，并分析參與者在博弈過程中的思考機制，并用形式化的語言提供精致的結(jié)構(gòu)來描述博弈論中的策略均衡。博弈論與邏輯學的關(guān)系用博弈術(shù)語的方法描述邏輯運算，用博弈方法解決邏輯問題，即邏輯的博弈化。利用邏輯知識來研究博弈理論，即博弈的邏輯化。邏輯的博弈化

辛提卡的“賦值博弈”賦值博弈基本的方法是把對一階公式的賦值看作是證實者和證