Model Checking Abilities under Incomplete Information Is Indeed ∆ P 2 -complete

Model Checking Abilities under Incomplete Information Is Indeed ∆ P 2 -complete WojciechJamroga wjamroga@in.tu-clausthal.de Department of Informatics Clausthal University of Technology

Germany

JürgenDix dix@in.tu-clausthal.de Department of Informatics Clausthal University of Technology

Germany

Model Checking Abilities under Incomplete Information Is Indeed ∆ P 2 -complete AD158833D82AD5368B806C0BF9D55D6F GROBID - A machine learning software for extracting information from scholarly documents multi-agent systems model checking temporal logic strategic ability computational complexity

We study the model checking complexity of Alternating-time temporal logic with imperfect information and imperfect recall (atlir). Contrary to what we have stated in [11], the problem turns out to be ∆ P 2 -complete, thus conrming the initial intuition of Schobbens [18]. We prove

2 -hardness through a reduction of the SNSAT problem, while the membership in ∆ P 2 stems from the algorithm presented in [18].

1 Introduction elterntingEtime temporl logi ID P is one of the most interesting frmeworks tht emerged reE ently for resoning out omputtionl systemsF Atl ir is vrint of atlD proposed y hoens in IV for gents with imperfect information nd imperfect recallF e hve lredy investigted the omplexity of atl ir model heking in IID onluding tht the prolem is NPEompleteF nfortuntelyD our lim ws inorretY we set it right with this pperF e egin with presenttion of the frmeworks of atl nd atl ir F hen we present some existing omplexity results with respet to atl ir model hekingD nd we give n lterntive proof of NPEhrdness of the prolemF sn etion QFPD we extend the onstrution to present redution of SNSATD thus proving tht model heking atl ir is ∆ P 2 EhrdF es the memership in ∆ P 2 stems from the lgorithms presented in oth IV nd IID we get tht model heking atl ir is

∆ P 2 EompleteF

Atl ir n e seen s the oreD miniml atlEsed lnguge for ility under inomplete inforE mtionX it does not ontin ny super)uous formule or opertorsF his is no forml sttement " other reserhers might ome up with weker lnguge tht they onsider ppropriteF xevertheE lessD atl ir is susumed y the mjority of existing logis tht omine strtegies nd qulittive unertintyF fy proving ∆ P 2 Eompleteness of atl ir model hekingD we otin lower ound for model heking of virtully ll logis of this kindD nd for most of them the ound is tightF 2 What Agents Can Achieve Atl ID P hs een invented y elurD renzinger nd uupfermn in order to pture properties of open computational systems @suh s omputer networksAD where di'erent omponents n t utonomouslyD nd omputtions in suh systems result from their omined tionsF elterntivelyD atl n serve s logi for systems involving multiple gentsD tht llows one to reson out wht gents n hieve in gmeElike senriosF es atl does not inlude inomplete informtion in its sopeD it n e seen s logi for resoning out gents who lwys hve omplete knowledge out the urrent stte of 'irsF 2.1 ATL: Ability in Perfect Information Games

