• Source: CTL

CTL can refer to:

Champions Tennis League, a tennis championship league in India
Chronic training load, cumulative sports training
Circuit Total Limitation, US standard for electrical panels
Coal to liquids, coal liquefaction
Combat Tank, Light such as the Marmon-Herrington CTLS
Commission de transport de la Ville de Laval
Complex Text Layout in typesetting
Core Transfer Library, a list of college courses for transfer credit among educational institutions in Indiana
Cut-to-length logging
Cytotoxic T lymphocyte
Constructive total loss, in marine insurance




Companies


Computer Technology Limited, a British computer manufacturer of the 1970s and 1980s
Communications Technology Laboratory, a NIST laboratory since 2010
CTL Corporation, manufacturer of Chromebooks




Computing


Certificate Transparency Logs
Computation tree logic
Control key, a computer keyboard key
CTL timecode, a timecode used on video tape




Culture


Changeling: The Lost, a tabletop role-playing game




Transportation


Centralia, Washington (Amtrak station), USA, Amtrak station code
Charleville Airport, Queensland, Australia (IATA airport code)
• Source: CTL*

CTL* is a superset of computational tree logic (CTL) and linear temporal logic (LTL). It freely combines path quantifiers and temporal operators. Like CTL, CTL* is a branching-time logic. The formal semantics of CTL* formulae are defined with respect to a given Kripke structure.




History


LTL had been proposed for the verification of computer programs, first by Amir Pnueli in 1977. Four years later in 1981 E. M. Clarke and E. A. Emerson invented CTL and CTL model checking. CTL* was defined by E. A. Emerson and Joseph Y. Halpern in 1983.
CTL and LTL were developed independently before CTL*. Both sublogics have become standards in the model checking community, while CTL* is of practical importance because it provides an expressive testbed for representing and comparing these and other logics. This is surprising because the computational complexity of model checking in CTL* is not worse than that of LTL: they both lie in PSPACE.




Syntax


The language of well-formed CTL* formulae is generated by the following unambiguous (with respect to bracketing) context-free grammar:




Φ
::=
⊥
∣
⊤
∣
p
∣
(
¬
Φ
)
∣
(
Φ
∧
Φ
)
∣
(
Φ
∨
Φ
)
∣
(
Φ
⇒
Φ
)
∣
(
Φ
⇔
Φ
)
∣
A
ϕ
∣
E
ϕ


{\displaystyle \Phi ::=\bot \mid \top \mid p\mid (\neg \Phi )\mid (\Phi \land \Phi )\mid (\Phi \lor \Phi )\mid (\Phi \Rightarrow \Phi )\mid (\Phi \Leftrightarrow \Phi )\mid A\phi \mid E\phi }





ϕ
::=
Φ
∣
(
¬
ϕ
)
∣
(
ϕ
∧
ϕ
)
∣
(
ϕ
∨
ϕ
)
∣
(
ϕ
⇒
ϕ
)
∣
(
ϕ
⇔
ϕ
)
∣
X
ϕ
∣
F
ϕ
∣
G
ϕ
∣
[
ϕ
U
ϕ
]
∣
[
ϕ
R
ϕ
]


{\displaystyle \phi ::=\Phi \mid (\neg \phi )\mid (\phi \land \phi )\mid (\phi \lor \phi )\mid (\phi \Rightarrow \phi )\mid (\phi \Leftrightarrow \phi )\mid X\phi \mid F\phi \mid G\phi \mid [\phi U\phi ]\mid [\phi R\phi ]}


where



p


{\displaystyle p}

ranges over a set of atomic formulas. Valid CTL*-formulae are built using the nonterminal



Φ


{\displaystyle \Phi }

. These formulae are called state formulae, while those created by the symbol



ϕ


{\displaystyle \phi }

are called path formulae. (The above grammar contains some redundancies; for example



Φ
∨
Φ


{\displaystyle \Phi \lor \Phi }

as well as implication and equivalence can be defined as just for Boolean algebras (or propositional logic) from negation and conjunction, and the temporal operators X and U are sufficient to define the other two.)
The operators basically are the same as in CTL. However, in CTL, every temporal operator (



X
,
F
,
G
,
U


{\displaystyle X,F,G,U}

) has to be directly preceded by a quantifier, while in CTL* this is not required. The universal path quantifier may be defined in CTL* in the same way as for classical predicate calculus



A
ϕ
=
¬
E
¬
ϕ


{\displaystyle A\phi =\neg E\neg \phi }

, although this is not possible in the CTL fragment.




= Examples of formulae

=
CTL* formula that is neither in LTL or in CTL:



E
X
(
p
)
∧
A
F
G
(
p
)


{\displaystyle EX(p)\land AFG(p)}


LTL formula that is not in CTL:




A
F
G
(
p
)


{\displaystyle \ AFG(p)}


CTL formula that is not in LTL:




E
X
(
p
)


{\displaystyle \ EX(p)}


CTL* formula that is in CTL and LTL:




A
G
(
p
)


{\displaystyle \ AG(p)}


