One-Pass Context-Based Tableaux Systems for CTL and ECTL

One-Pass Con ex -Based Tableaux Sys ems o CTL and ECTL Alex Abuin Ike lan Technology Resea ch Cen e, Basque Resea ch and Technology Alliance (BRTA), A asa e-Mond agón Gipuzkoa, Spain aabuin@ike lan.es Alexande Bolo o Uni e si y o Wes mins e , London, UK h ps://www.wes mins e .ac.uk/abou -us/ou -people/di ec o y/bolo o -alexande A.Bolo o @wes mins e .ac.uk Mon se a He mo Uni e si y o he Basque Coun y, San Sebas ián, Spain mon se a .he [email protected] Paqui Lucio Uni e si y o he Basque Coun y, San Sebas ián, Spain h p://www.sc.ehu.es/paqui [email protected] Abs ac When building ableau o empo al logic o mulae, applying a wo-pass cons uc ion, we i s check he alidi y o he gi en ableaux inpu by c ea ing a ableau g aph, and hen, in he second “pass”, we check i all he e en uali ies a e sa is ied. In one-pass ableaux checking he alidi y o he inpu does no equi e hese auxilia y cons uc ions. This pape con inues he de elopmen o one-pass ableau me hod o empo al logics in oducing ee-s yle one-pass ableau sys ems o Compu a ion T ee Logic (CTL) and shows how his can be ex ended o cap u e Ex ended CTL (ECTL). A dis inc i e ea u e he e is he u ilisa ion, o he co e ableau cons uc ion, o he concep o a con ex o an e en uali y which o ces i s ea lies ul ilmen . Rele an algo i hms o ob aining a sys ema ic ableau o hese b anching- ime logics a e also de ined. We p o e he soundness and comple eness o he me hod. Wi h hese de elopmen s o a ee-shaped one-pass ableau o CTL and ECTL, we ha e o malisms which a e well sui ed o he au oma ion and a e amenable o he implemen a ion, and o he o mula ion o dual sequen calculi. This b ings us one s ep close o he applica ion o one-pass con ex -based ableaux in ce i ied model checking o a a ie y o CTL- ype b anching- ime logics. 2012 ACM Subjec Classi ica ion Theo y o compu a ion →Modal and empo al logics Keywo ds and ph ases Tempo al logic, ai ness, exp essi eness, b anching- ime Digi al Objec Iden i ie 10.4230/LIPIcs.TIME.2020.14 Funding Alexande Bolo o : This au ho has been suppo ed by he Eu opean Union (FEDER unds) unde g an TIN2017-86727-C2-2-R, and by he Uni e si y o he Basque Coun y unde P ojec LoRea GIU18-182. Mon se a He mo: This au ho has been suppo ed by he Eu opean Union (FEDER unds) unde g an TIN2017-86727-C2-2-R, and by he Uni e si y o he Basque Coun y unde P ojec LoRea GIU18-182. Paqui Lucio: This au ho has been suppo ed by he Eu opean Union (FEDER unds) unde g an TIN2017-86727-C2-2-R, and by he Uni e si y o he Basque Coun y unde P ojec LoRea GIU18-182. ©Alex Abuin, Alexande Bolo o , Mon se a He mo, and Paqui Lucio; licensed unde C ea i e Commons License CC-BY 27 h In e na ional Symposium on Tempo al Rep esen a ion and Reasoning (TIME 2020). Edi o s: Emilio Muñoz-Velasco, Ana Ozaki, and Ma in Theobald; A icle No. 14; pp. 14:1–14:20 Leibniz In e na ional P oceedings in In o ma ics Schloss Dags uhl – Leibniz-Zen um ü In o ma ik, Dags uhl Publishing, Ge many 14:2 One-Pass Con ex -Based Tableaux Sys ems o CTL and ECTL 1 In oduc ion In his pape we con inue ou in es iga ion o ableaux-based deduc i e echniques o empo al logic ha ing in mind hei po en ial applica ion in model checking, mo e speci ically, in ce i ied model checking [ 16 ], which aims o gene a e p oo s as ce i ica es o he p ope ies ha a e e i ied, as well as coun e examples o hose p ope ies ha a e in alida ed. The e a e wo known ways o build ableau cons uc ions o empo al logic o mulae ( o he su ey o ableau me hod o empo al logic we e e an in e es ed eade o [ 13 ]). Two- pass cons uc ions check he alidi y o he gi en ableaux inpu in wo passes - in he i s pass a ableau g aph is ob ained and he second “pass” checks he sa is iabili y o all e en uali ies. In one-pass ableaux checking he alidi y o he inpu does no equi e hese auxilia y cons uc ions. This pape con inues he de elopmen o one-pass ableau me hod o empo al logics [ 11 , 4 ], his ime o Compu a ion T ee Logic ( CTL ) and Ex ended Compu a ion T ee Logic ( ECTL ) in oduced, espec i ely, in [ 6 ] and [ 10 ]. The co e ableau cons uc ion is based on he concep o a con ex o an e en uali y, which is a se o o mulae ha “accompanies” he e en uali y in he label o he node o a ableaux g aph. Ou speci ic ableau ules ha in ol e con ex o ce he ea lies ul ilmen o e en uali ies. In p e ious wo ks such a con ex -based one-pass ableaux app oach has been de eloped o p oposi ional linea - ime empo al logic, PLTL [ 11 ], and o he b anching- ime logic ECTL# [ 4 ], which in oduces a new class o ai ness cons ain s u ilising he “un il” empo al ope a o . I has also been shown how, in he linea - ime case, he me hod, being mingled wi h a SAT sol e , can be in oked as pa o he ce i ied model checking o PLTL [ 2 ]. Aiming a simila de elopmen s o b anching- ime cases, in pa icula o CTL, we make wo obse a ions. Fi s ly, he sa is iabili y o a p ope y ϕ in PLTL can be educed o checking i a comple e ansi ion sys em sa is ies ¬ϕ (since any coun e -model o ¬ϕ is a model o ϕ ) and bo h he sa is iabili y and model checking a e PSPACE-comple e [ 18 ]. Howe e , he CTL sa is iabili y p oblem canno be educed o he CTL model checking. In pa icula , a model checking algo i hm o CTL p ope ies ( o example [ 5 ] implemen ed in NuSMV) canno be adap ed o es ing CTL sa is iabili y: he model checking p oblem o CTL is known o be P-comple e [ 7 ], while he sa is iabili y p oblem o CTL is EXPTIME-comple e [ 9 ]. Howe e , any decision p ocedu e o CTL sa is iabili y can be used o pe o m model checking asks. Secondly, no e ha in ou p e ious wo k one-pass ableaux me hod was de eloped o a iche logic - ECTL# [ 4 ]. Howe e , he applica ion o such model checking p ocedu e o CTL simply based on he exis ing one-pass ableaux o ECTL# would become oo “non-in ui i e” due o he complexi y o i s ules ha a e needed o his iche logic. We also no e ha he dis inguished (and una oidable) ea u e o one-pass echnique o ECTL# is he u ilisa ion o wo ypes o con ex , unlike in he case o PLTL . He e he so-called “ou e ” (simila o PLTL ) con ex is a collec ion o s a e o mulae, and is complemen ed by so called “inne ” con ex , a collec ion o pa h o mulae. Subsequen ly, he de elopmen o a simple one-pass me hod o CTL is an impo an ask. In ou ableau me hod o CTL , simila ly o PLTL , we only need he “ou e ” con ex , ye , simila o ECTL# he gene a ed ableaux a e AND-OR ees. Ou esul s p o ide an in ui i e ableau me hod ha se es as a decision p ocedu e o CTL sa is iabili y and can also be used in ce i ied model checking o CTL p ope ies hence he me hod p esen ed in he pape would enable a subsequen s udy and implemen a ion o a ce i ied model checke . Wi h he de elopmen o ee-shaped one-pass ableaux o CTL and ECTL, his pape has p o ed he e ec i eness o he app oach which now co e s bo h linea - ime and a ange o b anching- ime logics. Mo eo e , he esul s o his pape gi e us o malisms which a e well sui ed o he au oma ion and a e amenable o he A. Abuin, A. Bolo o , M. He mo, and P. Lucio 14:3 implemen a ion, and o he o mula ion o a dual sequen calculi - all hese b ing us one s ep close o he applica ion o hese de elopmen s in ce i ied model checking o a a ie y o b anching- ime logics. Addi ionally, aiming a he ex ension o he ce i ied model checking o he b anching- ime amewo k, a p oo sys em, e.g. sequen calculus, is equi ed o check he p oo ce i ica es in he b anching- ime se ing. Ou ex ensi e sea ch o ableau me hods o CTL has no shown a g ea a ie y o sys ems. Fo example, [ 3 ] p esen s a wo-pass ableau, whe e in he i s pass he ableau ules a e applied c ea ing a cyclic g aph. In he second pass, “bad loops” a e p uned (whe e a “bad loop” is a loop con aining some e en uali y ha is no ul illed along i ). In [ 1 , 12 ] he au ho s in oduce a single-pass ableaux decision p ocedu e o CTL . I is based on Schwendimann’s one-pass p ocedu e o PLTL [ 17 ]. This ableau me hod uses an addi ional mechanism o collec ing in o ma ion on he se o o mulae in he nodes, and passing i , o subsequen nodes along b anches. The in o ma ion on p e iously gene a ed nodes helps de ec ing “bad loops” wi hou cons uc ing he whole g aph. Finally, we no e ha we ha e no ound an explici o mula ion o a ableaux (one o wo pass) me hod o ECTL. To ensu e ha he p esen a ion o qui e echnical de ails in he pape is clea and sel - con ained, we supply all majo echnical de ails in he ex . This de e mines he ollowing s uc u e o he pape . In §2 we gi e CTL and ECTL syn ax and seman ics as sublogics o CTL? . The o mula ion o he ableau me hod is p esen ed in §3, whe e we i s gi e some p elimina ies and hen o e iew he ableau cons uc ion as an AND-OR ee and p o ide examples. A sys ema ic ableau cons uc ion is in oduced in §4. In §5 we show u he ex ension o he me hod o ECTL . In §6 we d aw he conclusions and p ospec s o u u e wo k ha he p esen ed esul s open. Finally, in Appendix A we b ie ly ecall he cyclic models cha ac e iza ion o sa is iabili y in b anching empo al logics. The soundness and comple eness o ou ableau me hods a e p o ed in Appendix B. Finally, in Appendix C we depic he comple e ableau o he unning example in he pape . 2 Syn ax and Seman ics o CTL and ECTL The language o b anching- ime logic ex ends he language o classical p oposi ional logic by u u e ime empo al ope a o s ◦ - “a he nex momen o ime”, ♦ - “e en ually”,  - “always” and U - “un il”, oge he wi h pa hs quan i ie s A - “ o all pa hs” quan i ie , and E - “ he e exis s a pa h” quan i ie . The hie a chy o CTL - ype amily o B anching- ime logics (BTL) is de ined by eleasing es ic ions on he conca ena ions o empo al ope a o s and pa hs quan i ie s which de ine classes o admissible s a e o mulae dis inguished o hese logics. As in CTL e e y empo al ope a o mus be p eceded by a pa h quan i ie , his logic canno exp ess ai ness which equi es a leas he conca ena ion o  and ♦ . These a e ackled by ECTL [ 9 ] which enables simple ai ness cons ain s bu no hei Boolean combina ions. ECTL+ [ 10 ] u he ex ends he exp essi eness o ECTL allowing Boolean combina ions o empo al ope a o s and ECTL ai ness cons ain s (bu no pe mi ing hei nes ing). The logic ECTL# [ 4 ] ex ends ECTL+ by allowing he combina ions  ( AUB )o AUB , e e ed o as modali ies U and U . The logic CTL? , o en conside ed as he “ ull b anching- ime logic” o e comes all hese es ic ions on syn ax allowing any a bi a y combina ions o empo al ope a o s and pa h quan i ie s. Fo he sake o gene ali y, as all logics we a e in e es ed in a e subsumed by CTL? , we i s ecall CTL? syn ax and hen, by es ic ing i , de i e he syn ax o each o ECTL# , ECTL+ , ECTL and CTL. TIME 2020 14:4 One-Pass Con ex -Based Tableaux Sys ems o CTL and ECTL IDe ini ion 1 (Syn ax o CTL? ) . Gi en P op is a ixed se o p oposi ions, and p∈P op , we de ine se s o s a e ( σ ) and pa h ( π ) CTL? o mulae o e P op as ollows: σ ::= T|p| σ1∧σ2| ¬σ|Eπand πCTL?::= σ|π1∧π2| ¬π|◦π|πUπ. Obse e ha in De ini ion 1 o he se o pa h o mulae we delibe a ely used an index CTL? and did no use any index o he se o s a e o mulae: he syn ax o CTL? sublogics we will de ine la e , will be dis inguished exac ly by speci ic o hese logics pa h o mulae cons uc ions, while he se o s a e o mulae is p ese ed om he de ini ion o CTL? syn ax. O he usual Boolean ope a o s can be de i ed om hose in oduced in he s anda d way while he “ elease” ( R ), ♦ and  ope a o s can be de ined as ollows: ϕ1Rϕ2≡ ¬ ( ¬ϕ1U¬ϕ2 ), ♦ϕ≡TUϕ, and ϕ≡ ¬♦¬ϕ. We conside a K ipe-s yle seman ics o CTL? : a K ipke s uc u e, K , is a iple ( S, R, L ) whe e S6 = ∅ is a se o s a es, R⊆S×S is a o al bina y ela ion, called he ansi ion ela ion, and L : S→ 2 P op is a labelling unc ion. Ou K ipke s uc u es a e labelled di ec ed g aphs ha co espond o Eme son’s R-gene able s uc u es, i.e. he ansi ion ela ion R is su ix, usion and limi closed [ 8 ]. A pa h x h ough a K ipke s uc u e K is an in ini e sequence o s a es si, si+1, si+2 . . . such ha ( sj, sj+1 ) ∈R o any j≥i . A ullpa h x h ough a K ipke s uc u e K is an in ini e sequence o s a es s0, s1, s2. . . , whe e s0 is he oo . Gi en a pa h x = si, si+1, . . . and a s a e sk∈x such ha k > i , we deno e i s ini e p e ix x≤k = si, si+1 ...,sk and i s in ini e su ix x≥k = sk, sk+1, . . . . The no a ion Kx ( i ) deno es a K ipke s uc u e wi h he se o s a es o K es ic ed o hose ha a e R - eachable om x ( i )and ullpa hs ( K )is he se o all ullpa hs in K . Gi en he s uc u e K = ( S, R, L ), he ela ion | =e alua es pa h o mulae in a gi en pa h x and s a e o mulae a he s a e index i o x and is de ined on a oms by K, x, i | = pi p∈L ( x ( i )). Omi ing s anda d de ini ions o Booleans, we p esen he ela ion |= o empo al connec i es and pa h quan i ie E: K, x, i |=Eπi he e exis s a pa h y∈ ullpa hs(Kx(i)) such ha K, y |=π. K, x, i |=◦πi K, x, i + 1 |=π. K, x, i |=π1Uπ2i he e exis s k≥iwi h K, x≥k|=π2and K, x≥j|=π1 o all 0≤j≤k−1. Fo any se Σo s a e o mulae, K, x, i | = Σ i K, x, i | = σ, o all σ∈ Σ. Mo eo e , i o any ullpa h x∈ ullpa hs ( K ), we ha e K, x, 0 | = Σ, hen we simply w i e K | = Σ. Fo a s a e o mula ϕ , he se o i s models, Mod ( ϕ ), is o med by all iples ( K, x, i )such ha K, x, i | = ϕ . Then ϕ is sa is iable ( Sa ( ϕ )) i Mod ( ϕ ) 6 = ∅ , o he wise ϕ is unsa is iable ( UnSa ( ϕ )). Fo s a e o mulae ϕ and ϕ0 , i Mod ( ϕ ) = Mod ( ϕ0 ) hen ϕ and ϕ0 a e logically equi alen deno ed as ϕ≡ϕ0 . Sa is iabili y and logical equi alence a e gene alised o se s o s a e o mulae Σ, in he na u al way ( o mally by subs i u ing ϕ wi h Σin he ele an de ini ions and s a ing ha Σis sa is ied when all i s o mulae a e sa is ied). Fo each o BTL logics ECTL# , ECTL+ , ECTL and CTL i s syn ax is de ined o e a ixed se o p oposi ions P op , such ha he de ini ion o s a e o mulae is he same as o CTL? (De . 1), and he e en uali y ♦ϕ is he abb e ia ion o TUϕ . The speci ic o hese logics es ic ions on he CTL? g amma in De ini ion 1 gene a e he co esponding se s o pa h o mulae, as in De ini ion 2. Fo echnical con enience, he e we de ine  as he basic language ope a o . IDe ini ion 2 (Pa hs o mulae o ECTL#,ECTL+, ECTL and CTL). πECTL#::= σ|π1∧π2| ¬π|◦σ|σU(σ∧ ♦σ)|(σ∨σ)|σU(σ)|(σUσ) πECTL+::= σ|π1∧π2| ¬π|◦σ|σUσ|σ|♦σ| ♦σ. πECTL ::= σ| ¬π|◦σ|σUσ|σ|♦σ| ♦σ. πCTL ::= σ| ¬π|◦σ|σUσ|σ. A. Abuin, A. Bolo o , M. He mo, and P. Lucio 14:5 IDe ini ion 3 (Li e als) . Le P op be a ixed se o CTL ( ECTL ) p oposi ions, and le ρ∈P op . Then he se o CTL(ECTL) li e als is de ined as Li ::= F|T|ρ| ¬ρ. I is well known ha any gi en b anching- ime o mula ϕ can be con e ed o a o mula NNF ( ϕ )- he Nega ion No mal Fo m o ϕ ob ained by pushing nega ions inwa ds un il hey only apply o li e als. The con e sion is based on well-known equi alences which ensu e ha ϕ and NNF ( ϕ )ha e exac ly he same models, i.e. a e logically equi alen . Consequen ly, we assume ha inpu s o he ableaux p ocedu e in CTL and ECTL a e gi en in NNF . Fo simplici y, we will w i e ∼ϕ ins ead o NNF ( ¬ϕ ). Also, o a ini e se Φ = {ϕ1, . . . , ϕn} , we le ∼Φ = NNF(¬Vn i=1 ϕi). Fu he , i is impo an o no e ha he nes ing o “pu e pa h o mulae”, o ally un- es ic ed in CTL? , is now es ic ed in i s sublogics by ele an g amma cases o pa hs o mulae. Fo example, a CTL? o mula (1) is no an ECTL# o mula. Rew i ing i as A(TU(◦p∧E◦¬p)) we can see A♦(◦p∧E◦¬p)(1) ha ◦p∧E◦¬p is nei he a s a e o mula no o he o m σ . No e ha he alidi y o (1) which is indica i e o CTL? , is di ec ly linked o he limi closu e p ope y [ 8 ]. Simila ly, a ECTL# o mula A (( pUq ) ∧ ( sU¬q )) is no an ECTL+ o mula because pUq and sU¬q , hence hei conjunc ion, a e no admissible ECTL+ o mulae. Fu he , an ECTL+ o mula (2) does no belong o ECTL E(♦q∧♦¬q)(2) as ♦q∧ ♦¬q is no an admissible ECTL pa h o mula. Finally, he ai ness cons ain (3) exp essible in ECTL canno be cons uc ed in CTL syn ax as e e y empo al ope a o E♦q(3) in a CTL o mula mus be p eceded by a pa h quan i ie . No e ha i is impo an o dis inguish he p oblem i a o mula o a supe logic belongs o a sublogic and he p oblem i a o mula o a supe logic can be exp essed in a sublogic. Fo example, E ( ♦q∨ ♦¬q ), simila ly o o mula (2) does no belong o ECTL bu unlike (2), i is exp essible in his logic, as E(♦q∨ ♦¬q)≡E♦q∨E♦¬qwhich is an ECTL o mula i we de ine ∨ ia ∧. Table 1 Classi ica ion o con ex -based ableaux sys ems o CTL- ype logics and ele an di icul cases o conca ena ions o empo al ope a o s and pa h quan i ie s. BTL Logics E♦qE(♦q∧♦¬q)A((pUq) ∨ ( sU¬ )) A♦(◦p∧E◦¬p) One-pass Tableaux B(U,◦)(CTL)X X X X This pape B(U,◦,♦)(ECTL)√X X X This pape B+(U,◦,♦)(ECTL+)√ √ X X √ B+(U,◦,U)(ECTL#)√ √ √ X√ B?(U,◦)(CTL?)√ √ √ √ X Table 1 ep esen s BTL logics classi ied by hei exp essi eness using “ B ” o “B anching”, ollowed by he se o only allowed modali ies as pa ame e s; B+ indica es admissible Boolean combina ions o he modali ies and B? e lec s “no es ic ions” in ei he conca ena ions TIME 2020 14:6 One-Pass Con ex -Based Tableaux Sys ems o CTL and ECTL o he modali ies o Boolean combina ions be ween hem ollowing he no a ion ini ially p oposed in [ 8 ] and u he uned in [ 15 ]. The op ow o he igu e ep esen s he indica i e o mulae (1)-(3) o he lis ed logics. The las column in Table 1 e lec s he de elopmen o he con ex -based one-pass ableaux echnique o CTL- ype logics: he me hod has been de eloped o ECTL# ([ 4 ] whe e he mo i a ion was o ackle complex cases o ai ness). In his pape we in oduce he echnique o CTL and ECTL , while he case o ECTL+ can be ackled e ec i ely by he echnique de eloped o ECTL# . Indeed, ECTL+ and ECTL# ha e simila cases o he Boolean combina ion o e en uali ies in he scope o A and E , namely disjunc ions o he e en uali ies in he scope o he A quan i ie and conjunc ions o e en uali ies in he scope o he E quan i ie , see [ 4 ] o de ails. Thus, Table 1 also e lec s syn ac ical cases o conca ena ions o empo al ope a o s and pa h quan i ie s ha a e di icul o con ex -based one-pass ableaux. To ackle hese cases, in addi ion o α - and β - ules, ha a e s anda d o he ableaux, no el β+ - ules which use he con ex o o ce he e en uali ies o be ul illed as soon as possible, we e in oduced. As ECTL# is mo e exp essi e han ECTL+ in allowing new ype o ai ness cons ain s ha use he U ope a o , he ele an ules in oduced in [ 4 ] would co e all di icul conca ena ions o ope a o s in ECTL+ . Hence, simply ea ing he case o one-pass con ex -based ableaux o ECTL+ as sol ed by he ele an de elopmen o a iche logic ECTL# , in his pape we concen a e on b idging he gap in ou oadmap in supplying BTL logics by his echnique, by de eloping he me hod o CTL and ECTL . The ul ima e a ge o his oadmap - he one-pass con ex -based ableaux o CTL? emains ex emely di icul and an open p oblem. 3 Con ex -based One-pass Tableau Me hod o CTL We p ecede he p esen a ion o he me hod by he in oduc ion o a numbe o impo an concep s. Fi s ly, we in oduce a concep o basic modali y which e lec s he es ic ions on o ming he basic admissible combina ions o empo al ope a o s in he scope o a pa h quan i ie . Recall ha o mulae o CTL and ECTL logics a e w i en in NNF . Abb e ia ing by Q ei he o he pa h quan i ie s A o E , we conside a basic modali y o CTL o ECTL logic o be o he o m QT , whe e T is a empo al ope a o . The s uc u e QT is gene a ed by he g amma ules o hese logics in De . 2. We can iden i y all basic modali ies in a gi en o mula ϕ by inding i s mos embedded modali y(es), say M1 , hen looking a he nex basic modali y in which M1 is embedded, e c. Fo example, basic modali ies o CTL a e s uc u es Q◦,QU , and Q while o ECTL hese will be Q◦,QU , Q , Q♦ and Q♦ . I we analyse a CTL o mula E◦A◦p hen he mos embedded basic modali y, M1 , would be A◦p, which is embedded as E◦M1. These a e gene alised in De ini ion 4. IDe ini ion 4 (ECTL#,ECTL+, ECTL and CTL Basic Modali ies). MECTL ::= c|Q◦M|Q(MUM)|QM|Q♦M|Q♦M. MCTL ::= c|Q◦M|Q(MUM)|QM. whe e c s ands o a pu ely classical o mula (we can conside a pu ely classical o mula as a ze o-deg ee basic modali y) and Ms ands o any basic modali y o CTL in he de ini ion o MCTL and o ECTL in he de ini ion o MECTL . No e ha we ha e “de i ed” cases o basic modali ies o ♦M and MRM . In wha ollows, e e y CTL modali y QU o Q♦ is called e en uali y. CTL ableau ules a e based on ixpoin cha ac e isa ion o i s basic modali ies: (in he equa ions below ν and µ s and o “minimal ixpoin ” and “maximal ixpoin ” ope a o s, espec i ely) A. Abuin, A. Bolo o , M. He mo, and P. Lucio 14:7 Eϕ=νρ(ϕ∧E◦ρ)E(ϕRψ) = νρ(ψ∧(ϕ∨E◦ρ)) Aϕ=νρ(ϕ∧A◦ρ)A(ϕRψ) = νρ(ψ∧(ϕ∨A◦ρ)) (4) E♦ϕ=µρ(ϕ∨E◦ρ)E(ϕUψ) = µρ(ψ∨(ϕ∧E◦ρ)) A♦ϕ=µρ(ϕ∨A◦ρ)A(ϕUψ) = µρ(ψ∨(ϕ∧A◦ρ)) (5) This ixpoin cha ac e isa ion o basic CTL and ECTL modali ies as maximal o minimal ixpoin s gi e ise o hei analy ical classi ica ion as α - o β - o mulae which a e associa ed, in he ableau wi h α - and β - ules: Q , and QR as maximal ixpoin s a e classi ied as α - o mulae while Q♦ and QU as minimal ixpoin s a e β - o mulae. This is also e lec ed in he known equi alences: Eϕ=ϕ∧E◦EϕE(ϕRψ) = ψ∧(ϕ∨E◦E(ϕRψ)) Aϕ=ϕ∧A◦AϕA(ϕRψ) = ψ∧(ϕ∨A◦A(ϕRψ)) (6) E♦ϕ=ϕ∨E◦E♦ϕE(ϕUψ) = ψ∨(ϕ∧E◦E(ϕUψ)) A♦ϕ=ϕ∨A◦A♦ϕA(ϕUψ) = ψ∨(ϕ∧A◦A(ϕUψ)) (7) The ableau me hod de e mines i a gi en se o CTL s a e o mulae is sa is iable o no . We p ecede he o mal in oduc ion o he echnique by i s in o mal o e iew. The ini ial node o he ableaux is labelled by a CTL o mula in NNF . To expand he oo , and any subsequen node, we apply one o he ollowing ules: α - and β - ules, he “nex -s a e” ule, which e lec s a “jump” om a “s a e” o a “p e-s a e”, and, inally, cha ac e is ic o ou app oach, β+ - ules, whe e he use o he con ex (o an e en uali y) is essen ial. The use o he con ex in hese ules, which is a collec ion o s a e o mulae accompanying he e en uali y in he label o he node, o ces he soones ul illmen o e en uali ies. We apply α -, β -, and β+ - ules epea edly un il we each a node labelled by F o by an inconsis en se o o mulae, o a node whose labels ha e al eady occu ed wi hin he pa h unde conside a ion. In he o me case he expansion o he gi en b anch e mina es wi h ⊥ as i s lea . In he la e case, a epe i i e node in he b anch means ha he b anch has a loop – whe e some sub o mulae o he gi en o mula a e sa is ied o e e – which could be “bad” o “good”. A loop is “bad” when i has a node which con ains an un ul illed e en uali y, i.e. none o he nodes o he loop sa is ies i . In ou p ocedu e, he applica ion o β+ - ules o e en uali ies is essen ial o dis inguish be ween “good” and “bad” loops - i β+ - ules ha e al eady been applied o e e y e en uali y occu ing in he b anch hen we ha e a ’good loop’ and his b anch ep esen s a model o he gi en o mula. O he wise, we choose an e en uali y o which a co esponding β+ - ule has no been applied. IDe ini ion 5 (Syn ac ically Consis en Se o Fo mulae) . A se Σo s a e o mulae σ is syn ac ically consis en abb e ia ed as Σ > i F6∈ Σand {σ, ∼σ} 6⊆ Σ o any σ ; o he wise, Σ is inconsis en deno ed as Σ⊥. IDe ini ion 6 (Tableau, Consis en Node, Closed b anch) . A ableau o a se o CTL s a e o mulae Σis a labelled ee hT, τ, Σ i , whe e T is a ee, and τ is a mapping o he nodes o T o he s a e o mulae, elemen s o Σ, such ha he ollowing wo condi ions hold: (i) The oo is labelled by he se Σ. (ii) Fo any o he node m∈T , i s label τ ( m )is a se o s a e o mulae ob ained as he esul o he applica ion o one o he ules in Figu es 1, 2 and 4 o i s pa en node n . Gi en he applied ule is R , we e m m an R -successo o n . A node n o TIME 2020 14:8 One-Pass Con ex -Based Tableaux Sys ems o CTL and ECTL a ee T is consis en , abb e ia ed as n> , i i s label, τ ( n ), is a syn ac ically consis en se o o mulae (see De . 5), else n is inconsis en , abb e ia ed as n⊥ . I a b anch b o τ , con ains n⊥∈b, hen bis closed else bis open. (∧)Σ, σ1∧σ2 Σ, σ1, σ2 (Q)Σ,Qσ Σ, σ, Q◦Qσ (∨)Σ, σ1∨σ2 Σ, σ1|Σ, σ2 (QU)Σ,Q(σ1Uσ2) Σ, σ2|Σ, σ1,Q◦Q(σ1Uσ2) (QR)Σ,Q(σ1Rσ2) Σ, σ1, σ2|Σ, σ2,Q◦Q(σ1Rσ2)(Q♦)Σ,Q♦σ Σ, σ |Σ,Q◦Q♦σ Figu e 1 α- and β-Rules. The ules in Figu e 1 ollow he s anda d o he ableaux classi ica ion o ules in o α - ules and β - ules ha o he o mulae wi h CTL modali ies a e based on hei analy ic classi ica ion e lec ed in Equa ions (6)-(7). Thus, i a node, n , in he ableau g aph is labelled by a se o o mulae, Σ , ϕ , and a designa ed o mula o he applica ion o ableau ules, ϕ , is an α - o mula - Q o QR , hen a co esponding α - ule applies, while i ϕ is a β - o mula - Q♦ o QU hen a co esponding β - ule applies. In he la e case we ea Σ as a (possibly emp y) con ex o he e en uali y ϕ . These applica ions o α - and β - ules gene a e a se o o mulae in he conclusion as a label o he successo node, n + 1, in case o an α- ule, o as labels o wo successo s o n, in case o a β- ule. When a node n is labelled by an elemen a y se o o mulae – i.e. a se which exclusi ely o med by li e als and o mulae o he o m Q◦σ – hen his s uc u e is analogous o he cons uc ion o a “s a e” in he e minology o [ 19 ]; i enables us o cons uc he successo s o n co esponding o “p e-s a es” [ 19 ]. Acco ding o he nex p oposi ion we a e gua an eed o each such a ee s uc u e, whe e he las node o e e y b anch, a his s age o he cons uc ion, is a s a e. IP oposi ion 7. Any se o CTL s a e o mulae has a ableau T such ha he las node o e e y b anch is labelled by an elemen a y se o s a e o mulae. P oo . Repea edly apply o e e y expandable node any applicable α - o β - ule un il all expandable nodes a e elemen a y. Then, he nex -s a e ule mus be applied o e e y expandable node. J (Q◦)Σ,A◦σ1,...,A◦σ`,E◦σ0 1,...,E◦σ0 k, σ1, . . . , σ`, σ0 1&. . . &σ1, . . . , σ`, σ0 k whe e Σis a se o li e als. Figu e 2 Nex -s a e Rule. (“&” joins AND-successo s in he conclusion.) P oposi ion 7 enables he applica ion o he so-called “nex -s a e ule” depic ed in Figu e 2. Applying his ule we spli he cu en b anch a node n whe e he se Σ ,A◦σ1,...,A◦σ`,E◦σ0 1, . . . , E◦σ0 k is sa is ied, in o k b anches (i.e. in o he numbe o b anches equal o he numbe o E◦ cons ain s) whe e he successo s o n along hese b anches a e AND-successo s, and a e labelled each by a di e en se σ1, . . . , σ`, σ0 i , o i∈ { 1 , . . . , k} . This ule spli s b anches in a “conjunc i e” way, and we use he symbol & o ep esen he gene a ion o AND-successo s o A. Abuin, A. Bolo o , M. He mo, and P. Lucio 14:9 node n . Thus, he g aphs gene a ed by he ableaux wi h he applica ion o he “nex -s a e” ule a e AND-OR ees. The subsequen cons uc ion o a ableau, addi ionally, in ol es ules ha a e applied o so called “uni o m se s o o mulae”. IDe ini ion 8 (Uni o m Se o Fo mulae) . A se o CTL s a e o mulae Σis uni o m i Σis exclusi ely o med by li e als and basic CTL modali ies and i has a mos one E- o mula. Applying P oposi ion 7 o cons uc a ableau wi h all i s expandable nodes labelled by elemen a y se s o o mulae, and hen applying he ule ( Q◦ )( o e e y expandable node), and inally, epea edly applying ( o e e y expandable node) he ules ( ∧ )and ( ∨ ), we can p o e P oposi ion 9 which s a es ha we can also each he s age whe e he las nodes o ableaux b anches a e labelled by uni o m se s o o mulae. IP oposi ion 9. Any se o CTL s a e o mulae Σhas a ableau T such ha labels o all i s expandable nodes a e uni o m se s o o mulae. IDe ini ion 10 (Uni o m Tableau) . Fo any se Σo CTL s a e o mulae, he ableau o Σ p o ided by P oposi ion 9 is deno ed Uni o m_Tableau(Σ). Now we illus a e he p ocedu e by a unning example and in he subsequen ex will g adually explain i s main s eps wi h illus a i e igu es o some pa s. The whole ableau is depic ed in Appendix C. A◦A(FR ¬q),E◦E(pUq)∧E◦¬q A◦A(FR ¬q),E◦E(pUq),E◦¬q A(FR ¬q),E(pUq)A(FR ¬q),¬q (∧) (Q◦) Figu e 3 Example o uni o m ableau. IExample 11. The gi en se o o mulae {A◦A ( FR ¬q ) ,E◦E ( pUq ) ∧E◦¬q} is no uni o m. Hence, by applying he ules ( ∧ )and ( ◦ ), we ob ain he ableau in Figu e 3. The wo AND- successo s c ea ed by he “nex -s a e” ule ( Q◦ )a e espec i ely labelled by he uni o m se s: A(FR ¬q),E(pUq)and A(FR ¬q),¬q. We ex end ou se o ableau ules wi h he new wo ules named as β+ - ules (Figu e 4). No e ha he ( Q♦ ) + ule can be de i ed om he applica ion o he ( QU ) + o he CTL o mula TUσ . These ules, simila ly o β - ules, also spli a b anch in o wo b anches. These wo β+ - ules a e he only ules in ou sys em ha make use o he con ex - hei applica ion o ce he e en uali ies o be sa is ied as soon as possible ( om he poin o he ableau cons uc ion whe e an e en uali y is selec ed o be expanded wi h a β+ - ule). The con ex is gi en by he se s Σ ha con ain s a e o mulae. In he conclusion o a β+ - ule we add o he conclusion o he co esponding β - ule, a conjunc ∼ Σ 0 . Recall ha his is an NNF o he nega ion o he conjunc ion o all o mulae in Σ 0 ha a e le om Σa e pe o ming he se - heo e ical di e ence cons ain indica ed in he o mula ion o he ule. The idea now is ha ∼ Σ 0 should also be sa is ied un il σ2 becomes sa is ied. This p e en s he epe i ion o he con ex while σ2 is “delayed”. No e ha Σ 0 does no include he A (wi h any p e ix o TIME 2020 14:16 One-Pass Con ex -Based Tableaux Sys ems o CTL and ECTL B Soundness and Comple eness Since CTL and ECTL a e sublogics o ECTL# and he ableau me hod p esen ed he e is he adap a ion o he me hod in [ 4 ], in his sec ion we essen ially adap o CTL he soundness and comple eness p oo s de eloped in [ 4 ]. We i s ly p o e he soundness and comple eness o he ableau me hod o CTL, and hen we ex end bo h esul s o ECTL. To p o e he soundness o ou ableau me hod o CTL (Theo em 22), we show ha e e y ableau ule in Figu es 1, 2 and 4 a e sound (o p ese e sa is iabili y) in he sense o he nex Lemma 21. ILemma 21 (Soundness o he Tableau Rules o CTL ) . Conside all he ules in Figu es 1, and 2 and 4. 1. Fo any α- ule Σ Σ0:Sa (Σ) i and only i Sa (Σ0). 2. Fo any β- and β+- ule Σ Σ1|Σ2:Sa (Σ) i and only i Sa (Σ1)o Sa (Σ2). 3. I Σis a se o consis en li e als, hen Sa (Σ ,A◦σ1,...,A◦σ`,E◦σ0 1,...,E◦σ0 k )i and only i Sa (σ1, . . . , σ`, σ0 i) o all 1≤i≤k. P oo . All he i ems ollows e y easily by he “sys ema ic” applica ion o he seman ic de ini ions o he modali ies, excep he “i ” di ec ion o he wo o β+ - ules. We will p o e he e he “i ” di ec ion o he ules ( QU ) + o Q = E and Q = A , because he ules ( Q♦ ) + a e pa icula cases by abb e ia ion ♦σ=TUσ. Fo he “i ” di ec ion o ule ( EU ) + , le K | = Σ ,E ( σ1Uσ2 )and le x be he pa h in K such ha K, x, i | = Σ ,E ( σ1Uσ2 ). Then, le j be he leas i≥ 0such ha K, x, i | = σ2 . I j = i = 0, hen K, x, 0 | = Σ , σ2 . O he wise, i j > 0 hen K, x, m | = σ1 , o all 0 ≤m<j . Conside k o be he g ea es such m o which K, x, k | = Σ. Hence, K, x, h | = ∼ Σ, o all h such ha k + 1 ≤h < j . In pa icula , by de ini ion o Σ 0 (ob ained om Σ) i is easy o see ha K, x, h | = σ o e e y σ∈ (Σ Σ 0 )and o all h such ha 0 ≤h < j . The e o e, K, x, h | = ∼ Σ 0 , o all hsuch ha k+ 1 ≤h < j. Thus, K, x, k |=, σ1,E◦E((σ1∧ ∼Σ0)Uσ2). Fo he “i ” di ec ion o ule (AU)+, le us suppose ha UnSa (Σ, σ2)and UnSa (Σ, σ1,A◦A((σ1∧ ∼Σ0)Uσ2)). We will show ha UnSa (Σ ,A ( σ1Uσ2 )). Fo ha , le us conside any a bi a y K such ha K | = Σ o show ha K 6| = A ( σ1Uσ2 ). By he abo e unsa is iabili y hypo hesis, i K | = Σ, hen bo h K 6| = σ2 and K 6| = σ1∧A◦A (( σ1∧ ∼ Σ 0 ) Uσ2 ). Then, he e a e wo possible cases. Fi s , i K | = ¬σ1∧ ¬σ2 , hen i is ob ious ha K 6| = A ( σ1Uσ2 ). Second, i K | = ¬σ2∧¬A◦A (( σ1∧ ∼ Σ 0 ) Uσ2 ), hen he e exis s x1∈ ullpa hs ( K )and i1> 0 ha sa is y bo h K, x1, j | = ¬σ2 o all j such ha 0 ≤j≤i1 , and K, x1, i1| = ¬σ1∨ Σ 0 . Since all he o mulae in Σ Σ 0 a e sa is ied in all s a es along all pa hs, indeed K, x1, i1| = ¬σ1∨ Σ. The e o e, i K, x1, i1| = ¬σ1 , hen ob iously K 6| = A ( σ1Uσ2 ). O he wise, i K, x1, i1| = Σ, applying he same easoning o Kx1 ( i1 )as we did abo e o K , we can conclude ha he e should be a pa h x2∈ ullpa hs ( Kx1 ( i1 )) and some i2> 0such ha ei he Kx1 ( i1 ) , x2, j | = ¬σ2 o all j such ha i1≤j≤i2 and Kx1 ( i1 ) , x2, i2| = ¬σ1∨ Σ. Hence, i Kx1 ( i1 ) , x2, i1| = ¬σ1 , hen i ially K 6| = A ( σ1Uσ2 ). O he wise, Kx1 ( i1 ) , x2, i1| = Σ. Hence, he e a e wo possible scena ios: 1.) A e a ini e numbe o i e a ions we ge a pa h y = x≤i1 1x≤i2 2· · · x≤ik k such ha K, y, j | = ¬σ2 o all j such ha 0 ≤j≤ik and K, y, ik| = ¬σ1 . 2.) The in ini e i e a ion o he second case yields a pa h y = x≤i1 1x≤i2 2· · · x≤ik k· · · ( ha exis s by he limi closu e p ope y) such ha K, y, i | = ¬σ2 o all i≥ 0. In bo h scena ios we ha e K 6| = A ( σ1Uσ2 ) holds o any a bi a y K ha sa is ies Σ. Thus, UnSa (Σ,A(σ1Uσ2)).J A. Abuin, A. Bolo o , M. He mo, and P. Lucio 14:17 ITheo em 22 (Soundness o he Tableau Me hod o CTL ) . Gi en any se o s a e o mulae Σ, i he e exis s a closed ableau o Σ hen UnSa (Σ). P oo . In a closed ableau o Σ, he se o o mulae labelling a leas one lea in each bunch is inconsis en and he e o e unsa is iable. Then, by Lemma 21, he labelling o he oo node, Σ, is unsa is iable. J Nex , we p o e he e u a ional comple eness o he ableau me hod o CTL (Theo em 29). Fo ha , we i sly de ine he no ion o s age and p o e some auxilia y p ope ies on he s ages and bunches o he sys ema ic ableau, ha a e necessa y o p o e ha e e y open bunch in he sys ema ic ableau ep esen s a model o he ini ial se o o mulae (Lemma 28). IDe ini ion 23 (S age) . Gi en a b anch, b o a ableau T , a s age in T is e e y maximal subsequence o successi e nodes ni, ni+1, . . . , nj in b such ha τ ( nk )is no a ( Q◦ )-child o τ ( nk−1 ), o all k such ha i<k≤j . We deno e by s ages ( b ) he sequence o all s ages o b . The successo ela ion on s ages ( b )is induced by he successo ela ion on b . The labelling unc ion τ is ex ended o s ages as he union o he o iginal τ applied o e e y node in a s age. IDe ini ion 24 ( αβ+ -sa u a ed S age) . We say ha a s age s = ni, . . . , nj in Asys Σ is αβ+-sa u a ed i and only i i sa is ies he ollowing condi ions: 1. Fo all σ1∧σ2∈τ(s):{σ1, σ2} ⊆ τ(s). 2. Fo all Qσ∈τ(s):{σ, Q◦Qσ} ⊆ τ(s). 3. Fo all σ1∨σ2∈τ(s):σ1∈τ(s)o σ2∈τ(s). 4. Fo all Q(σ1Rσ2)∈τ(s):{σ1, σ2} ⊆ τ(s)o {σ2,Q◦Q(σ1Rσ2)} ⊆ τ(s). 5. Fo all Q(σ1Uσ2)∈τ(s):σ2∈τ(s)o {σ1,Q◦Q(σ1Uσ2)} ⊆ τ(s)o {σ1,Q◦Q((σ1∧ ∼Σ0)Uσ2)} ⊆ τ(s) whe e Σ0= (τ(ni) {Q(σ1Uσ2)}) {(A◦)iAϕ|i≥0and (A◦)iAϕ∈τ(ni)}. 6. Fo all Q(♦σ)∈τ(s):σ∈τ(s)o {Q◦Q(♦σ)} ⊆ τ(s)o {Q◦Q((∼Σ0)Uσ)} ⊆ τ(s) whe e Σ0= (τ(ni) {Q♦σ}) {(A◦)iAϕ|i≥0and (A◦)iAϕ∈τ(ni)}. IDe ini ion 25 (Expanded Bunch and Tableau) . An open b anch b is expanded i each s age s∈s ages ( b )is αβ+ -sa u a ed and b is e en uali y-co e ed. A bunch is expanded i all i s open b anches a e expanded. A ableau is expanded i all i s open bunches a e expanded. The cons uc ion o he sys ema ic ableau applies exac ly one β+ - ule o exac ly one selec ed e en uali y (i any) a he i s node o he s age, and hen applies exhaus i ely all he applicable α - and β - ules o he o mulas in he s age, un il he b anch closes, o i s lea is labelled by an elemen a y se , o i con ains a loop-node. Consequen ly, he ollowing P oposi ion 26 holds which can be i ially p o ed by cons uc ion. IP oposi ion 26. Gi en any se o s a e o mulae Σ, he sys ema ic ableau Asys Σ is expanded. Nex we p o e a c ucial p ope y o he sys ema ic ableau managemen o e en uali ies by means o he selec ion policy. IP oposi ion 27. Le b be an open b anch o Asys Σ and le Q ( σ1Uσ2 )be a o mula ha is selec ed a some s age si∈s ages ( b ). Then, he e exis s some s age sk∈s ages ( b )( o some k≥i) such ha σ2∈τ(sk)and σ1∈τ(sj) o all j∈ {i, . . . , k −1}. P oo . By cons uc ion, he uni o m se labelling he i s node a each s age sj ( j≥i ) o b has he o m Σ sj,Q (( σ1∧ ( ∼ Σ si∧· · · ∧ ∼ Σ sj−1 )) Uσ2 )whe e each Σ sj is he con ex o he selec ed o mula con aining he nex -s ep a ian o Q ( σ1Uσ2 )a he i s node o each s age sj . Since TIME 2020 14:18 One-Pass Con ex -Based Tableaux Sys ems o CTL and ECTL no o he β+ - ule is applied each Σ sj is a subse o he ini e se o med by all s a e o mulae ha a e sub o mulae o some o mula in Σ si and hei nega ions. Hence, he e a e a ini e numbe o di e en Σ sj . The e o e, a e ini ely many applica ions o he β+ - ule, Σ sh = Σ sj , o some h > = i , o some j∈ {i, . . . , h − 1 } , and σ1∧ ( ∼ Σ si∧ · · · ∧ ∼ Σ sh−1 ) ∈τ ( sh ). In pa icula , ∼ Σ sh∈τ ( sh ), hence, Σ sh mus be inconsis en . Since b is open, his is a con adic ion. This means ha , o some k≥i he applica ion o he co esponding β+ - ule should o ce ha σ2∈τ ( sk ). In addi ion, by P oposi ion 26 and De ini ion 24(5), σ1∈τ ( sj ) o all j∈ {i, . . . , k −1}.J ILemma 28 (Model Exis ence) . Le Σbe any se o o mulae. Fo any expanded bunch H o Asys Σ, he e exis s a K ipke s uc u e KHsuch ha KH|= Σ. P oo . Le H be any expanded bunch o Asys Σ . We de ine KH = ( S, R, L )such ha S = Sb∈Hs ages ( b )and o any s∈S : L ( s ) = {p|p∈τ ( n ) ∩P op o some node n∈s} ; and R is he ela ion induced in s ages ( b ) o each b∈H . Any b anch in b∈H is open, hence b ends in a loop-node. Mo eo e , e e y e en uali y has been selec ed in some s age o b . Hence, he e exis s a (possibly emp y) uni o m se Σ ` such ha o some i≥ 0: b = s0, s1, . . . , si−1, si, si+1, . . . , sj, n` , whe e each sh s ands o a s age and n` is a non- expandable loop-node labelled by Σ ` whose companion node is he i s node a s age si . We a e going o p o e he ollowing ac : KH, sa,0|=σ o any a∈ {0, . . . , j}and any o mula σin L(sa) by s uc u al induc ion on he o mula σ. The base o he induc ion, o σ=p∈P op, ollows by de ini ion o KH. The cases whe e σ has one o he o ms σ1∧σ2 , Qσ , σ1∨σ2 and Q ( σ1Rσ2 )a e i ial by De ini ion 24 and he induc ion hypo hesis. Hence, o comple e he induc i e p oo we will show ha KH, sa, 0 | = Q ( σ1Uσ2 ) o any Q ( σ1Uσ2 ) ∈L ( sa ). The case o all Q♦σ∈L ( sa ) ollows as a pa icula case by ♦σ≡TUσ. Conside any Q ( σ1Uσ2 ) ∈L ( sa ). Since b is e en uali y-co e ed and n` is a loop-node, Q ( σ1Uσ2 )mus be he selec ed e en uali y a some node be ween he s a es sa and sj . Hence, by P oposi ion 27 and he de ini ion o KH , he e should be a s a e sk∈S ( o some a≤k≤j ) such ha σ2∈L ( sk )and σ1∈L ( sz ) o all z∈ {a, . . . , k − 1 } . Then, by induc ion hypo hesis, KH, sk, 0 | = σ2 and KH, sz, 0 | = σ1 o all z∈ {a, . . . , k − 1 } . The e o e, KH, sa,0|=Q(σ1Uσ2). To comple e he p oo , we show ha he successo ela ion be ween s a es in KH is well- de ined. Fo ha , conside any ableau node in any s age sa ha is labelled by an elemen a y se {Σ,A◦σ1,...,A◦σn,E◦σ0 1,...,E◦σ0 k} whe e Σis a consis en se o li e als, by ule ( Q◦ ), sa has (in KH ) a successo s a e si a+1 , o each i∈ { 1 , . . . , k} , such ha L ( si a+1 ) = {σ1, . . . , σn, σ0 i} . We can assume (by he abo e p o ed ac ) ha KH, si a+1, 0 | = {σ1, . . . , σn, σ0 i} o all i∈ { 1 , . . . , k} . The e o e, we can in e ha KH, sa,0|={Σ,A◦σ1,...,A◦σn,E◦σ0 1,...,E◦σ0 k}.J Nex , we p o e he e u a ional comple eness o he ableau me hod. ITheo em 29 (Re u a ional Comple eness o CTL ) . Fo any se o s a e o mulae Σ, i UnSa (Σ) hen he e exis s a closed ableau o Σ. A. Abuin, A. Bolo o , M. He mo, and P. Lucio 14:19 P oo . Suppose he con a y, ha he e exis s no closed ableau o Σ. Then he sys ema ic ableau Asys Σ is open. Hence, he e is a leas one expanded bunch H in Asys Σ . By Lemma 28, he e exis s a K ipke s uc u e KHsuch ha KH|= Σ. Consequen ly, Sa (Σ).J Finally, we p o e he comple eness o ou ableau me hod o CTL. ITheo em 30 (Te mina ion o he Tableau Me hod o CTL ) . Fo any se o s a e o mulae Σ, he cons uc ion o he expanded ableau Asys Σ e mina es. P oo . Tableau ules p oduce a ini e b anching, hence König’s Lemma, applies. The e o e, i su ices o p o e ha e e y b anch is ini e. By P oposi ion 27, he applica ion o a β+ - ule o a selec ed o mula s ops a e a ini e numbe o s eps. Since he numbe o selec able e en uali ies in any open b anch is ini e, any open b anch is e en uali y-co e ed a e a ini e numbe o e en uali y selec ions. Recall ha we assume he e en uali y selec ion s a egy o be ai . J ITheo em 31 (Comple eness o he Tableau Me hod o CTL ) . Fo any se o s a e o mulae Σ, i Σis sa is iable hen he e exis s a ( ini e) open expanded ableau o Σ. P oo . The exis ence o he sys ema ic ableau Asys Σ su ices o p o e his ac , by Theo em 30. J Now, we explain how he p oo s o hese me a heo ems o CTL can be ex ended o ECTL . Fi s ly, we ex end he soundness o he ableau ules, in he sense o Lemma 21, o he ules in Figu e 7. ILemma 32. Fo any ECTL se o s a e o mulae Σand any s a e o mula σ: 1. Sa (Σ,Q♦σ)i and only i Sa (Σ,Q♦σ, Q◦Q♦σ). 2. Sa (Σ,Q♦σ)i and only i Sa (Σ,Qσ)o Sa (Σ,Q♦σ, Q◦Q♦σ). P oo . I ollows by “sys ema ic” applica ion o he seman ic de ini ions o he modali ies Q♦and Q♦gi en by he equi alences (8) in Sec ion 5. J To ex end he e u a ional comple eness esul o ECTL , we i s ly ex end he De ini ion 24 wi h he ollowing addi ional condi ions o a s age o be αβ+-sa u a ed: 7. Fo all Q♦σ∈τ(s):{Q♦σ, Q◦Q♦σ} ⊆ τ(s). 8. Fo all Q♦σ∈τ(s):{Qσ} ⊆ τ(s)o {Q♦σ, Q◦Q♦σ} ⊆ τ(s). I is ob ious ha hese wo addi ional condi ions a e sa is ied in any s age o he sys ema ic ableau by cons uc ion. Using hese condi ions, i is ou ine o p o e ha KH de ined in Lemma 28 sa is ies he ac ha : KH, sa, 0 | = σ o any a∈ { 0 , . . . , j} and any o mula o he o ms Q♦σ, Q♦σ ha belongs o L ( sa ). The e o e, e u a ional comple eness (i.e. Theo em 29) ex ends o ECTL. Finally, o ex end he e mina ion esul (see p oo o Theo em 30), i su ices o ensu e ha he ules in Figu e 7 do no a ec he beha iou o he β+ - ules on he selec ed e en uali ies in he sense ha P oposi ion 27 is p ese ed. Since each applica ion o a ule in Figu e 7 in oduces a new Q♦σ , in Sec ion 5 we ha e in oduced he simpli ica ion ule ( <QU )(see (9) o subsume any occu ence o he e en uali y ϕ by any nex -s ep a ian o ϕ. The e o e, P oposi ion 27 holds and hence Theo em 30 i ially ex ends o ECTL. TIME 2020 14:20 One-Pass Con ex -Based Tableaux Sys ems o CTL and ECTL C The Running Example Tableau In Figu e 9 we depic he whole ableau o he unning example we use in he pape . No e ha he Q ule a s ep 2, deno ed wi h a big ci cle gene a es wo AND-successo s, whe e he le successo has he closed ableau - his is explained in he pape . Hence, he bunch is closed, in spi e o he open ableau a he igh successo o he AND-node. A◦A(FR¬q),E◦E(pUq)∧E◦¬q A◦A(FR¬q),E◦E(pUq),E◦¬q E(pUq),A(FR¬q) q, A(FR¬q) q, F,¬q q, ¬q, A◦A(FR¬q) p, E◦E((p∧E(TUq))Uq),A(FR¬q) p, E◦E((p∧E(TUq))Uq),F,¬q p, E◦E((p∧E(TUq))Uq),¬q, A◦A(FR¬q) E((p∧E(TUq))Uq),A(FR¬q) q, A(FR¬q) q, F,¬q q, ¬q, A◦A(FR¬q) p∧E(TUq),E◦E((p∧E(TUq))Uq),A(FR¬q) p, E(TUq),E◦E((p∧E(TUq))Uq),A(FR¬q) A(FR¬q),¬q F,¬q¬q, A◦A(FR¬q) A(FR¬q) (∧) (Q◦) (EU)+ (AR) ⊗⊗ (AR) ⊗ (◦) (EU)+ (AR) ⊗⊗ (∧) ⊗ (AR) ⊗(Q◦) Figu e 9 A closed ableau o {A◦A(FR¬q),E◦E(pUq)∧E◦¬q}.