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.
