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}.