Towards Certified Model Checking for PLTL Using One-Pass Tableaux

Towa ds Ce i ied Model Checking o PLTL Using One-Pass Tableaux Alex Abuin Ike lan Technology Resea ch Cen e, P. J. M. A izmendia ie a, 2 20500 A asa e-Mond agón Gipuzkoa, Spain aabuin@ike lan.es Alexande Bolo o Uni e si y o Wes mins e , W1W 6UW, 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 Unai Díaz de Ce io Ike lan Technology Resea ch Cen e, P. J. M. A izmendia ie a, 2 20500 A asa e-Mond agón Gipuzkoa, Spain udiazce io@ike lan.es Mon se a He mo Uni e si y o he Basque Coun y, P. Manuel de La dizabal, 1, 20018-San Sebas ián, Spain mon se a .he [email protected] Paqui Lucio Uni e si y o he Basque Coun y, P. Manuel de La dizabal, 1, 20018-San Sebas ián, Spain h p://www.sc.ehu.es/paqui [email protected] Abs ac The s anda d model checking se up analyses whe he he gi en sys em speci ica ion sa is ies a dedica ed empo al p ope y o he sys em, p o iding a posi i e answe he e o a coun e -example. A he same ime, i is o en use ul o ha e an explici p oo ha ce i ies he sa is iabili y. This is exac ly wha he ce i ied model checking (CMC) has been in oduced o . The pape a gues ha one-pass (con ex -based) ableau o PLTL can be e icien ly used in he CMC se ing, emphasising he ollowing wo ad an ages o his echnique. Fi s , he use o he con ex in which he e en uali ies occu , o ces hem o ul il as soon as possible. Second, a dual o he ableau sequen calculus can be used o o malise he ce i ica es. The combina ion o he one-pass ableau and he dual sequen calculus enables us o p o ide no only coun e -examples o unsa is ied p ope ies, bu also p oo s o sa is ied p ope ies ha can be checked in a p oo assis an . In addi ion, he cons uc ion o he ableau is en iched by an embedded sol e , o which we dedica e hose (p oposi ional) compu a ional asks ha a e cos ly o he ableaux ules applied solely. The combina ion o he abo e echniques is pa icula ly help ul o eason abou la ge (sys em) speci ica ions. 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, linea - ime, Ce i ied model checking Digi al Objec Iden i ie 10.4230/LIPIcs.TIME.2019.12 Funding Alexande Bolo o : This au ho has been pa ially suppo ed by he UK Knowledge T ans e Pa ne ship KTP011063 Lumina Lea ning & Uni e si y o Wes mins e , and he Spanish P ojec 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 pa ially suppo ed by Spanish P ojec 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 pa ially suppo ed by Spanish P ojec 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 , Unai Díaz de Ce io, Mon se a He mo, and Paqui Lucio; licensed unde C ea i e Commons License CC-BY 26 h In e na ional Symposium on Tempo al Rep esen a ion and Reasoning (TIME 2019). Edi o s: Johann Gampe , Sophie Pinchina , and Guido Scia icco; A icle No. 12; pp. 12:1–12:18 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 12:2 Towa ds Ce i ied Model Checking o PLTL Using One-Pass Tableaux 1 In oduc ion and P oblem Se up Model Checking [ 10 , 31 , 11 ] is an algo i hmic me hod o de e mining whe he a complex ha dwa e o so wa e sys em sa is ies a gi en p ope y. Many impo an p ope ies o be e i ied e lec he sys em’s dynamics and a e exp essed in some empo al logic. I he p ope y does no hold, he checke e u ns a coun e -example: a ace/model o he sys em ha does no sa is y he p ope y. This coun e -model ac s as a “ce i ica e” o he ailu e and i s ole is o help he use o iden i y he sou ce o he p oblem which could be in he sys em design, in he p ope y, and e en in he model checke . Howe e , he e a e a numbe o scena ios whe e ano he ce i ica ion is needed. One o hese scena ios consis s on p o ing, only once, he co ec ion o he unde lying algo i hm o he model checke . Fo his ask, in e ac i e p oo assis an s such as Coq o Isabelle a e good ools. They allow us o ce i y a model checke and e en ob ain an execu able p og am by he e inemen o some ex ac ion mechanism. Fo ins ance Amjad [1] desc ibed how o code BDD-based symbolic model checking algo i hms in o an au oma ic heo em p o e . Mo e ecen ly, Espa za e al. [ 13 ] ha e e i ied an au oma a-based model checke wi h Isabelle heo em p o e . The second scena io in ol es he model checke o ce i y ha a pa icula p ope y is ue. Fo example, he use may deal wi h a e y complex speci ica ion and is no su e i he speci ica ion is well w i en. He e i is impo an o ha e echniques ha p o ide no only a coun e -example, bu also ce i y ha he sys em mee s he p ope y. This is exac ly wha he ce i ied model checking (CMC) has been in oduced o . In his second scena io a numbe o echniques ha e been p e iously p oposed. Some o he echuiques ha deal wi h ini e-s a e sys ems can be ound in [ 23 , 29 ]. In [ 23 ] an au oma a- heo e ic app oach o model checking is add essed. In [ 29 ] a deduc i e p oo sys em was in oduced o e i ying b anching ime p ope ies exp essed in he mu-calculus. Fo in ini e-s a e sys ems, Mebsou e al. [ 28 ] ecen ly p esen ed a new echnique o gene a ing and e i ying p oo ce i ied in SMT-based model checke s, ocusing on p oo s o in a ian p ope ies. The use o in a ian s has been exploi ed in [ 17 , 22 ], whe e he p oo is gene a ed om he induc i e in a ian ob ained wi h he k -li eness algo i hm [ 9 ]. The esul ing app oach can be implemen ed as a model checke based on he combina ion o k -li eness wi h an engine o in a ian p ope ies ha is capable o p oducing induc i e in a ian s. A d awback o his app oach is ha , al hough i is e y compe i i e, he ask o inding coun e -examples and he ask o gene a ing p oo s (in his case ia inding in a ian s), a e e y di e en equi ing o he la e he addi ion o ex a mechanisms o he own model checke . In his pape , we p opose an CMC based on dual sys ems o ableaux and sequen calculus, o iginally in oduced in [ 14 , 15 ]. I p oduces ce i ica e p oo s, o mal p oo s in he sequen calculus, and coun e examples - open b anches in he ableau. This is also one o he main ad an ages o ou app oach: he same easoning mechanism applies o bo h asks - ce i ica es and coun e examples. The CMC (see Figu e 1) di e s om he adi ional model checking in p o iding a p oo o he sa is iabili y o he gi en p ope y, and no only a coun e -example. Inco po a ing he no a ion o [ 21 ] (and sligh ly modi ying i ) we ep esen he me hodology o he ce i ied model checking as he ollowing signa u e: CMC :: Sys em ×ϕ−→ B×(P oo |Coun e -example) whe e, gi en a speci ica ion o a sys em, S , and a p ope y, ϕ , a ce i ied model checking p oduces a Boolean esul , B, indica ing whe he Ssa is ies ϕ, along wi h a p oo (o ce i ica ion), in he posi i e case, o a coun e -example, in he nega i e case. A. Abuin, A. Bolo o , U. Díaz de Ce io, M. He mo, and P. Lucio 12:3 Sys em Speci ica ion P ope y o e i y Coun e -example Fo mal P oo No Yes CMC Does he sys em sa is y he p ope y? Figu e 1 Gene al schema o CMC. Howe e , we belie e ha o ake he ull ad an age o CMC, and enabling i s indus ial applica ion o eal sys ems, we need o ensu e ha CMC mee s he ollowing equi emen s. (i) P oo s should be gene a ed au oma ically. (ii) An CMC needs o o e a CMC use su icien in o ma ion o unde s and he p oo wi hou addi ional “cos s” ela ed o specialis knowledge o he unde lying p oo echnique. (iii) The p esen a ion o he p oo should enable he CMC use s o easily na iga e h ough i s ace. This becomes pa icula ly impo an when he sys em is badly de ined – he e he na iga ion h ough he ace can help o de ec e o s. (i ) Finally, when de eloping a sa e y c i ical sys em ollowing a sa e y p ocess (e.g. p ocesses o s anda d ISO26262 [ 19 ], IEC61508 [ 18 ] o EN50128 [ 7 ]), i is manda o y o analyse how a bug in a ool (a model checke in ou case) may a ec he sa e y o he de eloped sys em. Depending on he le el o hese e ec s, some ac ions a e equi ed o inc ease ou con idence in he model checke . One o he mechanisms o inc ease he p obabili y o inding a ailu e is o e-e alua e he ou pu s o he CMC by an independen ool de eloped by an independen eam. We p opose a pa icula CMC me hod o ealising he CMC philosophy (see Figu e 2) mee ing he cha ac e is ics (i)-(i ) abo e while main aining he common ( o he adi ional Model Checke ) unc ionali y. Ou me hod is cen e ed on a con ex -based empo al one-pass ableaux echnique whose pe o mance is op imised by a SAT sol e . Va ious ableaux echniques ha e been p oposed o a ich a ie y o empo al logics, linea and b anching: P oposi ional Linea -Time Tempo al Logic (PLTL); Compu a ion T ee Logic (CTL); CTL ∗ which gene alizes PLTL and CTL, e c. (an excellen su ey can be ound in [ 16 ]). One o he co e ideas o he ableaux me hods is o iden i y e en uali ies wi hin he gi en empo al inpu and o check ha hey a e ul illed. T adi ional ableaux echniques equi e wo phases o pe o m his es . In he i s phase, a g aph which gi es all possible p e-models o he ableau inpu , in cons uc ed. In he second phase, o each s a e, s in his g aph, ha con ains some “e en ually ϕ ”, a g aph- heo e ic algo i hm looks o a s a e, eachable om s , ha sa is ies ϕ . No e also ha he wo-pass ableaux me hods ail o main ain he classical co espondence be ween ableaux and sequen s ha associa es a sequen p oo wi h he closed ableau. TIME 2019 12:4 Towa ds Ce i ied Model Checking o PLTL Using One-Pass Tableaux Sys em Speci ica ion P ope y o e i y Coun e -example Fo mal P oo No Yes CMC Fo maliza ion o ules in Isabelle/HOL Fo mal p oo Re- e i ica ion SAT-Sol e Tableaux me hod Figu e 2 Gene al schema o he p oposal. To a oid he second phase and, hence, o keep he abili y o gene a ing (sequen ) p oo s om ableaux, in [ 14 , 15 ], dual sys ems o ableaux and sequen s, o PLTL, we e p esen ed. E e y logic de ined in [ 14 , 15 ] was p o ed o be sound and comple e. In pa icula , [ 15 ] con ains a p oo ha he ableau sys em we use in he p esen pape , is a decision me hod o he ull PLTL, i.e. i is sound, e u a ionally comple e, and e mina ing. The e mina ion p ope y is achie ed on he basis o any ai selec ion s a egy. A e y simila sequen calculus is p esen ed in [ 6 ] (see [ 15 ] o mo e de ails abou he simila i ies and di e ences o hese sys ems). The one-pass ableau me hod [ 15 ] has been ex ended o a concu en cons ain logic in [12], and also o ECTL]- a b anching- ime sublogic o CTL∗in [5]. The ableau me hod in [ 15 ] makes use o he so-called con ex o an e en uali y o o ce i s ul illmen . The con ex o an e en uali y is simply he se o o mulae ha “accompanies” he e en uali y in he label o he node. When a one-pass ableau checks whe he a p ope y ϕholds o no , i is always able o issue a ce i ica e: ei he a coun e -model o a comple e explana ion ( o mal p oo ) o why ϕis ue. We abb e ia e he one-pass ableau me hod as τ↑ pl l and i s dual sequen calculus as TTC. Conside ing one-pass ableau me hod as one o he co e componen s o he CMC solu ion we p esen in his pape , we a gue ha i con o ms wi h he p ope ies (i)-(i ) men ioned abo e. Indeed, he me hod au oma ically checks whe he he speci ica ion o he sys em sa is ies he p ope y (i). 1 I i does no hen i p o ides a coun e -example. A coun e - example is gi en by a ace which is in ui i ely clea (ii). In he case o a posi i e answe , a ele an p oo ce i ies i . Again, he ou pu p oo is ep esen ed as a ace enabling an easy na iga ion h ough i (iii). Mo eo e , one o he a ac i e ea u es o ou me hod is ha i o ces he e en uali ies o be ul illed as soon as possible, hus, he me hod will po en ially gene a e sho e pa hs (wi h ewe nodes) han hose p oduced by non-con ex based ableaux. In ou p oposal, he pe o mance o he one-pass ableau echnique is complemen ed, o e iciency, by he SAT sol ing. No e ha he idea o encoding o ansi ion sys ems in o p oposi ional SAT was i s p oposed in [ 20 ] o AI planning p oblems, whe e he au ho s show ha SAT algo i hms scale much be e on he SAT-encodings han planing algo i hms 1 Fo he pu poses o he pape , we le he speci ica ion, S , be in a dedica ed o m S = Ini ∧T R , whe e Ini is a PLTL o mula ha ep esen s he ini ial s a es and T R is he ep esen a ion o all he ansi ions allowed, see §3 o de ails. A. Abuin, A. Bolo o , U. Díaz de Ce io, M. He mo, and P. Lucio 12:5 on he o iginal g aph o mula ion. Following his success, SAT sol e s ha e been also used in Bounded Model Checking (BMC). In bo h amewo ks, a p oposi ional o mula is used o encode he inpu p oblem. Planning p oblems deal wi h ini e pa hs along a ini e g aph, hence he encoding is comple e w. . . he o iginal p oblem. In model checking, pa hs wi hin he ansi ion sys ems a e, in gene al, in ini e. SAT-based BMC u ilises he encoding o he model-checking p oblems in sa is iabili y checking, mo e p ecisely, he p oposi ional encoding o s a emen s exp essing ha he e exis s a leng h- k pa h (along he ansi ion sys em) ha does no sa is y a gi en p ope y. The BMC inc eases k un il ei he he SAT’s answe is “yes” (i.e. a coun e -example is ound), o he sea ch becomes in ac able, o k eaches a ce ain bound. The o iginal SAT-based BMC algo i hm [ 3 ], al hough comple e o ini e s a e, is limi ed in p ac ice o alsi ica ion. Many addi ional s a egies ha e been in oduced o make BCM comple e, see [ 4 ] o a good su ey. The e is also a la ge amoun o wo k, s a ing wi h [ 32 ], on using SAT sol ing o imp o ing he sa is iabili y es o he ull PLTL. Recen pape s [ 24 , 25 ] use SAT sol e s o seek o a model o an inpu o mula. This model is essen ially a g aph/au oma on p oduced by he i s pass o a wo-pass ableau me hod, which should be ollowed o es ing he ul ilmen o e en uali ies. SAT sol e s a e called o he gene a ion o all (di e en ) successo s o e e y s a e in he g aph. The au ho s use well-known empo al equi alences (like pUq≡ ( q∨ ( p∧◦ ( pUq ))) o compu e he successo s o he gi en s a e. He e, he me hod u ilises he enaming o sub o mulae con aining empo al modali ies (such as pUq ) by esh p oposi ional a iables and u ilise he SAT sol ing o calcula e di e en successo s a es o each s a e in he ansi ion sys em. This p e en s he epea ed gene a ion o “p oposi ionally equi alen ” s a es. The ele an heu is ics o p uning he sea ch-space and on- he- ly mechanism o es ing e en uali y ul ilmen a e in oduced in he implemen a ion. Ou p oposal uses SAT sol e s in a simila way, bu is e y di e en in he p ima y goals. In ou me hod, SAT sol e s a e employed o calcula e a se o he “nex ” s a es in he ableau: being in he “cu en s a e”, SAT sol e calcula es hose successo s a es in he ansi ion sys ems ha sa is y he nega ion o he es ed p ope y. Fo ha , we do no ename all empo al modali ies in he label o he ableau node, bu only hose o he o m ◦ϕ , whe e ϕ only con ains classical ope a o s. Mo eo e , ou p oposal o using he one-pass ableau echnique (helped, o e iciency, by he SAT sol e ) is comple e o deciding (unbounded) model checking p oblems and wo ks on in ini e aces. The mos ema kable di e ence o ou p oposal ( ega ding [ 24 , 25 ]) is ela ed o he ac ha we pu sue CMC, i.e. we would like o gene a e p oo s in a calculus o PLTL, hence we use he one-pass con ex -based ableau along wi h i s dual sequen calculus. In addi ion, he con ex -based ableau is pa icula ly well sui ed o dealing wi h he speci ica ions o ansi ion sys ems (“always”- o mulae); he con ex plays he ole “o o cing e en uali ies o be ul illed as soon as possible” and ac s as a seman ic cons ain ha p e en s he gene a ion o se e al s a es (which a e gene a ed in he wo-pass app oach). In building he p oo , we in oke Isabelle/HOL [ 30 ] o e i y he cons uc ion o he ableaux in o de o a oid possible e o s caused by he implemen a ion (i ). This ex e nal alida ion is ca ied ou by a sequen calculus TTC which is o malized in Isabelle/HOL and is dual o he one-pass ableau me hod. We also no e ha he same easoning mechanism based on he one-pass ableau is applied in ou app oach o coun e -examples and p oo s which makes he ool easy o unde s and. This acili a es he indus ial sp eading o CMC. The emaining o he pape is o ganised as ollows. In §2 we e iew he echnique o cons uc a one-pass ableau τ↑ pl l . In §3 we p esen one-pass ableau based model checking. This ollows by he desc ip ion o he ce i ica ion u ilising Isabelle in §4. Finally, in §5 we summa ise he esul s and p o ide an accoun o u u e wo k. TIME 2019 12:6 Towa ds Ce i ied Model Checking o PLTL Using One-Pass Tableaux 2 One-pass Con ex -based Tableau To make he pape sel -con ained and easie o ead, in his sec ion we i s ecall he syn ax and seman ics o he unde lying logic, PLTL and hen we will e iew he one-pass ableau me hod. 2.1 Syn ax and Seman ics o PLTL IDe ini ion 1 (PLTL Language).The language o PLTL comp ises A se , P op, o p oposi ional symbols. P oposi ional connec i es ¬,∧,∨, and cons an s Tand F Fu u e- ime empo al connec i es, “  ” (always), “ ♦ ” (e en ually) “ ◦ ” (a he nex momen in ime), “U” (un il), and “R” ( elease). IDe ini ion 2 (WFF PLTL ) . The se o well- o med o mulae o PLTL, deno ed by WFF PLTL , is induc i ely de ined as he smalles se sa is ying he ollowing. Any elemen o P op,Tand Fa e in WFFPLTL. I Aand Ba e in WFFPLTL hen so a e ¬A, A ∧B, A ∨B, A, ♦A, AUB, and ARB. A li e al is ei he a p oposi ional symbol (a posi i e li e al) o he nega ion o a p oposi ional symbol (a nega i e li e al). De ini ion 1 in oduces PLTL wi h he se o empo al ope a o s ha a e con enien o ou ep esen a ion in he pape . We no e ha his se is iche han {U,◦} which is known o be su icien o ep esen all o he linea - ime empo al ope a o s. Fo example, ‘ ♦ϕ ’ can be de ined as TUϕ while ϕRψ can be de ined ia U as ¬ ( ¬ϕU¬ψ )(he e and in he emaining o he pape ϕand ψa e me a-symbols deno ing PLTL o mulae). Fo mulae o he ype ♦ϕ and ϕUψ a e called e en uali ies, and o mulae o he ype ϕ a e called always- o mulae. A model, M = s0, s1, s2, s3, . . . , o PLTL o mulae is a disc e e, linea sequence o s a es, isomo phic o na u al numbe s, N . Each s a e, si, 0 ≤i , is a se o posi i e li e als, which a e sa is ied a he i - h momen o ime. We w i e hM, ii | = ϕ o indica e ha ϕ is ue in he model Ma he (s a e) index i∈N. Below we induc i ely de ine he ela ion | =which e alua es PLTL o mulae in a model M a i - h momen o ime. No e ha he e we ollow so called “ancho ed” e sion o PLTL ha de ines he PLTL alidi y and sa is iabili y (see below) a he “beginning” o ime, he ini ial s a e, s0o a model. hM, ii |=T hM, ii 6|=F hM, ii |=¬ϕi hM, ii 6|=ϕ hM, ii |=ϕ∧ψi hM, ii |=ϕand hM, ii |=ψ hM, ii |=ϕ∨ψi hM, ii |=ϕo hM, ii |=ψ hM, ii |=◦ϕi hM, i + 1i |=ϕ hM, ii |=ϕi hM, ji |=ϕ o e e y j≥i. hM, ii |=♦ϕi he e exis s j≥isuch ha hM, ji |=ϕ. hM, ii | = ϕUψ i he e exis s j≥i such ha hM, ji | = ψ and o e e y k, i ≤k < j , we ha e hM, ki |=ϕ. hM, ii | = ϕRψ i o e e y j≥i , ei he hM, ji | = ψ o he e exis s k such ha i≤k < j and hM, ki |=ϕ. A. Abuin, A. Bolo o , U. Díaz de Ce io, M. He mo, and P. Lucio 12:7 IDe ini ion 3 (PLTL sa is iabili y, alidi y) . I , o a o mula ϕ , he e exis s a model, M , such ha ( M, 0) | = ϕ hen ϕ is sa is iable. Fo mula ϕ is called alid i i is sa is iable in all models. In he emaining o he pape we will use capi al le e s Φ , Ψ , ∆ , . . . o deno e se s o PLTL o mulae. The seman ics abo e can be ex ended o se s o o mulae in he s anda d way: gi en a se o PLTL o mulae Φ = γ1, γ2,...γn , he ollowing holds: hM, ii | = Φ i hM, ii |=γk, o all k, 1≤k≤n. 2.2 Use ul PLTL p ope ies In his sec ion we ecall hose PLTL syn ac ic and seman ic p ope ies ha a e use ul o ou ableau cons uc ion. Fi s , he ableau p ocedu e will ake as an inpu PLTL o mulae con e ed o hei nega ed no mal o ms (NNF). IDe ini ion 4 (P ocedu e o ob aining NNF) . Fo a gi en PLTL o mula, ϕ , push he nega ions in ϕ inwa d un il hey a e applied only o p oposi ions. This in ol es applying he s anda d se o ew i e ules used o ob ain NNF in classical logic (including ¬T−→ F and ¬F−→ T) wi h he addi ional ans o ma ions o empo al ope a o s: ¬◦ϕ−→ ◦¬ϕ¬ϕ−→ ♦¬ϕ¬♦ϕ−→ ¬ϕ ¬(ϕUψ)−→ ¬ϕR¬ψ¬(ϕRψ)−→ ¬ϕU¬ψ The ollowing esul [26] can be easily es ablished. IP oposi ion 5 (T ansla ion in o NNF p ese es sa is iabili y) . Fo any PLTL o mula ϕ , he ollowing holds hM,0i |=ϕi hM,0i |=NNF(ϕ). As a simple example, NNF(¬◦¬a) = ◦♦a. We will u ilise his in §3. In wha ollows we deal wi h se s o o mulae in NNF . Li e als and o mulae in NNF o he o m F , T and ◦ϕ a e called elemen a y, he emaining o mulae a e subsequen ly called non-elemen a y. In addi ion, se s o elemen a y o mulae a e also called elemen a y. IDe ini ion 6 (Consis en se o PLTL o mulae in NNF) . A se o PLTL o mulae in NNF is consis en i i does nei he con ain F , no {ϕ, NNF ( ¬ϕ ) } o any o mula ϕ . O he wise i is called inconsis en . No e ha he abo e no ion o consis ency is syn ac ic. To check whe he {ϕ, ψ} is inconsis en we es i ϕ=NNF(¬ψ). The cos o his check is linea on he leng h o he o mula. Since ou ansi ion sys em speci ica ions a e gi en by se s o PLTL o mulae and PLTL has he ini e model p ope y [ 33 ] we can conside i s in e p e a ion o e cyclic s uc u es. No ing ha an in ini e sequence s0, s1, . . . , sk, . . . induces he successo ela ion, R , such ha ( si, si+1 ) ∈R o all i∈π , we de ine below he no ions o a cyclic sequence, cyclic pa h and cyclic model. IDe ini ion 7 (Cyclic Sequence, Cyclic Pa h) . Le π be a ini e sequence o s a es π = s0, s1, . . . , sj. Then πis cyclic i he e exis s si,0≤i≤jsuch ha (sj, si)∈R. A sequence si, . . . , sjis a loop wi h a cycling elemen siabb e ia ed as hsi, . . . , sjiω. A cyclic pa h o e a cyclic sequence πis an in ini e sequence ξ(π) = s0, s1, . . . , si−1hsi, si+1, . . . , sjiω. TIME 2019 12:8 Towa ds Ce i ied Model Checking o PLTL Using One-Pass Tableaux IDe ini ion 8 (Cyclic Model).A model Mis cyclic i i is a cyclic pa h. Now, assuming ha PLTL o mulae a e in e p e ed o e cyclic models, we o e iew he cons uc ion o he one-pass ableau τ↑ pl l applied o some inpu Σ, in symbols τ↑ pl l (Σ), adap ing he echnique de eloped in [ 15 ]. We will see, in he subsequen sec ions, he bene i s o i s main ea u e – checking he alidi y o he gi en inpu in “one pass”, wi hou he second “pass” whe e an auxilia y g aph is buil o check i all he e en uali ies a e sa is ied o no . IDe ini ion 9 (Tableau, Consis en Node, Closed b anch) . A one-pass ableau o a se o o mulae Σ, abb e ia ed as τ↑ pl l (Σ) is a labelled ee T , whe e nodes a e labeled wi h se s o o mulae, such ha he ollowing wo condi ions hold: (a) The oo is labelled by he ableau inpu , Σ. (b) Any o he node, m , is labelled wi h se s o o mulae as he esul o he applica ion o one o he expansion ules o he pa en node, n. A node n∈T is consis en , abb e ia ed as n> , i i s label is a consis en se o o mulae (see De . 6), else nis inconsis en , abb e ia ed as n⊥. I a b anch, b, o T, con ains an inconsis en node n⊥, hen bis closed, else bis open. In o mal In oduc ion o one-pass ableau. In he se o expansion ules, on he op o he s anda d α−β ules, we also ha e β+ ules ha a e cha ac e is ic (and c ucial!) o ou cons uc ion. These ules (which we e o iginally in oduced in [ 14 , 15 ]) e lec ou dedica ed accoun o he e en uali ies, namely, we ea an e en uali y as occu ing in some con ex . By he con ex o he selec ed e en uali y, we unde s and a collec ion o all o he o mulae wi hin he label o he node. Subsequen ly, β+ ules use he con ex o o ce e en uali ies o be ul illed as soon as possible. The ableau expansion ules apply epea edly un il hey p oduce an inconsis en node, n⊥ , o a node wi h he labels ha al eady occu ed wi hin he gi en pa h. In he o me case he expansion o he gi en b anch e mina es wi h n⊥ as a lea . In he la e case, a epe i i e node in he b anch wi nesses ha he b anch is open. Once no mo e expansion ( α−β, β+ ype) ules a e applicable o he gi en b anch wi h he las consis en node n> , he expansion ules ensu e ha i s labelling is simila o a “s a e” in he s anda d empo al ableau. Then he “nex -s a e” ule applies which gene a es successo s wi h he labels ha a e a gumen s o all ◦ modali ies and he whole cycle o applying he expansion and he “nex -s a e” ules is epea ed un il he ableau cons uc ion e mina es. The na u e o ou ules ensu es ha he e mina ed ableau is ei he closed, indica ing ha he inpu does no ha e a model, hence unsa is iable, o open, indica ing a model o he ableau inpu . 2.3 τ↑ pl l Rules Recall ha all o mulae in he inpu o he ableau ha e been al eady ans o med in o hei NNF. P esen ing α -, β - and “nex -s a e” ules o he cons uc ion o he seman ic ableaux, we assume ha hese apply espec i ely, o α - o mulae, β - o mulae and “nex ”- o mulae such ha α1 deno es he se o o mulae in he conclusion o an α - ule, while β1, β2 deno e he se s o o mulae in he al e na i e conclusions o a β - ule, and γ1 deno es he esul o “jumping” om a s a e o a p e-s a e. The se s o α−β ules a e gi en in Table 1. These a e s anda d in empo al ableaux cons uc ion (see, o ins ance, [2]). A. Abuin, A. Bolo o , U. Díaz de Ce io, M. He mo, and P. Lucio 12:9 Table 1 α−β- ules. α α1 (∧)ϕ∧ψ ϕ, ψ ()ϕ ϕ, ◦ϕ β β1β2 (U)ϕUψ ψ ϕ, ◦(ϕUψ) (R)ϕRψ ϕ, ψ ψ, ◦(ϕRψ) (∨)ϕ∨ψ ϕ ψ (♦)♦ϕ ϕ ◦♦ϕ Table 2 β+- ules, whe e ∆is a (possibly emp y) se (conjunc ion) o o mulae, I ∆ 6 = ∅ hen ∆ 0 is a se (conjunc ion) o all elemen s o ∆excep o  - o mulae and ¬ ∆ 0 is he disjunc ion o all nega ed elemen s o ∆0, else ¬∆0is F. β β1β2 (U)+∆, ϕUψ∆, ψ ∆, ϕ, ◦((ϕ∧(NNF(¬∆0)))Uψ) (♦)+∆,♦ϕ∆, ϕ ∆,◦((NNF(¬∆0))Uϕ) β+ ules (see Table 2) a e c ucial in he cons uc ion o τ↑ pl l as hey use he so-called con ex ,∆, o o ce he e en uali y ϕUψ o be ul illed as soon as possible. We illus a e his concep on he ( U ) + ule. When ( U ) + is applied o a node labelled by a se o o mulae { ∆ , ϕUψ} , hen he con ex is ∆and he esul ing labelling o he nex node con ains he o mula ( ϕ∧ ¬ ∆) Uψ , whe e ¬ ∆means he disjunc ion o all nega ed elemen s o ∆. The e o e, i ψ is no sa is ied, hen ¬ ∆also belongs o he label o ha node. This means ha he con ex , ∆, o he p e ious label is no epea ed. As ∆is a ini e se /conjunc ion o o mulae and ¬ ∆is he ini e disjunc ion o he nega ions o he o mulae in ∆, he ( U ) + ule o ces a leas one o mula in ∆ o be alsi ied du ing he ansi ion om he p e ious node o he subsequen one, whene e ψis no sa is ied. No e ha he (U)+ ule only applies o some selec ed e en uali y, and in his sense, he unique e en uali y, which becomes ma ked. Each applica ion o he ( U ) + ule o he se { ∆ , ϕUψ} in oduces he so-called nex -s ep a ian ( ϕ∧ ( NNF ( ¬ ∆ 0 )) Uψ whe e ∆ 0 , as we know, is a conjunc ion o all elemen s o ∆ excep o  - o mulae, which keeps he ma k o he selec ed e en uali y. No e ha any o mula o he ype ϕ , which was a membe o ∆, will be epea ed o e e and i we keep i in ∆ 0 i would appea in he esul ing NNF ( ¬ ∆ 0 )as a disjunc ♦¬ϕ which would ne e be sa is ied. Hence, any  - o mula can be immedia ely d opped when we o m ∆ 0 . Fo he soundness o he cons uc ion, each node o he ableau mus ha e a mos one ma ked e en uali y, i.e. he one o which he ( U ) + has been applied. No e ha when a node o he ableau does no con ain any ma ked e en uali y, hen one o hem is andomly ma ked. The ( U ) + ule allows us o a oid he cons uc ion o he auxilia y g aph o s ages ( he second pass in wo-pass ableau me hods) which is used o de e mine whe he all e en uali ies a e sa is ied o no . The o he β+ ule, ( ♦ ) + , is ob iously de i able om he ( U ) + ule. Howe e , we p esen i as pa o he ableau as i s applica ion makes p oo s mo e anspa en o he eade and he use o he ableau as a model checke . We will explain his in he subsequen sec ions o he pape . I is wo h no ing ha , because in he β+ ules, ¬ ∆ 0 = F whene e ∆ = ∅ , he β ules ( U )and ( ♦ )become pa icula cases o β+ ules ( U ) + and ( ♦ ) + when ∆ = ∅ . In his case he β2 child o he ( U ) + ule is educed o ϕ, ◦ ( FUψ ), om which we can de i e he β2 child o he (U) ule. TIME 2019 12:16 Towa ds Ce i ied Model Checking o PLTL Using One-Pass Tableaux We ha e also implemen ed a me hod one_s ep_sol e _p in which p in s in o a ile o ex all applica ions o he TTC ules ha a e hidden in he big-s ep p oo . Indeed, i is a p in ing e sion o he me hod one_s ep_sol e . Calling one_s ep_sol e _p in , ins ead o one_s ep_sol e , we can gene a e a small-s ep p oo (see lemma unningExample_small- S ep_p oo ) o he use wishing o check he Isabelle’s subgoals s ep by s ep. This p oo is he esul o he subs i u ion, in he big-s ep p oo , o each o he i e occu ences o apply one_s ep_sol e by he lis o “apply” ins uc ions o TTC_Calculus ules. The me hod one_s ep_sol e _p in p in s such a lis , in a ex ile, while i is sol ing he goal. 5 Conclusions In his pape we ha e p esen ed a no el amewo k o applying a Ce i ied Model Checking me hodology. Ou me hod in ol es he ep esen a ion o he sys em speci ica ion, S , in a speci ic o ma ha e lec s he dynamic beha iou o he sys em. Fi s , i in ol es he o maliza ion o he “ini ial condi ions”, ( he Ini PLTL o mula), ha speci ies he ini ial s a es o he model o be build. Second, we use he ep esen a ion, TR , o he ansi ion ela ion o build a s a e space o he sys em, as a “global in a ian ”. Finally, he p ope y, P , o be checked agains he speci ica ion S is w i en as a PLTL o mula. This ask is pe o med by a one-pass empo al ableau, τ↑ pl l . I akes S, ¬P as i s inpu (con e ed in o he NNF). Fo an e en uali y o be ul illed, he ableau echnique essen ially uses i s con ex . Tableau ules ha deal wi h he e en uali ies in NNF ( ¬P ), o ce hei ul ilmen “as soon as possible”. This p ocess is op imised by a SAT sol e , which ackles non- empo al con en o he ableau nodes. The ableau me hod, in one pass, ei he e u ns a nega i e answe , p oducing a coun e -example, hus showing ha P is no sa is ied by S , o e i ies P agains he sys em speci ica ion. In he la e case, ou me hod gene a es an explici and easily eadable e idence in Isabelle/HOL. In his way he ableau esul is o mally p o en and he use can e iew he es o make su e ha e e y hing is wo king as expec ed (o ha no e o s ha e been made wi h he speci ica ion). Ou u u e wo k will co e h ee di ec ions. Fi s , i is u he wo k on he implemen a ion o and expe imen a ion wi h he one-pass ableau and he embedded SAT sol e . Second, he de eloped Isabelle au oma ic sol e o p oo gene a ion is only an ini ial p o o ype and we will imp o e i s e iciency. Finally, no e ha he one-pass ableau me hod has been also de eloped o he b anching- ime se ing, ackling Compu a ion T ee Logic CTL ([ 6 ]), widely used in model checking, and o a iche logic, ECT L] ([ 5 ]). This will enable us o ex end he use o he one-pass ableau as a model checke o he b anching- ime se ing, as he ex ensions a e concep ually in ui i e. Re e ences 1 Hasan Amjad. P og amming a Symbolic Model Checke in a Fully Expansi e Theo em P o e . In Theo em P o ing in Highe O de Logics, pages 171–187. Sp inge Be lin Heidelbe g, 2003. doi:10.1007/10930755_11. 2 Mo dechai Ben-A i. Ma hema ical Logic o Compu e Science. Sp inge -Ve lag, London, 2012. doi:10.1007/978-1-4471-4129-7. 3 A min Bie e, Alessand o Cima i, Edmund M. Cla ke, Masahi o Fuji a, and Yunshan Zhu. Symbolic Model Checking Using SAT P ocedu es Ins ead o BDDs. In P oceedings o he 36 h Annual ACM/IEEE Design Au oma ion Con e ence, DAC ’99, pages 317–320, New Yo k, NY, USA, 1999. ACM. doi:10.1145/309847.309942. A. Abuin, A. Bolo o , U. Díaz de Ce io, M. He mo, and P. Lucio 12:17 4 A min Bie e and Daniel K öning. SAT-based model checking. In Edmund M. Cla ke, Thomas A. Henzinge , Helmu Vei h, and Rode ick Bloem, edi o s, Handbook o Model Checking, pages 277– 303. Sp inge In e na ional Publishing, Cham, 2018. doi:10.1007/978-3-319-10575-8_10. 5 Alexande Bolo o , Mon se a He mo, and Paqui Lucio. Ex ending Fai ness Exp essibili y o ECTL+: A T ee-S yle One-Pass Tableau App oach. In Na asha Alechina, Kje il Nø åg, and Wojciech Penczek, edi o s, 25 h In e na ional Symposium on Tempo al Rep esen a ion and Reasoning (TIME 2018), olume 120 o Leibniz In e na ional P oceedings in In o ma ics (LIPIcs), pages 5:1–5:22, Dags uhl, Ge many, 2018. Schloss Dags uhl–Leibniz-Zen um ue In o ma ik. doi:10.4230/LIPIcs.TIME.2018.5. 6 Kai B ünnle and Ma in Lange. Cu - ee sequen sys ems o empo al logic. The Jou nal o Logic and Algeb aic P og amming, 76(2):216–225, 2008. doi:10.1016/j.jlap.2008.02.004. 7 CENELEC and EN50128. 50128. Railway applica ions-Communica ion, Signaling and P o- cessing Sys ems-So wa e o Railway Con ol and P o ec ion Sys ems, 2011. 8 Alessand o Cima i, Edmund Cla ke, Faus o Giunchiglia, and Ma co Ro e i. NUSMV: a new symbolic model checke . In e na ional Jou nal on So wa e Tools o Technology T ans e , 2(4):410–425, Ma ch 2000. doi:10.1007/s100090050046. 9 Koen Claessen and Niklas Sö ensson. A li eness checking algo i hm ha coun s. In Gianpie o Cabodi and Sa nam Singh, edi o s, Fo mal Me hods in Compu e -Aided Design, FMCAD 2012, Camb idge, UK, pages 52–59. IEEE, 2012. 10 Edmund M. Cla ke and E. Allen Eme son. Design and Syn hesis o Synch oniza ion Skele ons Using B anching-Time Tempo al Logic. In Logics o P og ams, Wo kshop, Yo k own Heigh s, New Yo k, May 1981, pages 52–71, 1981. doi:10.1007/BFb0025774. 11 Edmund M. Cla ke, O na G umbe g, and Do on A. Peled. Model Checking. MIT P ess, Camb idge, MA, USA, 1999. 12 Ma co Comini, Lau a Ti olo, and Alicia Villanue a. Abs ac Diagnosis o ccp using a Linea Tempo al Logic. Theo y and P ac ice o Logic P og amming, 14(4-5):787–801, 2014. doi:10.1017/S1471068414000349. 13 Ja ie Espa za, Pe e Lammich, René Neumann, Tobias Nipkow, Alexande Schimp , and Jan- Geo g Smaus. A Fully Ve i ied Execu able LTL Model Checke . In Compu e Aided Ve i ica ion, pages 463–478. Sp inge Be lin Heidelbe g, 2013. doi:10.1007/978-3-642-39799-8_31. 14 Joxe Gain za ain, Mon se a He mo, Paqui Lucio, Ma isa Na a o, and Fe nando O ejas. A Cu -F ee and In a ian -F ee Sequen Calculus o PLTL. In Jacques Dupa c and Thomas A. Henzinge , edi o s, Compu e Science Logic, 21s In e na ional Wo kshop, CSL 2007, 16 h Annual Con e ence o he EACSL, Lausanne, Swi ze land, Sep embe 11-15, 2007, P oceedings, olume 4646 o Lec u e No es in Compu e Science, pages 481–495. Sp inge , 2007. doi: 10.1007/978-3-540-74915-8_36. 15 Joxe Gain za ain, Mon se a He mo, Paqui Lucio, Ma isa Na a o, and Fe nando O ejas. Dual Sys ems o Tableaux and Sequen s o PLTL. The Jou nal o Logic and Algeb aic P og amming, 78(8):701–722, 2009. doi:10.1016/j.jlap.2009.05.001. 16 Rajee Go é. Tableau Me hods o Modal and Tempo al Logics. In Ma cello D’Agos ino, Do M. Gabbay, Reine Hähnle, and Joachim Posegga, edi o s, Handbook o Tableau Me hods, pages 297–396. Sp inge Ne he lands, Do d ech , 1999. doi:10.1007/978-94-017-1754-0_6 . 17 Albe o G iggio, Ma co Ro e i, and S e ano Tone a. Ce i ying P oo s o LTL Model Checking. In Fo mal Me hods in Compu e -Aided Design, FMCAD 2018, Aus in, USA, pages 1–9, Oc obe 2018. doi:10.23919/FMCAD.2018.8603022. 18 IEC. IEC 61508 Func ional sa e y o elec ical/elec onic/p og ammable elec onic sa e y- ela ed sys ems, 2010. 19 ISO. Road ehicles – Func ional sa e y, 2011. 20 Hen y Kau z and Ba Selman. Pushing he En elope: Planning, P oposi ional Logic, and S ochas ic Sea ch. In P oceedings o he Thi een h Na ional Con e ence on A i icial In elligence - Volume 2, AAAI’96, pages 1194–1201. AAAI P ess, 1996. URL: h p://dl.acm. o g/ci a ion.c m?id=1864519.1864564. TIME 2019 12:18 Towa ds Ce i ied Model Checking o PLTL Using One-Pass Tableaux 21 Jö g K eike , And zej Ta lecki, Moshe Y. Va di, and Reinha d Wilhelm. Modeling, Analysis, and Ve i ica ion - The Fo mal Me hods Mani es o 2010 (Dags uhl Pe spec i es Wo kshop 10482). Dags uhl Mani es os, 1(1):21–40, 2011. doi:10.4230/DagMan.1.1.21. 22 Tuomas Kuismin and Keijo Heljanko. Inc easing Con idence in Li eness Model Checking Resul s wi h P oo s. In Vale ia Be acco and Axel Legay, edi o s, Ha dwa e and So wa e: Ve i ica ion and Tes ing, pages 32–43. Sp inge In e na ional Publishing, 2013. 23 O na Kup e man and Moshe Y. Va di. F om complemen a ion o ce i ica ion. Theo e ical Compu e Science, 345(1):83–100, 2005. doi:10.1007/978-3-540-24730-2_43. 24 Jianwen Li, Geguang Pu, Lijun Zhang, Moshe Y Va di, and Ji eng He. Accele a ing LTL sa is iabili y checking by SAT sol e s. Jou nal o Logic and Compu a ion, 28(6):1011–1030, Ap il 2018. doi:10.1093/logcom/exy013. 25 Jianwen Li, Shu ang Zhu, Geguang Pu, Lijun Zhang, and Moshe Y. Va di. SAT-based explici LTL easoning and i s applica ion o sa is iabili y checking. Fo mal Me hods in Sys em Design, Janua y 2019. doi:10.1007/s10703-018-00326-5. 26 Zoha Manna and Ami Pnueli. The Tempo al Logic o Reac i e and Concu en Sys ems. Sp inge -Ve lag, Be lin, Heidelbe g, 1992. doi:10.1007/978-1-4612-0931-7. 27 Daniel Ma ichuk, Toby Mu ay, and Maka ius Wenzel. Eisbach: A P oo Me hod Lan- guage o Isabelle. Jou nal o Au oma ed Reasoning, 56, Janua y 2016. doi:10.1007/ s10817-015-9360-2. 28 Alain Mebsou and Cesa e Tinelli. P oo Ce i ica es o SMT-based Model Checke s o In ini e-s a e Sys ems. In P oceedings o he 16 h Con e ence on Fo mal Me hods in Compu e - Aided Design, FMCAD ’16, pages 117–124, 2016. doi:10.1109/FMCAD.2016.7886669. 29 Keda S. Namjoshi. Ce i ying Model Checke s. In P oceedings o he 13 h In e na ional Con e ence on Compu e Aided Ve i ica ion, CAV ’01, pages 2–13. Sp inge -Ve lag, 2001. doi:10.1007/3-540-44585-4_2. 30 Tobias Nipkow, Law ence C. Paulson, and Ma kus Wenzel. Isabelle/HOL — A P oo Assis an o Highe -O de Logic, olume 2283 o LNCS. Sp inge , 2002. doi:10.1007/3-540-45949-9 . 31 Jean-Pie e Queille and Joseph Si akis. Speci ica ion and e i ica ion o concu en sys ems in CESAR. In Ma iangiola Dezani-Ciancaglini and Ugo Mon ana i, edi o s, In e na ional Sym- posium on P og amming, pages 337–351, Be lin, Heidelbe g, 1982. Sp inge Be lin Heidelbe g. doi:10.1007/3-540-11494-7_22. 32 K is in Y. Rozie and Moshe Y. Va di. LTL Sa is iabili y Checking. In D agan Bošnački and S e an Edelkamp, edi o s, Model Checking So wa e, pages 149–167, Be lin, Heidelbe g, 2007. Sp inge Be lin Heidelbe g. doi:10.1007/978-3-540-73370-6_11. 33 A a inda P. Sis la and Edmund M. Cla ke. The Complexi y o P oposi ional Linea Tempo al Logics. In P oceedings o he Fou een h Annual ACM Symposium on Theo y o Compu ing, STOC ’82, pages 159–168, New Yo k, NY, USA, 1982. ACM. doi:10.1145/800070.802189.