Remark: When taking LTL as subset of CTL*, any LTL formula is implicitly prefixed with the universal path quantifier



A


{\displaystyle A}

.




Semantics


The semantics of CTL* are defined with respect to some Kripke structure. As the names imply, state formulae are interpreted with respect to the states of this structure, while path formulae are interpreted over paths on it.




= State formulae

=
If a state



s


{\displaystyle s}

of the Kripke structure satisfies a state formula



Φ


{\displaystyle \Phi }

it is denoted



s
⊨
Φ


{\displaystyle s\models \Phi }

. This relation is defined inductively as follows:






(


(


M


,
s
)
⊨
⊤


)


∧


(


(


M


,
s
)
⊭
⊥


)




{\displaystyle {\Big (}({\mathcal {M}},s)\models \top {\Big )}\land {\Big (}({\mathcal {M}},s)\not \models \bot {\Big )}}







(


(


M


,
s
)
⊨
p


)


⇔


(


p
∈
L
(
s
)


)




{\displaystyle {\Big (}({\mathcal {M}},s)\models p{\Big )}\Leftrightarrow {\Big (}p\in L(s){\Big )}}







(


(


M


,
s
)
⊨
¬
Φ


)


⇔


(


(


M


,
s
)
⊭
Φ


)




{\displaystyle {\Big (}({\mathcal {M}},s)\models \neg \Phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s)\not \models \Phi {\Big )}}







(


(


M


,
s
)
⊨

Φ

1


∧

Φ

2




)


⇔


(




(


(


M


,
s
)
⊨

Φ

1




)


∧


(


(


M


,
s
)
⊨

Φ

2




)




)




{\displaystyle {\Big (}({\mathcal {M}},s)\models \Phi _{1}\land \Phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\models \Phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}}







(


(


M


,
s
)
⊨

Φ

1


∨

Φ

2




)


⇔


(




(


(


M


,
s
)
⊨

Φ

1




)


∨


(


(


M


,
s
)
⊨

Φ

2




)




)




{\displaystyle {\Big (}({\mathcal {M}},s)\models \Phi _{1}\lor \Phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\models \Phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}}







(


(


M


,
s
)
⊨

Φ

1


⇒

Φ

2




)


⇔


(




(


(


M


,
s
)
⊭

Φ

1




)


∨


(


(


M


,
s
)
⊨

Φ

2




)




)




{\displaystyle {\Big (}({\mathcal {M}},s)\models \Phi _{1}\Rightarrow \Phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\not \models \Phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}}







(


(


M


,
s
)
⊨

Φ

1


⇔

Φ

2




)


⇔


(




(




(


(


M


,
s
)
⊨

Φ

1




)


∧


(


(


M


,
s
)
⊨

Φ

2




)




)


∨


(


¬


(


(


M


,
s
)
⊨

Φ

1




)


∧
¬


(


(


M


,
s
)
⊨

Φ

2




)




)




)




{\displaystyle {\bigg (}({\mathcal {M}},s)\models \Phi _{1}\Leftrightarrow \Phi _{2}{\bigg )}\Leftrightarrow {\bigg (}{\Big (}{\big (}({\mathcal {M}},s)\models \Phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}\lor {\Big (}\neg {\big (}({\mathcal {M}},s)\models \Phi _{1}{\big )}\land \neg {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}{\bigg )}}







(


(


M


,
s
)
⊨
A
ϕ


)


⇔


(


π
⊨
ϕ


{\displaystyle {\Big (}({\mathcal {M}},s)\models A\phi {\Big )}\Leftrightarrow {\Big (}\pi \models \phi }

for all paths




π


{\displaystyle \ \pi }

starting in



s


)




{\displaystyle s{\Big )}}







(


(


M


,
s
)
⊨
E
ϕ


)


⇔


(


π
⊨
ϕ


{\displaystyle {\Big (}({\mathcal {M}},s)\models E\phi {\Big )}\Leftrightarrow {\Big (}\pi \models \phi }

for some path




π


{\displaystyle \ \pi }

starting in



s


)




{\displaystyle s{\Big )}}





= Path formulae

=
The satisfaction relation



π
⊨
ϕ


{\displaystyle \pi \models \phi }

for path formulae




ϕ


{\displaystyle \ \phi }

and a path



π
=

s

0


→

s

1


→
⋯


{\displaystyle \pi =s_{0}\to s_{1}\to \cdots }

is also defined inductively. For this, let




π
[
n
]


{\displaystyle \ \pi [n]}

denote the sub-path




s

n


→

s

n
+
1


→
⋯


{\displaystyle s_{n}\to s_{n+1}\to \cdots }

:






(


π
⊨
Φ


)


⇔


(


(


M


,

s

0


)
⊨
Φ


)




{\displaystyle {\Big (}\pi \models \Phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s_{0})\models \Phi {\Big )}}







(


π
⊨
¬
ϕ


)


⇔


(


π
⊭
ϕ


)




{\displaystyle {\Big (}\pi \models \neg \phi {\Big )}\Leftrightarrow {\Big (}\pi \not \models \phi {\Big )}}







(


π
⊨

ϕ

1


∧

ϕ

2




)


⇔


(




(


π
⊨

ϕ

1




)


∧


(


π
⊨

ϕ

2




)




)




{\displaystyle {\Big (}\pi \models \phi _{1}\land \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \models \phi _{1}{\big )}\land {\big (}\pi \models \phi _{2}{\big )}{\Big )}}







