Certification for µ calculus with winning strategies (PresentedattheVeriSureworkshopassociatedwithCAV’13inSt.PetersburginJuly2013) MartinHofmann1andHaraldRueß2 1 DepartmentofInformatics,Ludwig-Maximilians-Universita¨t,Mu¨nchen,Germany 2 fortissAn-InstitutTechnischeUniversita¨tMu¨nchen,D-80805Mu¨nchen,Guerickestr.25,Germany Abstract. Wedefinememory-efficientcertificatesforµ-calculusmodelcheckingproblems 4 basedonthewell-knowncorrespondenceoftheµ-calculusmodelcheckingwithwinning 1 certain parity games. Winning strategies can independently checked, in low polynomial 0 time,byobservingthatthereisnoreachablestronglyconnectedcomponentinthegraphof 2 theparitygamewhoselargestpriorityisodd.Winningstrategiesarecomputedbyfixpoint n iterationfollowingthenaivesemanticsofµ-calculus.Weinstrumenttheusualfixpointit- a erationofµ-calculusmodelcheckingsothatitproducesevidenceintheformofawinning J strategy;thesewinningstrategiescanbecomputedinpolynomialtimein|S|andinspace 8 O(|S|2|φ|2),where|S|isthesizeofthestatespaceand|φ|thelengthoftheformulaφ. Onthetechnicallevelourworkcanbeseenasanew,simpler,andimmediateconstructive ] proofofthecorrespondencebetweenµ-calculusandparitygames. O L . 1 Introduction s c [ Wedevelopalgorithmsforconstructingconcisecertificatesforµ-calculusmodelcheckingprob- 1 lemsandforefficientlyandindependentlycheckingthesecertificatesbyatrustworthychecker. v Thesedevelopmentsmayformtheunderpinningforasoundintegrationofµ-calculusmodel 3 checking into a verification system such as PVS [18]. Using Shankar’s kernel of truth [20] ap- 9 proach,whichisbasedoncheckingtheverificationandonverifyingthechecker,certificatesare 6 generatedusinganuntrustedimplementationofourµ-calculusmodelcheckingalgorithms,and 1 . certificatesarethencheckedbymeansofanexecutablePVSfunction,whichitselfisverifiedin 1 a trusted kernel of PVS. In contrast to logical integration frameworks based on computational 0 reflection(e.g.[3])thekerneloftruthapproachdoesnotrequireprovingthecorrectnessofthe 4 1 completeimplementionoftheverificationprocedure. : In this way it should be possible to generate checkable certificates for the bisimulation be- v i tweenprogramsandformodelcheckingproblemsforbothlineartimetemporallogicsandcom- X putationtreelogics[10]asthebasisforassurancecasesandcertificationargumentsforsafety- r criticalsystems.Moreover,certificatesforµ-calculusmodelcheckingmightalsobeusedasym- a metricabstraction-refinement-basedmodelcheckingenginesforthefullµ-calculusbasedonre- finingover-approximationsusingspuriouscounterexamplesandrelaxingunder-approximations using dubious witnesses along the lines of [23,22], for sending code together with proofs of arbitrarysafetyandlivenesspropertiesproperties,whicharethencheckedbycodeconsumersac- cordingtotheproof-carryingcodeparadigmof[17],andforsynthesizingcorrect-by-construction controllersfromthesecertificatesalongthelinesof[22]. Our main result is an effective and efficient instrumentation of the usual fixpoint iteration of µ-calculus model checking [5] for generating certificates that are independently checkable in low polynomial time. This construction builds on the well-known correspondence of model checkingfortheµ-calculuswithwinningcertainparitygamesbyEmersonandJutla[9].Parity gamesareequivalentvialineartimereductionstotheproblemofµcalculusmodelchecking(e.g. [11]), Determinacy of parity games follows directly from Martin’s most general result on the 2 MartinHofmann,HaraldRueß determinacyofBorelgames[15].Playersofparitygamesmayrestrictthemselvestomemoryless strategies; this also implies that for each vertex one of the players has a winning strategy, so there are no draws. Algorithms for generating witnesses for players of parity games and their complexityaredescribedin[13]. There have been many results and algorithms for constructing witnesses and counterex- amples of various forms for different sublogics, including LTL, ACTL, CTL, CTL∗, or the µ-calculus [6,1,19,26,7,21,12]. Local model checking procedures for determining whether finite-statesystemshavepropertiesexpressibleintheµ-calculusincrementallyconstructtableau proofs[27,24,8],whichcanbeproof-checkedindependently.Thesizeoftheconstructedtableaux can be exponential in the number of states of the model. Based on the tableau method of local µ-calculus model checking, Kick [14] proposes an optimized construction by identifying iso- morphic subproofs. Namjoshi [16] introduced the notion of certifying model checker that can generate independently checkable witnesses for properties verified by a model checker. He de- fineswitnessesforpropertiesoflabelledtransitionsystemsexpressedintheµ-calculusbasedon paritygamesoveralternatingtreeautomata.Histechnicaldevelopmentsrelyonµ-calculussigna- tures[25]fortermination,andexploitsthecorrespondencebetweenµ-calculusmodelchecking withwinningparitygames[9]. Incontrasttotheabovemethods,thewitnessesgeneratedbyourglobalmodelcheckingal- gorithm are rather small, as they can be represented in space in O(|S|2|φ|2), where |S| is the sizeofthestatespaceand|φ|isthelengthoftheformulaφ.Onthetechnicallevelourworkcan be seen as a new, simpler, and immediately constructive proof of the correspondence between µ-calculusandparitygames.Winningstrategiesarecomputedbyfixpointiterationfollowingthe naivesemanticsofµ-calculus.Nocomplexauxiliarydevicessuchassignatures[25]oralternat- ingautomata[9]areneeded. The paper is structured as follows. In Sections 2 and 3 we are reviewing standard develop- ments for the µ-calculus to keep the paper as self-contained as possible. The definition of the nesting depth in Section 2, however, is non-standard and central to the technical developments in this paper. The low polynomial-time checker for certificates in Section 3 is inspired by the standard algorithm for nonemptiness of Street automata. Our constructive proof of the corre- spondence between µ calculus model checking and winning parity games forms the basis of our main contribution, namely the instrumentation of the global model checking iteration for producingmemory-efficientcertificatesintheformofwinningstrategies. 2 SyntaxandSemantics WeareassumingvariablesX ∈X,propositionsP ∈P,andactionsa∈A. Definition1. Thesetofµ-calculusformulaeφisgivenbythegrammar φ ::= X |P |(cid:104)a(cid:105)φ|[a]φ|φ ∧φ |φ ∨φ |µX.φ|νX.φ 1 2 1 2 ThesetoffreevariablesFV(φ)⊆X ,thesize|φ|ofaformula,andthesubstitutionφ[Z :=ψ] offormulaψforanyfreeoccurrenceZ ∈FV(φ)aredefinedintheusualway. ThenotationsQ ∈{µ,ν},M ∈{[a],(cid:104)a(cid:105)|a∈A},∗∈{∧,∨}areusedtosimplifyinductive definitions.Wedefinethenestingdepthnd(QX.φ)ofafixpointformulaasoneplusthemaximal nestingdepth—recursively—ofallfixpointformulasencountereduntilanyfreeoccurrenceofX Certificationforµcalculuswithwinningstrategies 3 inφ.Formally, nd(X,φ)=0, ifX (cid:54)∈FV(φ),otherwise: nd(X, X)=0 nd(X, φ ∗φ )=max(nd(X,φ ), nd(X,φ )) 1 2 1 2 nd(X, Mφ)=nd(X,φ) nd(X,QY.φ)=max(nd(QY.φ),nd(X, φ)) nd(QX,φ)=1+nd(X,φ) nd(φ)=0,otherwise. Forexample,nd(QW.Y)=1sond(QY.X∧QW.Y)=2andnd(QX.QY.X∧QW.Y)=3, howevernd(X,QY.X∧QW.Y)=1. The salient property of the nesting depth is summarised by the following lemma which is easilyprovedbyinduction. Lemma1. Let φ = QX.ψ [Z := QY.ψ ] where X ∈ FV(ψ ) and Z ∈ FV(ψ ); then 1 2 2 1 nd(QY.ψ )<nd(φ). 2 Thus,ifwetraveldownfromafixpointquantifiertoanoccurrenceofitsboundvariablethenall the fixpoint quantifiers encountered on the way in the abstract syntax tree have strictly smaller nestingdepth. Thesemanticsofµ-calculusformulaeisgivenintermsoflabelledtransitionsystems(LTS), a consistingofanonemptysetofstatesS,andafamilyoftotalrelations−→ ∈ S×S foreach actiona∈Aand,finally,anassignmentT ∈S →2P whichtellsforeachstateswhichatomic a propositionsP ∈P aretrueinthatstate.IfT isanLTS,weuse|T|foritssetofstates;−→ or T a simply−→foritstransitionrelationandT itselfforitsinterpretationofatomicpropositions. FixatransitionsystemT andputS =|T|.ForηisafinitepartialfunctionfromX toSwith FV(φ)⊆dom(η)wedefine φ η ⊆S by (cid:74) (cid:75) P η ={s|P ∈T(s)} (cid:74) (cid:75) X η =η(X) (cid:74) (cid:75) φ ∨φ η = φ η∪ φ η 1 2 1 2 (cid:74) (cid:75) (cid:74) (cid:75) (cid:74) (cid:75) φ ∧φ η = φ η∩ φ η 1 2 1 2 (cid:74) (cid:75) (cid:74) (cid:75) (cid:74) (cid:75) a (cid:104)a(cid:105)φ η =pre(−→)( φ η) (cid:74) (cid:75) (cid:74) (cid:75) a [a]φ η =pre(−→)( φ η) (cid:102) (cid:74) (cid:75) (cid:74) (cid:75) µX.φ η =lfp(U (cid:55)→ φ η[X :=U]) (cid:74) (cid:75) (cid:74) (cid:75) νX.φ η =gfp(U (cid:55)→ φ η[X :=U]) (cid:74) (cid:75) (cid:74) (cid:75) a a Thesetspre(−→)( φ η)andpre(−→)( φ η)respectivelydenotethepreimageandtheweakest (cid:102) (cid:74) (cid:75) (cid:74) (cid:75) a preconditionoftheset φ ηwithrespecttothebinaryrelation−→;formally: (cid:74) (cid:75) a a s∈pre(−→)( φ η)iff ∃t∈S.s−→tand t∈ φ η (cid:74) (cid:75) (cid:74) (cid:75) a a s∈pre(−→)( φ η)iff ∀t∈S.s−→timplies t∈ φ η (cid:102) (cid:74) (cid:75) (cid:74) (cid:75) Given the functional F(U) = φ η[X :=U], lfp(F) and gfp(F)respectively denote the least andthegreatest,withrespectto(cid:74)th(cid:75)esubsetorderingon2S,fixpointsofF.Thesefixpointsexist, sinceF ismonotone. 4 MartinHofmann,HaraldRueß sem(X,η)=η(X) sem(µX.φ,η)=iter (φ,η,∅) X sem(νX.φ,η)=iter (φ,η,S) X sem(φ ∧φ ,η)=sem(φ ,η)∩sem(φ ,η) 1 2 1 2 sem(φ ∨φ ,η)=sem(φ ,η)∪sem(φ ,η) 1 2 1 2 sem([a]φ,η)=pre(−a→)(sem(φ,η)) (cid:102) sem((cid:104)a(cid:105)φ,η)=pre(−a→)(sem(φ,η)) iter (φ,η,U)=if U =U thenU elseiter (φ,η,U ) X p X p whereU := sem(φ,η[X :=U]) p Fig.1.Fixpointiterationforcomputingthesemanticsofµ-calculusformulas. Proposition1. QX.φ η = φ[X :=QX.φ] η. (cid:74) (cid:75) (cid:74) (cid:75) ForthemonotonicityofF,∅⊆F(∅)⊆F2(∅)⊆...andS ⊇F(S)⊇F2(S)⊇....Moreover, ifS isfinitethenwehave µX.φ η ={s∈S|exists t≤|S|.s∈Ft(∅)}, (cid:74) (cid:75) νX.φ η ={s∈S|forall t≤|S|.s∈Ft(S)}. (cid:74) (cid:75) Therefore,inthecaseS isfinite,theiterativealgorithminFigure1computes φ η. (cid:74) (cid:75) Proposition2. φ η =sem(φ,η). (cid:74) (cid:75) Lemma2. s(cid:54)∈ φ ηiff s∈ φ∗ η(cid:48),whereη(cid:48)(X)=S\η(X)andφ∗isthedualofφgivenby (cid:74) (cid:75) (cid:74) (cid:75) (P)∗ =P (X)∗ =X (φ ∧φ )∗ =φ∗∨φ∗ 1 2 1 2 (φ ∨φ )∗ =φ∗∧φ∗ 1 2 1 2 ([a]φ)∗ =(cid:104)a(cid:105)φ∗ ((cid:104)a(cid:105)φ)∗ =[a]φ∗ (µX.φ)∗ =νX.φ∗ (νX.φ)∗ =µX.φ∗ 3 ParityGames Aparitygameisgivenbythefollowingdata: – a (finite or infinite) set of positions Pos partitioned into proponent’s (Player 0) and oppo- nent’s(Player1)positions:Pos =Pos +Pos ; 0 1 – atotaledgerelation→⊆ Pos×Pos;1 1totalmeansforallp∈Posthereexistsp(cid:48) ∈Poswithp→p(cid:48). Certificationforµcalculuswithwinningstrategies 5 – afunctionΩ ∈Pos →Nwithafiniterange;wecallΩ(p)thepriorityofpositionp. Theplayersmovea tokenalongtheedgerelation →.Whenthetoken isonapositionin Pos 0 thenproponentdecideswheretomovenextandlikewiseforopponent. In order to formalize the notion of “to decide” we must introduce strategies. Formally, a strategyforaplayeri∈0,1isafunctionσthatforanynonemptystringp(cid:126)=p(0)...p(n)over Pos andsuchthatp(k) → p(k+1)fork = 0...n−1andp(n) ∈ Pos associatesaposition i σ(p(cid:126))∈Pos suchthatp(n)→σ(p(cid:126)). Givenastartingpositionpandstrategiesσ andσ forthetwoplayersonethenobtainsan 0 1 infinitesequenceofpositions(a“play”)p(0),p(1),p(2),...by p(0)=p p(n+1)=σ (p(0)...p(n)) where p(n)∈Pos i i Wedenotethissequencebyplay(p,σ ,σ ). 0 1 Theplayiswonbyproponent(Player0)ifthelargestnumberthatoccursinfinitelyoftenin thesequenceΩ(play(p,σ ,σ ))isevenanditiswonbyopponentifthatnumberisodd.Note 0 1 thatΩ( )isappliedcomponent-wiseandthatalargestpriorityindeedexistssinceΩ hasfinite range. Playeriwinsfrompositionpifthereexistsastrategyσ forplayerisuchthatforanystrategy i σ fortheotherplayer(Player1−i)playeriwinsplay(p,σ ,σ ).WewriteW forthesetof 1−i 0 1 i positionsfromwhichPlayeriwins. Astrategyσ ispositionalifσ(p(0)..p(n))onlydependsonp(n).Playeriwinspositionally frompwhentheabovestrategyσ canbechosentobepositional. i Thefollowingisastandardresult. Theorem1. EverypositionpiseitherinW orinW andplayeriwinspositionallyfromevery 0 1 positioninW . i In view of this theorem we can now confine attention to positional strategies. A strategy that winsagainstallpositionalstrategiesisindeedawinningstrategy(againstallstrategies)sincethe optimalcounterstrategyisitselfpositional. Example1. Fig. 2 contains a graphical display of a parity game. Positions in Pos and Pos 0 1 are represented as circles and boxes, respectively, and labelled with their priorities. Formally, Pos ={a,b,c,d,e,f,g,h,i}andPos ={b,d,f,h}andPos ={a,c,e,g,i}andΩ(a)=3, 0 1 ...,and→={(a,b),(b,f),...}. IntherighthalfofFig.2thewinningsetsareindicatedandcorrespondingpositionalwinning strategiesaregivenasfatarrows.Themovesfrompositionsthatarenotintherespectivewinning setareomittedbutcanofcoursebefilledininanarbitraryfashion. 3.1 Certificationofwinningstrategies Givenaparitygamewithfinitelymanypositions,presentedexplicitlyasafinitelabelledgraph, andapartitionofPos intoV andV wearenowlookingforaneasytoverifycertificateasto 0 1 thefactthatV =W andV =W . 0 0 1 1 Inessence,suchacertificatewillconsistofapositionalstrategyσ foreachplayerisuchthat i iwinsusingσ fromeverypositionpinV .ClearlythisimpliesV =W andtheabovetheorem i i i i asserts that in principle such certificates always exist when V = W . However, it remains to i i explainhowwecancheckthatagivenpositionalstrategyσ winsfromagivenpositionp. i 6 MartinHofmann,HaraldRueß (cid:0)(cid:1)(cid:0)(cid:1) W (cid:0)(cid:1)(cid:0)(cid:1)W 0 (cid:0)(cid:1)(cid:0)(cid:1) 1 3 3 1 0 3 3 (cid:0)(cid:1)(cid:0)(cid:1)1(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)0(cid:0)(cid:1) a b c d a b (cid:0)(cid:1)(cid:0)(cid:1)c(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)d(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)(cid:0)(cid:1) 4 (cid:0)(cid:1)(cid:0)(cid:1)4(cid:0)(cid:1) e (cid:0)(cid:1)(cid:0)(cid:1)e(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)(cid:0)(cid:1) f g h i f g h (cid:0)(cid:1)(cid:0)(cid:1)i(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)(cid:0)(cid:1) 4 1 2 3 4 1 2 3 Fig.2.Aparitygameanditsdecompositionintowinningsets. Wefirstnotethatforthisitisenoughthatitwinsagainstanyadversarialpositionalstrategy becausethe“optimal”counterstrategy,i.e.,theonethatwinsfromalladversarialwinningposi- tionsispositional(bytheorem1).Thus,givenapositionalstrategyσ forplayeriwecanremove i alledgesfrompositionsp(cid:48) ∈Pos thatarenotchosenbythestrategyandintheremaininggame i graph look for a cycle whose largest priority has parity 1−i and is reachable from p. If there issuchacyclethenthestrategywasnotgoodandotherwiseitisindeedawinningstrategyfor Playeri. Algorithmically,theabsenceofsuchacyclecanbecheckedbystartingadepth-firstsearch fromeverypositionofadversarypriority(parity1−i)afterremovingallpositionsoffavourable andhigherpriority(parityi).Moreefficiently,onecandecomposethereachable(fromthepur- portedwinningset)partoftheremaininggraphintonontrivialstronglyconnectedcomponents (SCC).IfsuchanSCConlycontainspositionswhosepriorityhasparity1−ithen,clearly,the strategy is bad. Otherwise, one may remove the positions with the largest priority of parity i, decomposetheremaininggraphintoSCCsandcontinuerecursively.Essentially,thisisthestan- dard algorithm for nonemptiness of Strett automata described in [2]. This paper also describes anefficientalgorithmforSCCdecompositionthatcouldbeusedhere. Example2. AfterremovingtheedgesnottakenbyPlayer0accordingtohispurportedwinning strategyweobtainthefollowinggraph: (cid:0)(cid:1)(cid:0)(cid:1) W (cid:0)(cid:1)(cid:0)(cid:1)W 0 (cid:0)(cid:1)(cid:0)(cid:1) 1 3 3 (cid:0)(cid:1)(cid:0)(cid:1)1(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)0(cid:0)(cid:1) a b (cid:0)(cid:1)(cid:0)(cid:1)c(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)d(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)4(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)e(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)(cid:0)(cid:1) f g h (cid:0)(cid:1)(cid:0)(cid:1)i(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)(cid:0)(cid:1) 4 1 2 3 WeseethatthetworeachableSCCfromW are{a,b,f}and{g,h}.Thefirstonecontains 0 thecyclesa,f anda,b,f whichbothhavelargestpriority4.Theotheroneisitselfacyclewith largestpriority2. Likewise, adopting the viewpoint of Player 1, after removing the edges not taken by his strategyweobtain Certificationforµcalculuswithwinningstrategies 7 (cid:0)(cid:1)(cid:0)(cid:1) W (cid:0)(cid:1)(cid:0)(cid:1)W 0 (cid:0)(cid:1)(cid:0)(cid:1) 1 3 3 (cid:0)(cid:1)(cid:0)(cid:1)1(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)0(cid:0)(cid:1) a b (cid:0)(cid:1)(cid:0)(cid:1)c(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)d(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)4(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)e(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)(cid:0)(cid:1) f g h (cid:0)(cid:1)(cid:0)(cid:1)i(cid:0)(cid:1) (cid:0)(cid:1)(cid:0)(cid:1)(cid:0)(cid:1) 4 1 2 3 andfindthereachable(fromW )SCCstobe{c,d,i}.Theonlycyclesthereinared,eand 1 d,e,i.BotharegoodforPlayer1. 3.2 Game-theoreticcharacterization ThegameG(T,η)associatedwiththeLTST andηasaboveisthedefinedasfollows.Positions are pairs (s,φ) where FV(φ) ⊆ dom(η) and s ∈ S. In positions of the form (s,ψ) where ψ starts with ∨ or (cid:104)a(cid:105), it is proponent’s (Player 0) turn. The possible moves (for proponent to choosefrom)are: (s,ψ ∨ψ )(cid:32)(s,ψ ) 1 2 1 (s,ψ ∨ψ )(cid:32)(s,ψ ) 1 2 2 (s,(cid:104)a(cid:105)ψ)(cid:32)(t,ψ)where (s −a→ t)∈T. Inpositionsoftheform(s,ψ)whereψstartswith∧or[a]itistheopponent’sturn.Thepossible moves(foropponenttochoosefrom)are: (s,ψ ∧ψ )(cid:32)(s,ψ ) 1 2 1 (s,ψ ∧ψ )(cid:32)(s,ψ ) 1 2 2 (s,[a]ψ)(cid:32)(t,ψ)where(s −a→t)∈T. Inpositionsoftheform(s,QX.φ)theproponentistomove,butthereisonlyonepossiblemove: (s,µX.φ)(cid:32)(s,φ[X :=µX.φ]) (s,νX.φ)(cid:32)(s,φ[X :=νX.φ]) Inpositionsoftheform(s,X),(s,P),theproponentistomove,butthereisonlyonepossible move:(s,X)(respectively(s,P))itself.So,defacto,thegameendsinsuchaposition. Eachposition(s,φ)isassignedanaturalnumberΩ(s,φ),itspriority,asfollows: Ω(s,µX.φ)=2∗nd(µX.φ)+1 Ω(s,νX.φ)=2∗nd(νX.φ) Ω(s,P)=0 if P ∈T(s) Ω(s,P)=1 if P (cid:54)∈T(s) Ω(s,X)=0 if s∈η(X) Ω(s,X)=1 if s(cid:54)∈η(X) Ω(s,φ)=0 in all other cases. For any position (s,φ) we can consider the subgame consisting of the positions reachable from(s,φ).EvenifT isinfinitethissubgamehasonlyfinitelymanyprioritiesbecausetheonly secondcomponentsoccurringinreachablepositionsaresubformulasofφandone-stepunwind- ingsthereof.Thissubgameisthereforeaparitygametowhichtheprevioussectionapplies. 8 MartinHofmann,HaraldRueß Example3. Letφ=µX.P ∨(cid:104)a(cid:105)X whichassertsthatastatewhereP istruecanbereached. a DefinethetransitionsystemT by|T|={s,t}and−→ ={(s,s),(s,t),(t,t)}andT(s)= T ∅andT(t)={P}.Theassociatedgamegraphisasfollows φ,s a P ∨(cid:104)a(cid:105)φ,s a P,s a a a (cid:104)a(cid:105)φ,s a a φ,t a P ∨(cid:104)a(cid:105)φ,t a P,t The priorities of the positions labelled (φ,s),(φ,t),(P,s) are 1; the priorities of the three otherpositionsare0. Player0winsfromeverypositionexcept(P,s).Thewinningstrategymovesto((cid:104)a(cid:105)φ,s)and then (φ,t) and then (P,t). Note that a strategy that moves from (P ∨(cid:104)a(cid:105)φ,s) to (φ,s) looses eventhoughitneverleavesthewinningsetW .Thus,inordertocomputewinningstrategiesit 0 isnotenoughtochooseanymovethatremainsinthewinningset. Theorem2. Ifs∈ φ ηthenproponentwinsG(T,η)from(s,φ). (cid:74) (cid:75) Beforeprovingthis,wenotethattheconverseisinthiscaseactuallyarelativelysimpleconse- quence. Corollary1. IfproponentwinsG(T,η)from(s,φ)thens∈ φ η. (cid:74) (cid:75) Proof. SupposethatproponentwinsG(T,η)from(s,φ)ands(cid:54)∈ φ η.Wethenhaves∈ φ∗ η(cid:48) usingLemma2fortheformaldualisationforformulasandcomp(cid:74)lem(cid:75) entationforenviron(cid:74)men(cid:75)ts. Thus, by the theorem, proponent wins G(T,η(cid:48)) from (s,φ∗). However, it is easy to see that a winningstrategyforproponentinG(T,η(cid:48))from(s,φ∗)istantamounttoawinningstrategyfor opponentinG(T,η)from(s,φ);sowegetacontradictionusingtheorem1. Proof (ofTheorem2).TheproofofTheorem2nowworksbyinductiononφ.Thecaseswhere φisaformulawithanoutermostfixpointaretheinterestingones. IncaseφisoftheformµX.ψ,define U :={t|proponent wins G(T,η)from (t,µX.ψ)}. Wemustshowthat φ η ⊆U.Bydefinitionof φ ηitsufficestoshowthat ψ η[X (cid:55)→U]⊆U. Thus, suppose that(cid:74)t ∈(cid:75) ψ η[X (cid:55)→U]. By the(cid:74)in(cid:75)duction hypothesis this m(cid:74)ea(cid:75)ns that proponent winsG(T,η[X (cid:55)→U])fr(cid:74)om(cid:75) (t,ψ).Callthecorrespondingwinningstrategyσ.Weshouldprove thatproponentalsowinsfrom(t,µX.ψ).Wemoveto(t,ψ[X :=µX.ψ])andplayaccordingto σuntilwereachastate(t(cid:48),µX.ψ)atwhichpointweknowthatt(cid:48) ∈U sowecanthencontinue toplayaccordingtothestrategyembodiedinthatstatement.Ofcourse,ifweneverreachsucha positionthenσwillwinthewholegame. In case φ is of the form νX.ψ define U := νX.ψ η. We define a winning strategy for positionsoftheform(t,νX.ψ)wheret∈U asfoll(cid:74)ows.Fi(cid:75)rst,wemove(forcedly)to(t,ψ[X := νX.ψ]).Weknowthatt ∈ ψ η[X (cid:55)→U]byunwindingsothat,inductively,wehaveastrategy that allows us to either win(cid:74)ri(cid:75)ghtaway, or move to another position (t(cid:48),νX.ψ) where t(cid:48) ∈ U andallprioritiesencounteredonthewayaresmallerthantheoneofνX.ψ duetothedefinition Certificationforµcalculuswithwinningstrategies 9 of nesting depth and in particular Lemma 1. We start over and unless we eventually do win rightaway at some point we would have seen the priority of νX.ψ infinitely often which is the largestandeven. Weremarkthatwhilethepreviousresultiswell-knowntheproofpresentedhereisquitedifferent fromtheonesinthestandardliterature,e.g.[4]whichusestheorder-theoreticconceptofsigna- turesandarelesscompositionalthanoursinthesensethattheproofisnotdirectlybystructural inductiononformulasbutratherontheglobaldevelopmentofallthefixpoints. 4 Computingwinningstrategiesviafixpointiteration 4.1 Fixpointiteration Itiswell-knownthatthefixpointiterationinFigure1computes φ ηinthefinitecase.Ourgoal is to somehow instrument this algorithm so that it produces evi(cid:74)den(cid:75)ce in the form of a winning strategy.Ininstrumentingthisalgorithmtoproduceevidenceintheformofawinningstrategyit isnotenoughtosimplycomputethewinningsetsusingsem( , )andthensimplychoosemoves thatdonotleavethewinningset.Thisisbecauseofexampleslike3whichshowthatastrategy thatneverleavesthewinningsetmaynonethelessbelosing. Instead we will use the construction from the proof of Theorem 2. Some care needs to be takenwiththeexactsetupofthetyping;inparticular,ouralgorithmwillreturnpartialwinning strategies(thatwinonasubsetofthewholewinningset)butonlyrequiresetsofstates(rather thanpartialwinningstrategies)asthevaluesoffreevariables. 4.2 Computingwinningstrategies Partialwinningstrategies. ApartialwinningstrategyisapartialfunctionΣ mappingpositions of the game G(T,η) to elements of S extended with {1,2,∗}; it must satisfy the following conditions: STAR IfΣ(φ,s)=∗thenallimmediatesuccessorsof(φ,s)areindom(Σ); OR IfΣ(φ,s)=i∈{1,2}thenφisoftheformφ ∨φ and(φ ,s)∈dom(Σ); 1 2 i DIA IfΣ(φ,s)=s(cid:48) ∈S thenφisoftheform(cid:104)a(cid:105)ψands −a→ s(cid:48)and(ψ,s(cid:48))∈dom(Σ). WIN Player0winsfromallthepositionsindom(Σ)andtheobviousstrategyinduced2byΣ isa winningstrategyforPlayer0fromthosepositions. Notethattheemptyfunctionisinparticularapartialwinningstrategy.Toillustratethenotation wedescribea(partial)winningstrategyfortheentirewinningsetforExample3: Σ(φ,s)=∗ Σ(P ∨(cid:104)a(cid:105)φ,s)=2 Σ((cid:104)a(cid:105)φ,s)=t Σ(φ,t)=∗ Σ(P ∨(cid:104)a(cid:105)φ,t)=1 Σ(P,t)=∗, and undefined elsewhere. So, dom(Σ) = {(φ,s),...,(P,t)} and, indeed, player 0 wins from all these positions by fol- lowingtheadvicegivenbyΣ.Ofcourse,Σ(cid:48)(P,t)=∗andundefinedelsewhereisalsoapartial winningstrategyalbeitwithsmallerdomainofdefinition. 2Arbitrarymovesoutsidedom(Σ)+removethe*-setting. 10 MartinHofmann,HaraldRueß Updating of winning strategies. Suppose that Σ and Σ(cid:48) are partial winning strategies. A new partialwinningstrategyΣ+Σ(cid:48)withdom(Σ+Σ(cid:48))isdefinedby (Σ+Σ(cid:48))(φ,s)=if (φ,s)∈dom(Σ)then Σ(φ,s)else Σ(cid:48)(φ,s). Lemma3. Σ+Σ(cid:48)isapartialwinningstrategyanddom(Σ+Σ(cid:48))=dom(Σ)∪dom(Σ(cid:48)) Proof. A play following Σ +Σ(cid:48) will eventually remain in one of Σ or Σ(cid:48); this, together with thefactthatinitialsegmentsdonotaffecttheoutcomeofagameimpliestheclaim. Let φ be a formula and let Σ be a partial winning strategy for G(T,η[X (cid:55)→ S]) such that the mapping (ρ,s) (cid:55)→ (ρ[X := ψ],s) is injective on dom(Σ). Furthermore, let Σ(cid:48) be a winning strategy for G(T,η) such that (φ,s)|s∈S is contained in dom(Σ(cid:48)). A new partial strategy Σ[X :=φ,Σ(cid:48)]isdefinedby Σ[X :=φ,Σ(cid:48)](ρ,s)=if (ρ,s)∈dom(Σ(cid:48))then Σ(cid:48)(ρ,s)else if exists ψ,ρ=ψ[X :=φ]then Σ(ψ,s)else undef Lemma4. UndertheassumptionsmadethestrategyΣ[X :=φ,Σ(cid:48)]isindeedapartialwinning strategyforthegameG(T,η)and{(ρ[X :=φ],s)|(ρ,s)∈dom(Σ)}⊆dom(Σ[X :=φ,Σ(cid:48)]). Proof. Injectivity of the substitution [X := φ] shows that Σ[X := φ,Σ(cid:48)] is well defined. A game according to Σ[X := Σ(cid:48)] starting from ρ[X := φ] either stays completely in Σ or else reachesoneofthepositions(X,s)atwhichpointΣ(cid:48)takesover. 4.3 Computingwinningstrategiesbyfixpointiteration For any formula φ and environment η with dom(η) ⊇ FV(φ) we define a partial winning strategySEM(φ) bythefollowingclauses: η SEM(X) =λρ,s.if ρ=X and s∈η(X)then ∗ else undef η SEM(P) =λρ,s.if ρ=X and P ∈T(s)then ∗ else undef η SEM(φ∧ψ) =SEM(φ) η η +SEM(ψ) η +λρ,s.if ρ=φ∧ψand (s,φ)∈dom(SEM(φ) )and (s,ψ)∈dom(SEM(φ) ) η η then ∗ else undef SEM(φ∨ψ) =SEM(φ) η η +SEM(ψ) η +{(φ∨ψ,s)(cid:55)→1|(φ,s)∈dom(SEM(φ) )} η +{(φ∨ψ,s)(cid:55)→2|(ψ,s)∈dom(SEM(φ) )} η SEM([a]φ) =SEM([a]φ) η η SEM((cid:104)a(cid:105)φ) =SEM(φ) η η +{((cid:104)a(cid:105)φ,s)(cid:55)→(φ,s(cid:48))|(φ,t)∈dom(SEM(φ) ),s −a→ s(cid:48)} η