Atl is generliztion of the rnhing time temporl logi ctl RD SD in whih pth qunti(ers re repled with so lled cooperation modalitiesF pormul A ϕD where A ⊆ Agt is olition of gents @Agt is the set of ll gentsAD expresses tht olition A hs olletive strtegy to enfore ϕF Atl formule inlude temporl opertorsX g @in the next stteAD @lwys from now onA nd U @untilAF ypertor ♦ @now or sometime in the futureA n e de(ned s ♦ϕ ≡ U ϕF vike in ctlD every ourrene of temporl opertor is immeditely preeded y extly one oopertion modlityF 1 he roder lnguge of atl * D in whih no suh restrition is imposedD is not used in this pperF e numer of semntis hve een de(ned for atlD most of them equivlent TD UF sn this pperD we refer to vrint of concurrent game structuresD whih inludes nonempty (nite set of ll gents Agt = {1, ..., k}D nonempty set of sttes StD set of tomi propositions ΠD vlution of propositions π : Π → P(St)D nd the set of @tomiA tions ActF puntion d : Agt × St → P(Act) de(nes nonempty sets of tions ville to gents t eh stteD nd o is @deterministiA trnsition funtion tht ssigns the outome stte q = o(q, α 1 , . . . , α k ) to stte q nd tuple of tions α 1 , . . . , α k tht n e exeuted y the gent in qF e strategy s a of gent a is onditionl pln tht spei(es wht a is going to do for every possile stte @iFeFD s a : St → Act suh tht s a (q) ∈ d a (q)AF2 e collective strategy S A for group of gents A ⊆ Agt is tuple of strtegiesD one per gent from AF e path λ in model M is n in(nite sequene of sttes tht n e rehed y susequent trnsitionsD nd refers to possile ourse of tion @or possile omputtionA tht my our in the systemY y λ[i]D we denote the ith position on pth λF puntion out(q, S A ) returns the set of ll pths tht my result from gents A exeuting strtegy S A from stte q onwrdF xowD informlly spekingD M, q |= A ϕ i' there is olletive strtegy S A suh tht ϕ holds for every λ ∈ out(q, S A )F sn etion PFQD we give more preise semnti de(nition of atl ir D whih is the min sujet of our studyF yne of the most ppreited fetures of atl is its model heking omplexity ! liner in the numer of trnsitions in the model nd the length of the formulF roweverD fter reful inspeE tionD this result is not s good s it seemsF his liner omplexity is no more vlid when we mesure the size of models in the number of states, actions and agents IHD ITD or when we represent systems in more ompt wy IWF tillD we hve the followingF Proposition 1 ([2]) The atl model checking problem is ptime-complete, and can be done in time O(ml), where m is the number of transitions in the model and l is the length of the formula.

Strategic Abilities under Incomplete Information

Atl nd its models inlude no wy of ddressing unertinty tht n gent or proess my hve out the urrent situtionF woreoverD strtegies in atl n de(ne di'erent hoies for ny pir of di'erent sttesD hene implying tht n gent n reognize eh @glolA stte of the systemD nd t ordinglyF husD it n e rgued tht the logi is tilored for desriing nd nlyzing systems in whih every gentGproess hs complete and accurate knowledge out the urrent stte of the systemF his is usully not the se for most pplition dominsD where proess n ess its local stteD ut the stte of the environment nd the @lolA sttes of other gents n e oserved only prtillyF yne of the min hllenges for logi of strtegi ilities under inomplete informtion is the question of how gents9 knowledge should interfere with the gents9 ville strtegiesF he erly pprohes to atl with inomplete informtion PD eFUFPDPHD PI did not hndle this interE tion in ompletely stisftory wy @fF WD IVD ISAD whih triggered )urry of logisD proposed to overome the prolems WD IPD IVD ISD PPD VD IQF wost of the proposls gree tht only uniform strtegies @iFeFD strtegies tht speify the sme hoies in indistinguishle sttesA re relly exeE utleF roweverD in order to identify suessful strtegyD the gents must onsider not only the ourses of tions strting from the urrent stte of the systemD ut lso those strting from sttes tht re indistinguishle from the urrent oneF here re mny ses hereD espeilly when group epistemis is onernedX the gents my hve commonD mutual or distributed knowledge out strtegy eing suessfulD or they my e given hint for the right strtegy y distinguished memer @the ossAD sugroup @hedqurters ommitteeA or even nother group of gents @onE sulting ompnyA etF wost existing solutions tret only some of the ses @leit rther in n elegnt wyAD while the others o'er very generl tretment of the prolem t the expense of omplited logil lnguge @whih is y no mens elegntAF e elieve tht n elegnt nd generl solution hs een reently proposed in the form of gonstrutive trtegi vogi IQD IRD ut this lim is yet to e veri(edF Atl ir stnds out mong the existing solutions for its simpliityF hile y no mens the most expressiveD we elieve it n e treted s the oreD miniml atlEsed lnguge for ility under inomplete informtionF his is no forml sttementY we just nnot think of sustntilly weker temporl lnguge to express ilities of gentsF

ATL ir

Atl ir inludes the sme formule s atlD only the oopertion modlities re presented with susriptX A ir to indite tht they ddress gents with imperfet information nd imperfet recallF pormllyD the reursive de(nition of atl ir formule isX

ϕ ::= p | ¬ϕ | ϕ ∧ ϕ | A ir g ϕ | A ir ϕ | A ir ϕ U ϕ eginD we de(ne A ir ♦ϕ ≡ A ir U ϕF

wodels of atl ir D imperfect information concurrent game structures @icgsAD n e presented s onurrent gme strutures ugmented with fmily of epistemi indistinguishility reltions ∼ a ⊆ St × StD one per gent a ∈ AgtF he reltions desrie gents9 unertintyX q ∼ a q mens thtD while the system is in stte qD gent a onsiders it possile tht it is in q nowF st is required tht gents hve the sme hoies in indistinguishle sttesF o repitulteD icgs n e de(ned s tuples

M = Agt, St, Π, π, Act, d, o, ∼ 1 , ..., ∼ k , whereX • Agt = {1, ..., k} is (nite nonempty set of ll gentsD • St is nonempty set of sttesD • Π is set of tomi propositionsD • π : Π → P(St) is vlution of propositionsD • Act is (nite nonempty set of @tomiA tionsY • funtion d : Agt × St → P(Act) de(nes tions ville to n gent in stteY d(a, q) = ∅ for ll a ∈ Agt, q ∈ StD • o is @deterministiA trnsition funtion tht ssigns outome sttes to sttes nd tuples of tionsY tht isD o(q, α 1 , . . . , α k ) ∈ St for every q ∈ St nd α 1 , . . . , α k ∈ d(1, q) × • • • × d(k, q)Y • ∼ 1 , ..., ∼ k ⊆ St ×

St re epistemi reltionsD one per gentF ivery ∼ a is ssumed to e n equivleneF e require tht q ∼ a q implies d(a, q) = d(a, q )F eginD @memorylessA strtegy of gent a is onditionl pln tht spei(es wht a is going to do in every possile stteF en exeutle pln must presrie the sme hoies for indistinguishle sttesF herefore atl ir restrits the strtegies tht n e used y gents to the set of so lled uniform strtegiesF e uniform strategy of gent a is de(ned s funtion s a : St → ActD suh thtX @IA s a (q) ∈ d(a, q)D nd @PA if q ∼ a q then s a (q) = s a (q )F e collective strategy for group of gents A = {a 1 , ..., a r } is tuple of strtegies S A = s a1 , ..., s ar D one per gent from AF e olletive strtegy is uniform if it ontins only uniform individul strtegiesF eginD funtion out(q, S A ) returns the set of ll pths tht my result from gents A exeuting strtegy S A from stte q onwrdX 3 3 The notation S A (a) stands for the strategy sa of agent a in the tuple S A = sa 1 , ..., sa r . pigure IX qmling oots gme out(q, S A ) = {λ = q 0 q 1 q 2 ... | q 0 = q nd for every i = 1, 2, ... there exists tuple of gents9 deisions

q 0 q w q l win q AK q AQ q KQ q KA q QA q QK a a a b b b keep,chg keep,α i−1 1 , ..., α i−1 k suh tht α i−1 a = S A (a)(q i−1 ) for eh a ∈ AD α i−1 a ∈ d(a, q i−1 ) for eh a / ∈ AD nd o(q i−1 , α i−1 1 , ..., α i−1 k ) = q i }F

he semntis of atl ir formule is de(ned s followsF he (rst three lines re oviousD similr to the de(nition of truth in uripke modelsF hile the (rst sttes tht n tomi proposition is true in model nd stte i' the vlution mkes it true in this stteD the next two lines de(ne the usul mening of ¬ϕ nd ϕ ∧ ψF vines R!T de(ne the mening of oopertion modlitiesF

M, q |= A ir g ϕ i' there exists uniform strtegy S A suh thtD for every a ∈ AD q ∈ St suh tht q ∼ a q D nd λ ∈ out(S A , q )D we hve M, λ[1] |= ϕY M, q |= A ir ϕ i' there exists uniform strtegy S A suh thtD for every a ∈ AD q ∈ St suh tht q ∼ a q D nd λ ∈ out(S A , q )D we hve M, λ[i] |= ϕ for every i ≥ 0Y

M, q |= A ir ϕ U ψ i' there exist uniform strtegy S A suh thtD for every a

∈ AD q ∈ St suh tht q ∼ a q D nd λ ∈ out(S A , q )D there is i ≥ 0 for whih M, λ[i] |= ψD nd M, λ[j] |= ϕ for every 0 ≤ j < iF

ht isD A ir ϕ if olition A hs uniform strtegyD suh tht for every pth that can possibly result from execution of the strategy according to at least one agent from AD ϕ is the seF his is strong requirementD euse it su0es tht t lest one of the gents in A onsiders some sttes q, q equivlentX thenD ll relevnt pths strting from oth q nd q must e onsideredF xote tht the universl pth qunti(er A @for every pthA from ctl n e expressed in atl ir s ∅ ir F Example 1 (Gambling robots) Two robots (a and b) play a simple card game. The deck consists of Ace, King and Queen (A, K, Q). Normally, it is assumed that A is the best card, K the second best, and Q the worst. Therefore A beats K and Q, K beats Q, and Q beats no card. At the beginning of the game, the environment agent deals a random card to both robots (face down), so that each player can see his own hand, but he does not know the card of the other player. Then robot a can exchange his card for the one remaining in the deck (action exch), or he can keep the current one (keep). At the same time, robot b can change the priorities of the cards, so that Q becomes better than A (action chg) or he can do nothing (nop), i.e. leave the priorities unchanged. If a has a better card than b after that, then a win is scored, otherwise the game ends in a losing state. An icgs M 1 for the game is shown in Figure 1.

It is easy to see that M 1 , q 0 |= ¬ a ir ♦win, because, for every a's (uniform) strategy, if it guarantees a win in e.g. state q AK then it fails in q AQ (and similarly for other pairs of indistinguishable states). Let us also observe that M 1 , q 0 |= ¬ a, b ir ♦win (in order to win, a must exchange his card in state q QK , so he must exchange his card in q QA too (by uniformity), and playing exch in q QA leads to the losing state). On the other hand, M 1 , q AQ |= a, b ir g win (a winning strategy: s a (q AK ) = s a (q AQ ) = s a (q KQ ) = keep, s b (q AQ ) = s b (q KQ ) = s b (q AK ) = nop; q AK , q AQ , q KQ are the states that must be considered by a and b in q AQ ). Still, M 1 , q AK |= ¬ a, b ir g win.

hoens IV proved tht atl ir model heking is NPEhrd nd ∆ P 2 EesyF re lso onjetured tht the prolem is ∆ P 2 EompleteF e prove tht it is indeed the se in etion QF 3 Model Checking ATL ir hoens IV proved tht atl ir model heking is intrtleX more preiselyD it is NPEhrd nd ∆ P 2 Eesy when the size of the model is de(ned in terms of the numer of trnsitionsF re lso onjetured tht the prolem is ∆ P 2 EompleteF sn this setionD we lose the gp nd prove tht it is ∆ P 2 EhrdD nd hene indeed ∆ P 2 EompleteF he proof proeeds y redution of the SNSAT prolem to atl ir model hekingD presented in etion QFPF e prolem is in ∆ P 2 = P NP if it n e solved in deterministi polynomil time with sulls to n NPEorle @we refer the reder to IUD Q for more detiled informtion out omplexity lsses nd their omplete prolemsAF glss ∆ P 2 elongs to the (rst level of the polynomil hierrhy @lthough the index suggests it elongs to the seond levelAF he lss is supposed to e just ove NP @unless the polynomil hierrhy ollpsesAX

NP ∪ coENP ⊆ ∆ P 2 ⊆ Σ P 2 ∩ Π P 2 .

where Σ P 2 = NP NP D nd Π P 2 = coENP NP F e hve lredy investigted the omplexity of atl ir model heking in IID onluding tht the prolem is NPEompleteF nfortuntelyD our lim ws inorretX we set it right in this pperF

Existing Results

wodel heking atl ir hs een proved to e NPEhrd nd ∆ P 2 Eesy in the numer of trnsitions nd the length of the formul IVF he memership in ∆ P 2 ws demonstrted through the following oservtionF sf the formul to e model heked is of the form A ir ϕ @ϕ eing g ψD ψ or ψ 1 U ψ 2 AD where ϕ ontins no more oopertion modlitiesD then it is su0ient to guess strtegy for AD trim the model y removing ll trnsitions tht will never e exeuted @ording to this strtegyAD nd model hek ctl formul Aϕ in the resulting modelF husD model heking n ritrry atl ir formul n e done y heking the suformule itertivelyD whih requires polynomil numer of lls to n NP lgorithmF 4he NPEhrdness follows from redution of the well known SAT prolemF rereD we present redution whih is somewht di'erent from the one in IVF e will dpt it in etion QFP to prove ∆ P 2 EhrdnessF sn SATD we re given gxp formul

ϕ ≡ C 1 ∧ . . . ∧ C n involving k propositionl vriles from set X = {x 1 , ..., x k }F ih luse C i n e written s C i ≡ x si,1 1 ∨ . . . ∨ x s i,k

k D where s i,j ∈ {+, −, 0}Y x + j denotes positive ourrene of x j in C i D x − j denotes n ourrene of ¬x j in C i D nd x 0 j indites tht x j does not our in C i F he prolem sks if ∃X.ϕD tht isD if there is vlution of x 1 , ..., x k suh tht ϕ holdsF e onstrut the orresponding icgs M ϕ s followsF here re two plyersX veri(er v nd refuter rF he refuter deides t the eginning of the gme whih luse C i will hve to e stis(edX it is done y proeeding from the initil stte q 0 to luse stte q i F et q i D veri(er deides @y proeeding to proposition stte q i,j A whih of the literls x si,j j from C i will e ttemptedF pinllyD t q i,j D veri(er ttempts to prove C i y delring the underlying propositionl vrile x j true @tion A or flse @tion ⊥AF sf she sueeds @iFeFD if she exeutes for x + j D or exeutes ⊥ for x − j AD then the system proeeds to the winning stte q F ytherwiseD the system stys in q i,j F edditionllyD proposition sttes referring to the sme vrile re indistinguishle for veri(erD so q 0 q 1,1 q 1,3 q 2,1 q 2,2 q 2,3 q 1 q 2 v:1 v:v where St cl = {q 1 , . . . , q n }D nd St prop = {q 1,1 , . . . , q 1,k , . . . , q n,1 , . . . , q n,k }Y

• Π = {yes}D π(yes) = {q }D • Act = {1, ..., max(k, n), , ⊥}D • d(v, q 0 ) = d(v, q ) = {1}D d(v, q i ) = {1, ..., k}D d(v, q i,j ) = { , ⊥}Y d(r, q) = {1, ..., n} for q = q 0 D nd d(r, q) = {1} otherwiseY • o(q 0 , 1, i) = q i D

o(q i , j, 1) = q i,j D o(q i,j , , 1) = q if s i,j = +D nd q i,j otherwiseD o(q i,j , ⊥, 1) = q if s i,j = −D nd q i,j otherwiseY

• q 0 ∼ v q i' q = q 0 D q i ∼ v q i' q = q i D q i,j ∼ v q i' q = q i ,j F es n exmpleD model M ϕ for ϕ ≡ (x 1 ∨ ¬x 3 ) ∧ (¬x 1 ∨ x 2 ∨ x 3 ) is presented in pigure PF Theorem 2 ϕ is satisable i M ϕ , q 0 |= v ir ♦yes.

Proof.

(⇒) pirstlyD if there is vlution tht mkes ϕ trueD then for every luse C i one n hoose literl out of C i tht is mde true y the vlutionF he hoieD together with the vlutionD orresponds to uniform strtegy for v suh thtD for ll possile exeutionsD q is hieved t the endF (⇐) gonverselyD if M ϕ , q 0 |= v ir ♦yesD then there is strtegy s v suh tht q is hieved for ll pths from out(q 0 , s v )F fut then the vlutionD whih ssigns propositions x 1 , ..., x k with the sme vlues s s v D stis(es ϕF foth the numer of sttes nd trnsitions in M ϕ re liner in the length of ϕD nd the onstruE tion of M requires liner time tooF husD the model heking prolem for atl ir is NPEhrdF xote tht it is NPEhrd even for formule with single oopertion modlityD nd turnEsed models with t most two gentsF5 e lredy investigted the omplexity of atl ir model heking in IID onluding tht the prolem ws NPEompleteF nfortuntelyD our lim ws inorretX the error ourred in the wy we hndled negtion in our model heking lgorithm @fF ITAF tillD s oserved y vroussinieD wrkey nd yreiy in ITD our lgorithm is orret for positive atl ir ! iFeFD atl ir without negtionF husD the following holdsF Proposition 3 Model checking of positive atl ir is NP-complete with respect to the number of transitions in the model and the length of the formula. he ∆ P 2 Ehrdness for the full atl ir is proved in etion QFPF

3.2

Model Checking ATL ir Is Indeed ∆ P 2 -complete vet us (rst rell @fter ITA the de(nition of SNSATD typil ∆ P 2 Ehrd prolemF Denition 1 (SNSAT)

Input: p sets of propositional variables X r = {x 1,r , ..., x k,r }, p propositional variables z r , and p Boolean formulae ϕ r in CNF, with each ϕ r involving only variables in X r ∪ {z 1 , ..., z r−1 }, with the following requirement:

z r ≡ there exists an assignment of variables in X r such that ϕ r is true.

We will also write, by abuse of notation, z r ≡ ∃X r ϕ r (z 1 , ..., z r−1 , X r ).

Output: The truth-value of z p (i.e., or ⊥).

vet n e the mximl numer of luses in ny ϕ 1 , ..., ϕ p from the given inputF xowD eh ϕ r n e written sX

ϕ r ≡ C r 1 ∧ . . . ∧ C r n , and C r i ≡ x s r i,1 1,r ∨ . . . ∨ x s r i,k k,r ∨ z s r i,k+1 1 ∨ . . . z s r i,k+r−1 r−1

. eginD s r i,j ∈ {+, −, 0}Y x + denotes positive ourrene of xD x − denotes n ourrene of ¬xD nd x 0 indites tht x does not our in the luseF imilrlyD s r i,k+j de(nes the sign of z j in luse C r i F qiven suh n instne of SNSATD we onstrut sequene of onurrent gme strutures M r for r = 1, ..., p in similr wy to the onstrution in etion QFIF ht isD luses nd vriles x i,r re hndled in extly the sme wy s eforeF woreoverD if z i ours s positive literl in ϕ r D we emed M i in M r D nd dd trnsition to the initil stte q i 0 of M i F sf ¬z i ours in ϕ r D we do lmost the smeX the only di'erene is tht we split the trnsition into two stepsD with stte neg r i @leled with n atl ir proposition negA dded in etweenF

wore formllyD M r = Agt, St r , Π, π r , Act r , d r , o r , ∼ r 1 , ..., ∼ r k D whereX • Agt = {v, r}D • St r = {q r 0 , q r 1 , . . . , q r n , q r 1,1 , . . . , q r n,k , neg r 1 , . . . , neg r r−1 , q } ∪ St r−1 D • Π = {yes, neg}D π r (yes) = {q }D π r (neg) = {neg j i | i, j = 1, ..., r}D • Act r = {1, ..., max(k + r − 1, n), , ⊥}D • d r (v, q r 0 ) = d r (v, neg r i ) = d r (v, q ) = {1}D d r (v, q r i ) = {1, ..., k + r − 1}D d r (v, q r i,j ) = { , ⊥}D d r (r, q) = {1, ..., n} for q = q r 0 nd {1} for the other q ∈ St r F por q ∈ St r−1 D we simply inlude the funtion from M r−1 X d r (a, q) = d r−1 (a, q)Y • o r (q r 0 , 1, i) = q r i D o r (q r i , j, 1) = q r i,j for j ≤ kD o r (q r i , k + j, 1) = q j if s r i,k+j = +D nd o r (q r i , k + j, 1) = neg r j if s r i,k+j = −D o r (neg r j , 1, 1) = q j D o r (q r i,j , , 1) = q if s r i,j = +D nd q r i,j otherwiseD o r (q r i,j , ⊥, 1) = q if s r i,j = −D nd q r i,j otherwiseF por q ∈ St r−1 D we inlude the trnsitions from M r−1 X o r (q, α) = o r−1 (q, α)Y q 0 q 1,1 q 2,1 q 1,2 q 2,1 q 1 q 1 q 2 q 2 v:1 v:1 v:v :r :1 r:1 v:2 v:2 v:1 r:2 r:2 x 1 z 1 x 3 x 2 Øx 1 Øz 1 Øz 1 Øx 3 v: v: ^v: ^yes neg neg q M1 M 2 M 3 q 0 q 0 neg 1 q 1 q 2 r:1 r:2 neg 2 neg 1 q 1,1 neg Øz 2 v:1 v:2

pigure QX en icgs for the redution of SNSAT

• q r 0 ∼ v q i' q = q r 0 D q r i ∼ v q i' q = q r i D q r i,j ∼ v q i' q = q r i ,j F por q, q ∈ St r−1 D we inlude the tuples from

M r−1 X q ∼ r v q i' q ∼ r−1 v q F es n exmpleD model M 3 for ϕ 3 ≡ (x 3 ∨ ¬z 2 ) ∧ (¬x 3 ∨ ¬z 1 )D ϕ 2 ≡ z 1 ∧ ¬z 1 D ϕ 1 ≡ (x 1 ∨ x 2 ) ∧ ¬x 1 D is presented in pigure QF Theorem 4 Let Φ 1 ≡ v ir (¬neg) U yes, Φ i ≡ v ir (¬neg) U (yes ∨ (neg ∧ A g ¬Φ i−1 )).

Now, for all r: z r is true i M r , q r 0 |= Φ r .

fefore we prove the theoremD we stte n importnt lemmF vemm S sys tht overlong formule Φ i do not introdue new properties of model M r F wore preiselyD formul Φ i tht inludes more nestings thn model M r n e s well redued to

Φ i−1 when model heked in M r , q r 0 F Lemma 5 For i ≥ r: M r , q r 0 |= Φ i i M r , q r 0 |= Φ i+1 .

Proof (induction on r).

xote thtD y the onstrution of M r D λ[u + 1] must refer to the initil stte q j 0 of some sumodel

Proof of Theorem 4 (induction on r).

IF por r = 1X we use the proof of heorem PF PF por r > 1X

For the implication from left to right (⇒): let z r e trueX thenD there is vlution of X r suh tht ϕ r holdsF e onstrut s v s in the proof of heorem PF sn se tht some x s i hs een hosen in luse C r i D we re doneF sn se tht some z − j hs een hosen in luse C r i @noteX j must e smller thn iAD we hve @y indutionA tht M j , q j 0 |= ¬Φ j F fy vemm SD lso M j , q j 0 |= ¬Φ r D nd hene M r , q j 0 |= ¬Φ r F o we n mke the sme hoie @iFeFD z − j A in s v D nd this will led to stte neg r j D in whih it holds tht neg ∧ A g ¬Φ r F sn se tht some z + j hs een hosen in luse C r i D we hve @y indutionA tht M j , q j 0 |= Φ j D nd heneD y vemm SD M j , q j 0 |= Φ r F ht isD there is strtegy s v in M j suh tht (¬neg) U (yes ∨ (neg ∧ A g ¬Φ r−1 )) holds for ll pths from out(q j 0 , s v )F es the sttes in M j hve no epistemi links to sttes outside of itD we n merge s v into s v F For the other direction (⇐): let M r , q r 0 |= Φ r ≡ v ir (¬neg) U (yes ∨ (neg ∧ A g ¬Φ r−1 ))F e tke the strtegy s v tht enfores (¬neg) U (yes ∨ (neg ∧ A g ¬Φ r−1 ))F e (rst onsider the luse C r i for whih propositionl stte is hosen y s v F he strtegy de(nes uniform vlution for X r tht stis(es these lusesF por the other lusesD we hve two possiilitiesX • s v hooses q j 0 in the stte orresponding to C r i F xeither yes nor neg hve een enountered on this pth yetD so we n tke s v to demonstrte tht M r , q j 0 |= Φ r D nd hene M j , q j 0 |= Φ r F fy vemm SD lso M j , q j 0 |= Φ j F fy indutionD z j must e trueD nd hene luse C r i is stis(edF • s v hooses neg r j in the stte orresponding to C r i F henD it must e tht M r , neg r j |= A g ¬Φ r−1 D nd hene M j , q j 0 |= ¬Φ r−1 F fy vemm SD lso M j , q j 0 |= ¬Φ j F fy indutionD z j must e flseD nd hene luse C r i @ontining ¬z j A is lso stis(edF husD in order to determine the vlue of z p D it is su0ient to model hek Φ p in M p , q

icgs for heking stis(ility of ϕ ≡ (x1 ∨ ¬x 3 ) ∧ (¬x 1 ∨ x 2 ∨ x 3 )tht she hs to delre the sme vlue of x j in ll of them within uniform strtegyF e sole atl ir proposition yes holds only in the winning stte q F yviouslyD sttes orresponding to literls x 0 j n e omitted from the modelF peking more formllyD M ϕ = Agt, St, Π, π, Act, d, o, ∼ 1 , ..., ∼ k D whereX • Agt = {v, r}D • St = {q 0 } ∪ St cl ∪ St prop ∪ {q }D

p 0 F xote tht model M p onsists of O(|ϕ|p) sttes nd O(|ϕ|p) trnsitionsD where |ϕ| is the mximl length of formule ϕ 1 , ..., ϕ p F woreoverD the length of formul Φ p is liner in pD nd the onstrution of M p nd Φ p n e lso done in time O(|ϕ|p) nd O(p)D respetivelyF sn onsequeneD we otin polynomil redution of SNSAT to atl ir model hekingF Theorem 6 Model checking atl ir is ∆ P sn this pper we proved tht model heking of atl ir formule is ∆ P 2 EhrdD nd therefore ∆ P 2 E ompleteF husD we losed n existing gp @etween NPEhrdness nd ∆ P 2 EesinessA in the work of hoens IVD nd t the sme time orreted our own lim from IIF hile it is possile tht NP nd ∆ P 2 re identilD mny elieve tht ∆ P 2 is strit superset of NPF tillD NP nd ∆ P 2 re quite loseD oth elonging to the (rst level of the polynomil hierrhyF herefore our result might seem minor one ! lthoughD tehnillyD it ws not tht trivil to prove itF yn the other hndD its importne goes well eyond model heking of atl ir F sn ftD heorem T yields immedite orollries with ∆ P 2 Eompleteness of other logis like atol IPD pesile atel ISD csl IQ etFD nd ∆ P 2 Ehrdness of etsl PPF e would like to thnk xils fulling for reful reding of our proofsF References I F elurD F eF renzingerD nd yF uupfermnF elterntingEtime emporl vogiF sn Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS)D pges IHH!IHWF siii gomputer oiety ressD IWWUF P F elurD F eF renzingerD nd yF uupfermnF elterntingEtime emporl vogiF Journal of the ACMD RWXTUP!UIQD PHHPF Q tFvF flázrD tF hizD nd tF qrróF Structural Complexity IF pringerEerlgD IWVVF R iFwF glrke nd iFeF imersonF hesign nd synthesis of synhroniztion skeletons using rnhing time temporl logiF sn Proceedings of Logics of Programs WorkshopD volume IQI of Lecture Notes in Computer ScienceD pges SP!UID IWVIF S iF eF imersonF emporl nd modl logiF sn tF vn veeuwenD editorD Handbook of Theoretical Computer ScienceD volume fD pges WWS!IHUPF ilsevier iene ulishersD IWWHF T F qornkoF golition gmes nd lternting temporl logisF sn tF vn fenthemD editorD Proceedings of TARK VIIID pges PSW!PUPF worgn uufmnnD PHHIF U F qornko nd F tmrogF gompring semntis of logis for multiEgent systemsF SyntheseD IQW@PAXPRI!PVHD PHHRF V eF rerzig nd xF roqurdF unowing how to plyX niform hoies in logis of genyF sn Proceedings of AAMAS'06D PHHTF W F tmrogF ome remrks on lternting temporl epistemi logiF sn fF huninEuepliz nd F erruggeD editorsD Proceedings of Formal Approaches to Multi-Agent Systems (FAMAS 2003)D pges IQQ!IRHD PHHQF IH F tmrog nd tF hixF ho gents mke model heking explode @omputtionllyAc sn wF ëhouekD F ettD nd vFF rgD editorsD Proceedings of CEEMAS 2005D volume QTWH of Lecture Notes in Computer ScienceD pges QWV!RHUF pringer erlgD PHHSF II F tmrog nd tF hixF wodel heking strtegi ilities of gents under inomplete inforE mtionF sn wF goppoD iF vodiD nd qFwF innD editorsD Proceedings of ICTCS 2005D volume QUHI of Lecture Notes in Computer ScienceD pges PWS!QHVF pringer erlgD PHHSF IP F tmrog nd F vn der roekF egents tht know how to plyF Fundamenta InformaticaeD TQ@P!QAXIVS!PIWD PHHRF IQ F tmrog nd homs ÅgotnesF gonstrutive knowledgeX ht gents n hieve under inomplete informtionF ehnil eport sfsEHSEIHD glusthl niversity of ehnologyD PHHSF IR ojieh tmrog nd homs ÅgotnesF ht gents n hieve under inomplete informE tionF sn Proceedings of AAMAS'06D PHHTF IS qF tonkerF pesile strtegies in elterntingEtime emporl ipistemi vogiF wster thesisD niversity of trehtD PHHQF IT pF vroussinieD xF wrkeyD nd qF yreiyF ixpressiveness nd omplexity of evF ehnil eport vEHTEHQD gx 8 ix ghnD prneD PHHTF IU gFrF pdimitriouF Computational ComplexityF eddison esley X edingD IWWRF IV F F hoensF elterntingEtime logi with imperfet rellF Electronic Notes in Theoretical Computer ScienceD VS@PAD PHHRF IW F vn der roekD eF vomusioD nd wF ooldridgeF yn the omplexity of prtil ev model hekingF sn F tone nd qF eissD editorsD Proceedings of AAMAS'06D pges PHI!PHVD PHHTF PH F vn der roek nd wF ooldridgeF rtle multigent plnning for epistemi golsF sn gF gstelfrnhi nd FvF tohnsonD editorsD Proceedings of the First International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS-02)D pges IITU!IIURF egw ressD xew orkD PHHPF PI F vn der roek nd wF ooldridgeF goopertionD knowledge nd timeX elterntingEtime emporl ipistemi vogi nd its pplitionsF Studia LogicaD US@IAXIPS!ISUD PHHQF PP F vn ytterloo nd qF tonkerF yn ipistemi emporl trtegi vogiF Electronic Notes in Theoretical Computer ScienceD XQS!RSD PHHRF roeedings of vgwe9HRFThe logic to which such a syntactic restriction applies is sometimes called vanilla atl (resp. vanilla ctl etc.).Note that in the original formulation of atl [1, 2], strategies assign agents' choices to sequences of states, which suggests that agents can by denition recall the whole history of each game.The algorithm from[11] can be also used to demonstrate the upper bounds for the complexity of this problem.In fact, it is NP-hard even for models with a single agent, although the construction must be a little dierent to demonstrate this.-complete with respect to the number of transitions in the model, and the length of the formula. The problem is ∆ P 2 -complete even for turn-based models with at most two agents.