(


π
⊨

ϕ

1


∨

ϕ

2




)


⇔


(




(


π
⊨

ϕ

1




)


∨


(


π
⊨

ϕ

2




)




)




{\displaystyle {\Big (}\pi \models \phi _{1}\lor \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \models \phi _{1}{\big )}\lor {\big (}\pi \models \phi _{2}{\big )}{\Big )}}







(


π
⊨

ϕ

1


⇒

ϕ

2




)


⇔


(




(


π
⊭

ϕ

1




)


∨


(


π
⊨

ϕ

2




)




)




{\displaystyle {\Big (}\pi \models \phi _{1}\Rightarrow \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \not \models \phi _{1}{\big )}\lor {\big (}\pi \models \phi _{2}{\big )}{\Big )}}







(


π
⊨

ϕ

1


⇔

ϕ

2




)


⇔


(




(




(


π
⊨

ϕ

1




)


∧


(


π
⊨

ϕ

2




)




)


∨


(


¬


(


π
⊨

ϕ

1




)


∧
¬


(


π
⊨

ϕ

2




)




)




)




{\displaystyle {\bigg (}\pi \models \phi _{1}\Leftrightarrow \phi _{2}{\bigg )}\Leftrightarrow {\bigg (}{\Big (}{\big (}\pi \models \phi _{1}{\big )}\land {\big (}\pi \models \phi _{2}{\big )}{\Big )}\lor {\Big (}\neg {\big (}\pi \models \phi _{1}{\big )}\land \neg {\big (}\pi \models \phi _{2}{\big )}{\Big )}{\bigg )}}







(


π
⊨
X
ϕ


)


⇔


(


π
[
1
]
⊨
ϕ


)




{\displaystyle {\Big (}\pi \models X\phi {\Big )}\Leftrightarrow {\Big (}\pi [1]\models \phi {\Big )}}







(


π
⊨
F
ϕ


)


⇔


(


∃
n
⩾
0
:
π
[
n
]
⊨
ϕ


)




{\displaystyle {\Big (}\pi \models F\phi {\Big )}\Leftrightarrow {\Big (}\exists n\geqslant 0:\pi [n]\models \phi {\Big )}}







(


π
⊨
G
ϕ


)


⇔


(


∀
n
⩾
0
:
π
[
n
]
⊨
ϕ


)




{\displaystyle {\Big (}\pi \models G\phi {\Big )}\Leftrightarrow {\Big (}\forall n\geqslant 0:\pi [n]\models \phi {\Big )}}







(


π
⊨
[

ϕ

1


U

ϕ

2


]


)


⇔


(


∃
n
⩾
0
:


(


π
[
n
]
⊨

ϕ

2


∧
∀
0
⩽
k
<
n
:

π
[
k
]
⊨

ϕ

1




)




)




{\displaystyle {\Big (}\pi \models [\phi _{1}U\phi _{2}]{\Big )}\Leftrightarrow {\Big (}\exists n\geqslant 0:{\big (}\pi [n]\models \phi _{2}\land \forall 0\leqslant k




Decision problems


CTL* model checking (of an input formula on a fixed model) is PSPACE-complete and the satisfiability problem is 2EXPTIME-complete.




See also


Temporal logic
Kripke structure
Model checking
Reo Coordination Language




References



Amir Pnueli: The temporal logic of programs. Proceedings of the 18th IEEE Annual Symposium on Foundations of Computer Science (FOCS), 1977, 46–57. DOI= 10.1109/SFCS.1977.32
E. Allen Emerson, Joseph Y. Halpern: "Sometimes" and "not never" revisited: on branching versus linear time temporal logic. Journal of the ACM 33, 1 (Jan. 1986), 151–178. DOI= http://doi.acm.org/10.1145/4904.4999
Ph. Schnoebelen: The Complexity of Temporal Logic Model Checking. Advances in Modal Logic 2002: 393–436




External links


CTL Teaching slides of professor Alessandro Artale at the Free University of Bozen-Bolzano

Kata Kunci Pencarian:

• Ipilimumab
• CenturyLink
• Sel T pembunuh
• DLL Hell
• Imunoterapi
• Sekolah Tinggi Ilmu Hukum Sumpah Pemuda
• Institut Standar dan Teknologi Nasional
• Antigen
• Jalur kereta api Bandung–Ciwidey
• Faktor produksi
• CTLGroup
• CTLS
• CTLD
• CTL
• CTL*
• Erdos CTL
• Probabilistic CTL
• CTL Corporation
• Secunda CTL
• Marmon–Herrington CTLS