120:. For example, CTL can specify that when some initial condition is satisfied (e.g., all program variables are positive or no cars on a highway straddle two lanes), then all possible executions of a program avoid some undesirable condition (e.g., dividing a number by zero or two cars colliding on a highway). In this example, the safety property could be verified by a model checker that explores all possible transitions out of program states satisfying the initial condition and ensures that all such executions satisfy the property. Computation tree logic belongs to a class of
33:
2687:
466:
4377:
4067:
2372:
190:
4073:
3763:
2682:{\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 )}}
461:{\displaystyle {\begin{aligned}\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 \quad {\mbox{AX }}\phi \mid {\mbox{EX }}\phi \mid {\mbox{AF }}\phi \mid {\mbox{EF }}\phi \mid {\mbox{AG }}\phi \mid {\mbox{EG }}\phi \mid {\mbox{A }}\mid {\mbox{E }}\end{aligned}}}
2366:
3757:
3565:
3373:
3181:
1988:
2177:
2989:
2838:
4372:{\displaystyle {\bigg (}({\mathcal {M}},s)\models E{\bigg )}\Leftrightarrow {\bigg (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}}
4062:{\displaystyle {\bigg (}({\mathcal {M}},s)\models A{\bigg )}\Leftrightarrow {\bigg (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}}
2183:
3571:
3379:
3187:
2995:
5318:"Depending on what happens in the future (E), it's possible that for the rest of time (G), I'll be guaranteed at least one (AF) chocolate-liking day still ahead of me. However, if something ever goes wrong, then all bets are off and there's no guarantee about whether I'll ever like chocolate."
1805:
163:
Since the introduction of CTL, there has been debate about the relative merits of CTL and LTL. Because CTL is more computationally efficient to model check, it has become more common in industrial use, and many of the most successful model-checking tools use CTL as a specification language.
1994:
1799:
1605:
2844:
2693:
5346:"From now until it's warm outside, I will like chocolate every single day. Once it's warm outside, all bets are off as to whether I'll like chocolate anymore. Oh, and it's guaranteed to be warm outside eventually, even if only for a single day."
1697:
2361:{\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 )}}
3752:{\displaystyle {\Big (}({\mathcal {M}},s)\models EF\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}
3560:{\displaystyle {\Big (}({\mathcal {M}},s)\models AF\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}
3368:{\displaystyle {\Big (}({\mathcal {M}},s)\models EG\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\forall i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}
3176:{\displaystyle {\Big (}({\mathcal {M}},s)\models AG\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\forall i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}
5719:
4387:
Rules 10–15 above refer to computation paths in models and are what ultimately characterise the "Computation Tree"; they are assertions about the nature of the infinitely deep computation tree rooted at the given state
1983:{\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 )}}
2172:{\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 )}}
674:
555:
4568:
1703:
731:
1210:
195:
5245:
5164:
4981:
4930:
5083:
5032:
1332:
1264:
5518:
A reduction from the model-checking problem of QCTL with the structure semantics, to TQBF (true quantified
Boolean formulae) has been proposed, in order to take advantage of the QBF solvers.
1512:
4759:
4714:
4669:
2984:{\displaystyle {\Big (}({\mathcal {M}},s)\models EX\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\models \phi {\big )}{\Big )}}
2833:{\displaystyle {\Big (}({\mathcal {M}},s)\models AX\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\models \phi {\big )}{\Big )}}
1484:
4480:
128: (LTL). Although there are properties expressible only in CTL and properties expressible only in LTL, all properties expressible in either logic can also be expressed in
1436:
4870:
4615:
4593:
4526:
4504:
800:
778:
756:
1611:
1384:
1016:, the temporal operators can be freely mixed. In CTL, operators must always be grouped in pairs: one path operator followed by a state operator. See the examples below.
611:
582:
5485:
5462:
4823:
1358:
4454:
4434:
1504:
108:
structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized. It is used in
5297:"It's always possible (AF) that I will suddenly start liking chocolate for the rest of time." (Note: not just the rest of my life, since my life is finite, while
4785:
4406:
1404:
1284:
1230:
489:
5814:
5322:
The two following examples show the difference between CTL and CTL*, as they allow for the until operator to not be qualified with any path operator (
5371:"It's possible that: there will eventually come a time when it will be warm forever (AG.Q) and that before that time there will always be
626:
498:
4531:
1794:{\displaystyle {\Big (}({\mathcal {M}},s)\models \neg \phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s)\not \models \phi {\Big )}}
834:
are the usual ones: ¬, ∨, ∧, ⇒ and ⇔. Along with these operators CTL formulas can also make use of the boolean constants
17:
809:
as its building blocks to make statements about the states of a system. These propositions are then combined into formulas using
5777:
685:
1028:
In CTL there are minimal sets of operators. All CTL formulas can be transformed to use only those operators. This is useful in
4456:
are said to be semantically equivalent if any state in any model that satisfies one also satisfies the other. This is denoted
5858:
5761:
5695:
5652:
5577:
1600:{\displaystyle {\Big (}({\mathcal {M}},s)\models \top {\Big )}\land {\Big (}({\mathcal {M}},s)\not \models \bot {\Big )}}
1165:
5170:
5089:
4936:
4885:
5889:
5038:
4987:
1289:
1235:
5742:
4720:
4675:
4630:
1447:
76:
54:
47:
5899:
5389:
4764:
It can be shown using such identities that a subset of the CTL temporal connectives is adequate if it contains
117:
5532:
5625:
David, Amélie; Laroussinie, Francois; Markey, Nicolas (2016). Desharnais, Josée; Jagadeesan, Radha (eds.).
5503:
5668:
Hossain, Akash; Laroussinie, François (2019). Gamper, Johann; Pinchinat, Sophie; Sciavicco, Guido (eds.).
5611:
5496:
4459:
5791:
5599:
5558:
1692:{\displaystyle {\Big (}({\mathcal {M}},s)\models p{\Big )}\Leftrightarrow {\Big (}p\in L(s){\Big )}}
1417:
41:
4828:
4598:
4576:
4509:
4487:
783:
761:
739:
5894:
1266:
is a transition relation, assumed to be serial, i.e. every state has at least one successor, and
5403:
are not equivalent and they have a common subset, which is a proper subset of both CTL and LTL.
1363:
806:
592:
563:
5810:"Automatic verification of finite-state concurrent systems using temporal logic specifications"
5786:
5467:
5444:
4790:
58:
5537:
5400:
5396:
125:
4879:; they allow unfolding the verification of a CTL connective towards its successors in time.
1337:
4439:
4419:
1489:
181:
5775:(1985). "Decision procedures and expressiveness in the temporal logic of branching time".
8:
5511:
4621:
1407:
874:
xists: there exists at least one path starting from the current state where Φ holds.
177:
109:
105:
4767:
5833:
5720:"Design and synthesis of synchronisation skeletons using branching time temporal logic"
5701:
5587:
5438:
4391:
1389:
1269:
1215:
831:
474:
157:
97:
5564:. Lecture Notes in Computer Science. Vol. 2031. Springer, Berlin. pp. 1–22.
4528:
are duals, being universal and existential computation path quantifiers respectively:
5854:
5800:
5757:
5738:
5705:
5691:
5669:
5648:
5573:
5527:
5385:
1159:
5837:
5626:
5823:
5796:
5730:
5681:
5680:. Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik: 11:1–11:20.
5638:
5637:. Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik: 28:1–28:15.
5565:
810:
557:
comprises a complete set of connectives, and the others can be defined using them.
173:
145:
141:
5643:
5846:
5674:
26th
International Symposium on Temporal Representation and Reasoning (TIME 2019)
5507:
1411:
5874:
5686:
5772:
1029:
814:
492:
121:
112:
of software or hardware artifacts, typically by software applications known as
5883:
5727:
Logic of
Programs, Proceedings of Workshop, Lecture Notes in Computer Science
839:
113:
5569:
5495:
the tree semantics. We label nodes of the computation tree. QCTL* = QCTL =
1286:
is a labelling function, assigning propositional letters to states. Let
5807:
5734:
1442:
495:. It is not necessary to use all connectives – for example,
5828:
5809:
5280:"It's possible I may like chocolate some day, at least for one day."
864:
ll: Φ has to hold on all paths starting from the current state.
669:{\displaystyle {\mbox{EF }}({\mbox{EG }}p\Rightarrow {\mbox{AF }}r)}
550:{\displaystyle \{\neg ,\land ,{\mbox{AX}},{\mbox{AU}},{\mbox{EU}}\}}
5384:
Computation tree logic (CTL) is a subset of CTL* as well as of the
4563:{\displaystyle \neg \mathrm {A} \Phi \equiv \mathrm {E} \neg \Phi }
5502:
the structure semantics. We label states. QCTL* = QCTL = MSO over
5631:
27th
International Conference on Concurrency Theory (CONCUR 2016)
5499:
over trees. Model checking and satisfiability are tower complete.
5255:
Let "P" mean "I like chocolate" and Q mean "It's warm outside."
896:
has to hold at the next state (this operator is sometimes noted
5676:. Leibniz International Proceedings in Informatics (LIPIcs).
5633:. Leibniz International Proceedings in Informatics (LIPIcs).
1047:
Some of the transformations used for temporal operators are:
835:
5770:
5756:(Second ed.). Cambridge University Press. p. 207.
5388:. CTL is also a fragment of Alur, Henzinger and Kupferman's
5267:"I will like chocolate from now on, no matter what happens."
1017:
1013:
129:
101:
5808:
Clarke, E. M.; Emerson, E. A. & Sistla, A. P. (1986).
938:
eventually has to hold (somewhere on the subsequent path).
726:{\displaystyle {\mbox{EF }}{\big (}r{\mbox{ U }}q{\big )}}
620:
For example, the following is a well-formed CTL formula:
5717:
5845:
Emerson, E. A. (1990). "Temporal and modal logic". In
5624:
1032:. One minimal set of operators is: {true, ∨, ¬,
707:
690:
654:
641:
631:
597:
568:
538:
528:
518:
442:
429:
413:
400:
387:
374:
361:
348:
335:
322:
5815:
5751:
5470:
5447:
5375:
way to get me to like chocolate the next day (EX.P)."
5173:
5092:
5041:
4990:
4939:
4888:
4831:
4793:
4770:
4723:
4678:
4633:
4601:
4579:
4534:
4512:
4490:
4462:
4442:
4422:
4394:
4076:
3766:
3574:
3382:
3190:
2998:
2847:
2696:
2375:
2186:
1997:
1808:
1706:
1614:
1515:
1492:
1450:
1420:
1392:
1366:
1340:
1292:
1272:
1238:
1218:
1168:
786:
764:
742:
688:
629:
595:
566:
501:
477:
193:
5729:. Vol. 131. Springer, Berlin. pp. 52–71.
1205:{\displaystyle {\mathcal {M}}=(S,{\rightarrow },L)}
5667:
5479:
5456:
5240:{\displaystyle E\equiv \psi \lor (\phi \land EXE)}
5239:
5159:{\displaystyle A\equiv \psi \lor (\phi \land AXA)}
5158:
5077:
5026:
4976:{\displaystyle EG\phi \equiv \phi \land EXEG\phi }
4975:
4925:{\displaystyle AG\phi \equiv \phi \land AXAG\phi }
4924:
4864:
4817:
4779:
4753:
4708:
4663:
4609:
4587:
4562:
4520:
4498:
4474:
4448:
4428:
4400:
4371:
4061:
3751:
3559:
3367:
3175:
2983:
2832:
2681:
2360:
2171:
1982:
1793:
1691:
1599:
1498:
1478:
1430:
1398:
1378:
1352:
1326:
1278:
1258:
1224:
1204:
794:
772:
750:
725:
668:
605:
576:
549:
483:
460:
5078:{\displaystyle EF\phi \equiv \phi \lor EXEF\phi }
5027:{\displaystyle AF\phi \equiv \phi \lor AXAF\phi }
4364:
4357:
4223:
4150:
4140:
4079:
4054:
4047:
3913:
3840:
3830:
3769:
3744:
3625:
3615:
3577:
3552:
3433:
3423:
3385:
3360:
3241:
3231:
3193:
3168:
3049:
3039:
3001:
2976:
2898:
2888:
2850:
2825:
2747:
2737:
2699:
2674:
2667:
2559:
2549:
2447:
2440:
2430:
2378:
2353:
2251:
2241:
2189:
2164:
2062:
2052:
2000:
1975:
1873:
1863:
1811:
1786:
1754:
1744:
1709:
1684:
1659:
1649:
1617:
1592:
1560:
1550:
1518:
1327:{\displaystyle {\mathcal {M}}=(S,\rightarrow ,L)}
1259:{\displaystyle {\rightarrow }\subseteq S\times S}
5881:
5851:Handbook of Theoretical Computer Science, vol. B
4875:The important equivalences below are called the
679:The following is not a well-formed CTL formula:
116:, which determine if a given artifact possesses
4754:{\displaystyle \neg AX\phi \equiv EX\neg \phi }
4709:{\displaystyle \neg EF\phi \equiv AG\neg \phi }
4664:{\displaystyle \neg AF\phi \equiv EG\neg \phi }
1479:{\displaystyle ({\mathcal {M}},s\models \phi )}
613:means 'along at least (there Exists) one path'
5844:
5379:
4350:
4286:
4276:
4230:
4040:
3976:
3966:
3920:
3737:
3698:
3545:
3506:
3353:
3314:
3161:
3122:
2969:
2930:
2818:
2779:
2660:
2621:
2608:
2569:
2542:
2503:
2493:
2454:
2346:
2307:
2297:
2258:
2157:
2118:
2108:
2069:
1968:
1929:
1919:
1880:
718:
698:
148:in 1981, who used it to synthesize so-called
4859:
4832:
4812:
4794:
4190:
4158:
3880:
3848:
3665:
3633:
3473:
3441:
3281:
3249:
3089:
3057:
2925:
2906:
2774:
2755:
544:
502:
5559:"Branching vs. Linear Time: Final Showdown"
1023:
4382:
921:has to hold on the entire subsequent path.
850:The temporal operators are the following:
5827:
5790:
5685:
5642:
5399:(LTL) are both a subset of CTL*. CTL and
77:Learn how and when to remove this message
4411:
40:This article includes a list of general
5778:Journal of Computer and System Sciences
14:
5882:
1020:is strictly more expressive than CTL.
1006:operator is sometimes called "unless".
180:for CTL is generated by the following
5556:
845:
736:The problem with this string is that
825:
26:
5489:quantified computational tree logic
1162:. A transition system is a triple
1148:
998:is that there is no guarantee that
758:can occur only when paired with an
24:
5718:E.M. Clarke; E.A. Emerson (1981).
5471:
5448:
4745:
4724:
4700:
4679:
4655:
4634:
4603:
4581:
4557:
4554:
4550:
4543:
4539:
4535:
4514:
4492:
4314:
4291:
4240:
4215:
4155:
4089:
4004:
3981:
3930:
3905:
3845:
3779:
3708:
3690:
3630:
3587:
3516:
3498:
3438:
3395:
3324:
3306:
3246:
3203:
3132:
3114:
3054:
3011:
2940:
2903:
2860:
2789:
2752:
2709:
2631:
2616:
2579:
2564:
2513:
2464:
2388:
2317:
2268:
2199:
2128:
2079:
2010:
1939:
1890:
1821:
1764:
1736:
1719:
1627:
1587:
1570:
1545:
1528:
1456:
1423:
1295:
1171:
1158:CTL formulae are interpreted over
788:
766:
744:
505:
229:
214:
208:
46:it lacks sufficient corresponding
25:
5911:
5868:
5491:(QCTL). There are two semantics:
5395:Computation tree logic (CTL) and
4475:{\displaystyle \phi \equiv \psi }
1334:be such a transition model, with
5853:. MIT Press. pp. 955–1072.
5752:Michael Huth; Mark Ryan (2004).
5410:.P exists in LTL but not in CTL.
167:
31:
5627:"On the Expressiveness of QCTL"
5428:.P exist in CTL but not in LTL.
5390:alternating-time temporal logic
970:will be verified in the future.
320:
5661:
5618:
5550:
5234:
5231:
5219:
5201:
5189:
5177:
5153:
5150:
5138:
5120:
5108:
5096:
4332:
4309:
4306:
4294:
4258:
4235:
4212:
4193:
4184:
4171:
4145:
4135:
4109:
4100:
4084:
4022:
3999:
3996:
3984:
3948:
3925:
3902:
3883:
3874:
3861:
3835:
3825:
3799:
3790:
3774:
3726:
3703:
3687:
3668:
3659:
3646:
3620:
3598:
3582:
3534:
3511:
3495:
3476:
3467:
3454:
3428:
3406:
3390:
3342:
3319:
3303:
3284:
3275:
3262:
3236:
3214:
3198:
3150:
3127:
3111:
3092:
3083:
3070:
3044:
3022:
3006:
2958:
2935:
2912:
2893:
2871:
2855:
2807:
2784:
2761:
2742:
2720:
2704:
2642:
2626:
2590:
2574:
2524:
2508:
2475:
2459:
2435:
2415:
2399:
2383:
2328:
2312:
2279:
2263:
2246:
2226:
2210:
2194:
2139:
2123:
2090:
2074:
2057:
2021:
2005:
1950:
1934:
1901:
1885:
1868:
1832:
1816:
1775:
1759:
1749:
1730:
1714:
1679:
1673:
1654:
1638:
1622:
1581:
1565:
1539:
1523:
1473:
1451:
1441:Then the relation of semantic
1431:{\displaystyle {\mathcal {M}}}
1321:
1312:
1303:
1240:
1199:
1189:
1179:
663:
650:
637:
451:
435:
422:
406:
307:
301:
295:
289:
283:
277:
271:
259:
253:
241:
235:
226:
13:
1:
5644:10.4230/LIPIcs.CONCUR.2016.28
5543:
5533:Fair computational tree logic
5432:
4872:and the boolean connectives.
1153:
118:safety or liveness properties
5801:10.1016/0022-0000(85)90001-7
5670:"From Quantified CTL to QBF"
4865:{\displaystyle \{EG,AF,AU\}}
4610:{\displaystyle \mathrm {F} }
4588:{\displaystyle \mathrm {G} }
4521:{\displaystyle \mathrm {E} }
4499:{\displaystyle \mathrm {A} }
820:
795:{\displaystyle \mathrm {E} }
773:{\displaystyle \mathrm {A} }
751:{\displaystyle \mathrm {U} }
100:, meaning that its model of
7:
5687:10.4230/LIPIcs.TIME.2019.11
5521:
5437:CTL has been extended with
5380:Relations with other logics
5250:
1002:will ever be verified. The
994:holds. The difference with
10:
5916:
4624:can be formulated in CTL:
1486:is defined recursively on
1379:{\displaystyle \phi \in F}
879:Path-specific quantifiers
606:{\displaystyle {\mbox{E}}}
577:{\displaystyle {\mbox{A}}}
140:CTL was first proposed by
135:
5890:Logic in computer science
5754:Logic in Computer Science
5480:{\displaystyle \forall p}
5457:{\displaystyle \exists p}
4818:{\displaystyle \{AX,EX\}}
966:holds. This implies that
150:synchronisation skeletons
5557:Vardi, Moshe Y. (2001).
1024:Minimal set of operators
584:means 'along All paths'
18:Computational tree logic
5570:10.1007/3-540-45319-9_1
4383:Characterisation of CTL
962:until at some position
854:Quantifiers over paths
61:more precise citations.
5900:Automata (computation)
5875:Teaching slides of CTL
5510:but satisfiability is
5481:
5458:
5241:
5160:
5079:
5028:
4977:
4926:
4866:
4819:
4781:
4755:
4710:
4665:
4611:
4589:
4564:
4522:
4500:
4476:
4450:
4430:
4402:
4373:
4063:
3753:
3561:
3369:
3177:
2985:
2834:
2683:
2362:
2173:
1984:
1795:
1693:
1601:
1500:
1480:
1432:
1400:
1380:
1354:
1353:{\displaystyle s\in S}
1328:
1280:
1260:
1226:
1206:
796:
774:
752:
727:
670:
607:
578:
551:
485:
462:
96:) is a branching-time
90:Computation tree logic
5538:Linear temporal logic
5482:
5459:
5397:linear temporal logic
5242:
5161:
5080:
5029:
4978:
4927:
4867:
4820:
4782:
4756:
4711:
4666:
4620:Hence an instance of
4612:
4590:
4565:
4523:
4501:
4477:
4451:
4449:{\displaystyle \psi }
4431:
4429:{\displaystyle \phi }
4412:Semantic equivalences
4403:
4374:
4064:
3754:
3562:
3370:
3178:
2986:
2835:
2684:
2363:
2174:
1985:
1796:
1694:
1602:
1501:
1499:{\displaystyle \phi }
1481:
1433:
1401:
1381:
1355:
1329:
1281:
1261:
1227:
1207:
797:
775:
753:
728:
671:
608:
579:
552:
491:ranges over a set of
486:
463:
126:linear temporal logic
5506:. Model checking is
5468:
5445:
5171:
5090:
5039:
4988:
4937:
4886:
4829:
4825:and at least one of
4791:
4768:
4721:
4676:
4631:
4599:
4577:
4573:Furthermore, so are
4532:
4510:
4488:
4484:It can be seen that
4460:
4440:
4420:
4392:
4074:
3764:
3572:
3380:
3188:
2996:
2845:
2694:
2373:
2184:
1995:
1806:
1704:
1612:
1513:
1490:
1448:
1418:
1408:well-formed formulas
1390:
1364:
1338:
1290:
1270:
1236:
1232:is a set of states,
1216:
1166:
870:Φ –
860:Φ –
784:
762:
740:
686:
627:
593:
564:
499:
475:
191:
178:well-formed formulas
807:atomic propositions
158:concurrent programs
110:formal verification
5735:10.1007/BFb0025774
5477:
5454:
5237:
5156:
5075:
5024:
4973:
4922:
4862:
4815:
4787:, at least one of
4780:{\displaystyle EU}
4777:
4751:
4706:
4661:
4607:
4585:
4560:
4518:
4496:
4472:
4446:
4426:
4398:
4369:
4059:
3749:
3557:
3365:
3173:
2981:
2830:
2679:
2358:
2169:
1980:
1791:
1689:
1597:
1496:
1476:
1428:
1396:
1376:
1350:
1324:
1276:
1256:
1222:
1202:
1160:transition systems
990:has to hold until
846:Temporal operators
815:temporal operators
792:
770:
748:
723:
711:
694:
666:
658:
645:
635:
603:
601:
574:
572:
547:
542:
532:
522:
481:
458:
456:
446:
433:
417:
404:
391:
378:
365:
352:
339:
326:
5860:978-0-262-22039-2
5829:10.1145/5397.5399
5763:978-0-521-54310-1
5697:978-3-95977-127-6
5654:978-3-95977-017-0
5606:Missing or empty
5579:978-3-540-41865-8
5528:Probabilistic CTL
4401:{\displaystyle s}
1399:{\displaystyle F}
1279:{\displaystyle L}
1225:{\displaystyle S}
832:logical operators
826:Logical operators
811:logical operators
710:
693:
657:
644:
634:
600:
571:
541:
531:
521:
484:{\displaystyle p}
445:
432:
416:
403:
390:
377:
364:
351:
338:
325:
87:
86:
79:
16:(Redirected from
5907:
5864:
5841:
5831:
5804:
5794:
5771:Emerson, E. A.;
5767:
5748:
5724:
5710:
5709:
5689:
5665:
5659:
5658:
5646:
5622:
5616:
5615:
5609:
5603:
5597:
5593:
5591:
5583:
5563:
5554:
5486:
5484:
5483:
5478:
5463:
5461:
5460:
5455:
5386:modal μ calculus
5246:
5244:
5243:
5238:
5165:
5163:
5162:
5157:
5084:
5082:
5081:
5076:
5033:
5031:
5030:
5025:
4982:
4980:
4979:
4974:
4931:
4929:
4928:
4923:
4871:
4869:
4868:
4863:
4824:
4822:
4821:
4816:
4786:
4784:
4783:
4778:
4760:
4758:
4757:
4752:
4715:
4713:
4712:
4707:
4670:
4668:
4667:
4662:
4622:De Morgan's laws
4616:
4614:
4613:
4608:
4606:
4594:
4592:
4591:
4586:
4584:
4569:
4567:
4566:
4561:
4553:
4542:
4527:
4525:
4524:
4519:
4517:
4505:
4503:
4502:
4497:
4495:
4481:
4479:
4478:
4473:
4455:
4453:
4452:
4447:
4435:
4433:
4432:
4427:
4407:
4405:
4404:
4399:
4378:
4376:
4375:
4370:
4368:
4367:
4361:
4360:
4354:
4353:
4347:
4346:
4331:
4330:
4318:
4317:
4290:
4289:
4280:
4279:
4273:
4272:
4257:
4256:
4244:
4243:
4234:
4233:
4227:
4226:
4211:
4210:
4183:
4182:
4170:
4169:
4154:
4153:
4144:
4143:
4134:
4133:
4121:
4120:
4093:
4092:
4083:
4082:
4068:
4066:
4065:
4060:
4058:
4057:
4051:
4050:
4044:
4043:
4037:
4036:
4021:
4020:
4008:
4007:
3980:
3979:
3970:
3969:
3963:
3962:
3947:
3946:
3934:
3933:
3924:
3923:
3917:
3916:
3901:
3900:
3873:
3872:
3860:
3859:
3844:
3843:
3834:
3833:
3824:
3823:
3811:
3810:
3783:
3782:
3773:
3772:
3758:
3756:
3755:
3750:
3748:
3747:
3741:
3740:
3725:
3724:
3712:
3711:
3702:
3701:
3686:
3685:
3658:
3657:
3645:
3644:
3629:
3628:
3619:
3618:
3591:
3590:
3581:
3580:
3566:
3564:
3563:
3558:
3556:
3555:
3549:
3548:
3533:
3532:
3520:
3519:
3510:
3509:
3494:
3493:
3466:
3465:
3453:
3452:
3437:
3436:
3427:
3426:
3399:
3398:
3389:
3388:
3374:
3372:
3371:
3366:
3364:
3363:
3357:
3356:
3341:
3340:
3328:
3327:
3318:
3317:
3302:
3301:
3274:
3273:
3261:
3260:
3245:
3244:
3235:
3234:
3207:
3206:
3197:
3196:
3182:
3180:
3179:
3174:
3172:
3171:
3165:
3164:
3149:
3148:
3136:
3135:
3126:
3125:
3110:
3109:
3082:
3081:
3069:
3068:
3053:
3052:
3043:
3042:
3015:
3014:
3005:
3004:
2990:
2988:
2987:
2982:
2980:
2979:
2973:
2972:
2957:
2956:
2944:
2943:
2934:
2933:
2924:
2923:
2902:
2901:
2892:
2891:
2864:
2863:
2854:
2853:
2839:
2837:
2836:
2831:
2829:
2828:
2822:
2821:
2806:
2805:
2793:
2792:
2783:
2782:
2773:
2772:
2751:
2750:
2741:
2740:
2713:
2712:
2703:
2702:
2688:
2686:
2685:
2680:
2678:
2677:
2671:
2670:
2664:
2663:
2657:
2656:
2635:
2634:
2625:
2624:
2612:
2611:
2605:
2604:
2583:
2582:
2573:
2572:
2563:
2562:
2553:
2552:
2546:
2545:
2539:
2538:
2517:
2516:
2507:
2506:
2497:
2496:
2490:
2489:
2468:
2467:
2458:
2457:
2451:
2450:
2444:
2443:
2434:
2433:
2427:
2426:
2414:
2413:
2392:
2391:
2382:
2381:
2367:
2365:
2364:
2359:
2357:
2356:
2350:
2349:
2343:
2342:
2321:
2320:
2311:
2310:
2301:
2300:
2294:
2293:
2272:
2271:
2262:
2261:
2255:
2254:
2245:
2244:
2238:
2237:
2225:
2224:
2203:
2202:
2193:
2192:
2178:
2176:
2175:
2170:
2168:
2167:
2161:
2160:
2154:
2153:
2132:
2131:
2122:
2121:
2112:
2111:
2105:
2104:
2083:
2082:
2073:
2072:
2066:
2065:
2056:
2055:
2049:
2048:
2036:
2035:
2014:
2013:
2004:
2003:
1989:
1987:
1986:
1981:
1979:
1978:
1972:
1971:
1965:
1964:
1943:
1942:
1933:
1932:
1923:
1922:
1916:
1915:
1894:
1893:
1884:
1883:
1877:
1876:
1867:
1866:
1860:
1859:
1847:
1846:
1825:
1824:
1815:
1814:
1800:
1798:
1797:
1792:
1790:
1789:
1768:
1767:
1758:
1757:
1748:
1747:
1723:
1722:
1713:
1712:
1698:
1696:
1695:
1690:
1688:
1687:
1663:
1662:
1653:
1652:
1631:
1630:
1621:
1620:
1606:
1604:
1603:
1598:
1596:
1595:
1574:
1573:
1564:
1563:
1554:
1553:
1532:
1531:
1522:
1521:
1505:
1503:
1502:
1497:
1485:
1483:
1482:
1477:
1460:
1459:
1437:
1435:
1434:
1429:
1427:
1426:
1405:
1403:
1402:
1397:
1385:
1383:
1382:
1377:
1359:
1357:
1356:
1351:
1333:
1331:
1330:
1325:
1299:
1298:
1285:
1283:
1282:
1277:
1265:
1263:
1262:
1257:
1243:
1231:
1229:
1228:
1223:
1211:
1209:
1208:
1203:
1192:
1175:
1174:
1149:Semantics of CTL
888: – Ne
801:
799:
798:
793:
791:
779:
777:
776:
771:
769:
757:
755:
754:
749:
747:
732:
730:
729:
724:
722:
721:
712:
708:
702:
701:
695:
691:
675:
673:
672:
667:
659:
655:
646:
642:
636:
632:
612:
610:
609:
604:
602:
598:
583:
581:
580:
575:
573:
569:
556:
554:
553:
548:
543:
539:
533:
529:
523:
519:
490:
488:
487:
482:
467:
465:
464:
459:
457:
447:
443:
434:
430:
418:
414:
405:
401:
392:
388:
379:
375:
366:
362:
353:
349:
340:
336:
327:
323:
313:
156:abstractions of
146:E. Allen Emerson
142:Edmund M. Clarke
82:
75:
71:
68:
62:
57:this article by
48:inline citations
35:
34:
27:
21:
5915:
5914:
5910:
5909:
5908:
5906:
5905:
5904:
5880:
5879:
5871:
5861:
5847:Jan van Leeuwen
5792:10.1.1.221.6187
5764:
5745:
5722:
5714:
5713:
5698:
5666:
5662:
5655:
5623:
5619:
5607:
5605:
5595:
5594:
5585:
5584:
5580:
5561:
5555:
5551:
5546:
5524:
5508:PSPACE-complete
5469:
5466:
5465:
5446:
5443:
5442:
5441:quantification
5435:
5382:
5253:
5172:
5169:
5168:
5091:
5088:
5087:
5040:
5037:
5036:
4989:
4986:
4985:
4938:
4935:
4934:
4887:
4884:
4883:
4830:
4827:
4826:
4792:
4789:
4788:
4769:
4766:
4765:
4722:
4719:
4718:
4677:
4674:
4673:
4632:
4629:
4628:
4602:
4600:
4597:
4596:
4580:
4578:
4575:
4574:
4549:
4538:
4533:
4530:
4529:
4513:
4511:
4508:
4507:
4491:
4489:
4486:
4485:
4461:
4458:
4457:
4441:
4438:
4437:
4421:
4418:
4417:
4414:
4393:
4390:
4389:
4385:
4363:
4362:
4356:
4355:
4349:
4348:
4342:
4338:
4326:
4322:
4313:
4312:
4285:
4284:
4275:
4274:
4268:
4264:
4252:
4248:
4239:
4238:
4229:
4228:
4222:
4221:
4206:
4202:
4178:
4174:
4165:
4161:
4149:
4148:
4139:
4138:
4129:
4125:
4116:
4112:
4088:
4087:
4078:
4077:
4075:
4072:
4071:
4053:
4052:
4046:
4045:
4039:
4038:
4032:
4028:
4016:
4012:
4003:
4002:
3975:
3974:
3965:
3964:
3958:
3954:
3942:
3938:
3929:
3928:
3919:
3918:
3912:
3911:
3896:
3892:
3868:
3864:
3855:
3851:
3839:
3838:
3829:
3828:
3819:
3815:
3806:
3802:
3778:
3777:
3768:
3767:
3765:
3762:
3761:
3743:
3742:
3736:
3735:
3720:
3716:
3707:
3706:
3697:
3696:
3681:
3677:
3653:
3649:
3640:
3636:
3624:
3623:
3614:
3613:
3586:
3585:
3576:
3575:
3573:
3570:
3569:
3551:
3550:
3544:
3543:
3528:
3524:
3515:
3514:
3505:
3504:
3489:
3485:
3461:
3457:
3448:
3444:
3432:
3431:
3422:
3421:
3394:
3393:
3384:
3383:
3381:
3378:
3377:
3359:
3358:
3352:
3351:
3336:
3332:
3323:
3322:
3313:
3312:
3297:
3293:
3269:
3265:
3256:
3252:
3240:
3239:
3230:
3229:
3202:
3201:
3192:
3191:
3189:
3186:
3185:
3167:
3166:
3160:
3159:
3144:
3140:
3131:
3130:
3121:
3120:
3105:
3101:
3077:
3073:
3064:
3060:
3048:
3047:
3038:
3037:
3010:
3009:
3000:
2999:
2997:
2994:
2993:
2975:
2974:
2968:
2967:
2952:
2948:
2939:
2938:
2929:
2928:
2919:
2915:
2897:
2896:
2887:
2886:
2859:
2858:
2849:
2848:
2846:
2843:
2842:
2824:
2823:
2817:
2816:
2801:
2797:
2788:
2787:
2778:
2777:
2768:
2764:
2746:
2745:
2736:
2735:
2708:
2707:
2698:
2697:
2695:
2692:
2691:
2673:
2672:
2666:
2665:
2659:
2658:
2652:
2648:
2630:
2629:
2620:
2619:
2607:
2606:
2600:
2596:
2578:
2577:
2568:
2567:
2558:
2557:
2548:
2547:
2541:
2540:
2534:
2530:
2512:
2511:
2502:
2501:
2492:
2491:
2485:
2481:
2463:
2462:
2453:
2452:
2446:
2445:
2439:
2438:
2429:
2428:
2422:
2418:
2409:
2405:
2387:
2386:
2377:
2376:
2374:
2371:
2370:
2352:
2351:
2345:
2344:
2338:
2334:
2316:
2315:
2306:
2305:
2296:
2295:
2289:
2285:
2267:
2266:
2257:
2256:
2250:
2249:
2240:
2239:
2233:
2229:
2220:
2216:
2198:
2197:
2188:
2187:
2185:
2182:
2181:
2163:
2162:
2156:
2155:
2149:
2145:
2127:
2126:
2117:
2116:
2107:
2106:
2100:
2096:
2078:
2077:
2068:
2067:
2061:
2060:
2051:
2050:
2044:
2040:
2031:
2027:
2009:
2008:
1999:
1998:
1996:
1993:
1992:
1974:
1973:
1967:
1966:
1960:
1956:
1938:
1937:
1928:
1927:
1918:
1917:
1911:
1907:
1889:
1888:
1879:
1878:
1872:
1871:
1862:
1861:
1855:
1851:
1842:
1838:
1820:
1819:
1810:
1809:
1807:
1804:
1803:
1785:
1784:
1763:
1762:
1753:
1752:
1743:
1742:
1718:
1717:
1708:
1707:
1705:
1702:
1701:
1683:
1682:
1658:
1657:
1648:
1647:
1626:
1625:
1616:
1615:
1613:
1610:
1609:
1591:
1590:
1569:
1568:
1559:
1558:
1549:
1548:
1527:
1526:
1517:
1516:
1514:
1511:
1510:
1491:
1488:
1487:
1455:
1454:
1449:
1446:
1445:
1422:
1421:
1419:
1416:
1415:
1391:
1388:
1387:
1365:
1362:
1361:
1339:
1336:
1335:
1294:
1293:
1291:
1288:
1287:
1271:
1268:
1267:
1239:
1237:
1234:
1233:
1217:
1214:
1213:
1188:
1170:
1169:
1167:
1164:
1163:
1156:
1151:
1026:
848:
828:
823:
787:
785:
782:
781:
765:
763:
760:
759:
743:
741:
738:
737:
717:
716:
706:
697:
696:
689:
687:
684:
683:
653:
640:
630:
628:
625:
624:
596:
594:
591:
590:
567:
565:
562:
561:
537:
527:
517:
500:
497:
496:
493:atomic formulas
476:
473:
472:
455:
454:
441:
428:
412:
399:
386:
373:
360:
347:
334:
321:
311:
310:
201:
194:
192:
189:
188:
170:
138:
122:temporal logics
83:
72:
66:
63:
53:Please help to
52:
36:
32:
23:
22:
15:
12:
11:
5:
5913:
5903:
5902:
5897:
5895:Temporal logic
5892:
5878:
5877:
5870:
5869:External links
5867:
5866:
5865:
5859:
5842:
5822:(2): 244–263.
5805:
5773:Halpern, J. Y.
5768:
5762:
5749:
5743:
5712:
5711:
5696:
5660:
5653:
5617:
5596:|journal=
5578:
5548:
5547:
5545:
5542:
5541:
5540:
5535:
5530:
5523:
5520:
5516:
5515:
5500:
5476:
5473:
5453:
5450:
5434:
5431:
5430:
5429:
5411:
5381:
5378:
5377:
5376:
5368:
5367:
5348:
5347:
5343:
5342:
5320:
5319:
5315:
5314:
5303:
5302:
5294:
5293:
5282:
5281:
5277:
5276:
5269:
5268:
5264:
5263:
5252:
5249:
5248:
5247:
5236:
5233:
5230:
5227:
5224:
5221:
5218:
5215:
5212:
5209:
5206:
5203:
5200:
5197:
5194:
5191:
5188:
5185:
5182:
5179:
5176:
5166:
5155:
5152:
5149:
5146:
5143:
5140:
5137:
5134:
5131:
5128:
5125:
5122:
5119:
5116:
5113:
5110:
5107:
5104:
5101:
5098:
5095:
5085:
5074:
5071:
5068:
5065:
5062:
5059:
5056:
5053:
5050:
5047:
5044:
5034:
5023:
5020:
5017:
5014:
5011:
5008:
5005:
5002:
4999:
4996:
4993:
4983:
4972:
4969:
4966:
4963:
4960:
4957:
4954:
4951:
4948:
4945:
4942:
4932:
4921:
4918:
4915:
4912:
4909:
4906:
4903:
4900:
4897:
4894:
4891:
4877:expansion laws
4861:
4858:
4855:
4852:
4849:
4846:
4843:
4840:
4837:
4834:
4814:
4811:
4808:
4805:
4802:
4799:
4796:
4776:
4773:
4762:
4761:
4750:
4747:
4744:
4741:
4738:
4735:
4732:
4729:
4726:
4716:
4705:
4702:
4699:
4696:
4693:
4690:
4687:
4684:
4681:
4671:
4660:
4657:
4654:
4651:
4648:
4645:
4642:
4639:
4636:
4605:
4583:
4559:
4556:
4552:
4548:
4545:
4541:
4537:
4516:
4494:
4471:
4468:
4465:
4445:
4425:
4413:
4410:
4397:
4384:
4381:
4380:
4379:
4366:
4359:
4352:
4345:
4341:
4337:
4334:
4329:
4325:
4321:
4316:
4311:
4308:
4305:
4302:
4299:
4296:
4293:
4288:
4283:
4278:
4271:
4267:
4263:
4260:
4255:
4251:
4247:
4242:
4237:
4232:
4225:
4220:
4217:
4214:
4209:
4205:
4201:
4198:
4195:
4192:
4189:
4186:
4181:
4177:
4173:
4168:
4164:
4160:
4157:
4152:
4147:
4142:
4137:
4132:
4128:
4124:
4119:
4115:
4111:
4108:
4105:
4102:
4099:
4096:
4091:
4086:
4081:
4069:
4056:
4049:
4042:
4035:
4031:
4027:
4024:
4019:
4015:
4011:
4006:
4001:
3998:
3995:
3992:
3989:
3986:
3983:
3978:
3973:
3968:
3961:
3957:
3953:
3950:
3945:
3941:
3937:
3932:
3927:
3922:
3915:
3910:
3907:
3904:
3899:
3895:
3891:
3888:
3885:
3882:
3879:
3876:
3871:
3867:
3863:
3858:
3854:
3850:
3847:
3842:
3837:
3832:
3827:
3822:
3818:
3814:
3809:
3805:
3801:
3798:
3795:
3792:
3789:
3786:
3781:
3776:
3771:
3759:
3746:
3739:
3734:
3731:
3728:
3723:
3719:
3715:
3710:
3705:
3700:
3695:
3692:
3689:
3684:
3680:
3676:
3673:
3670:
3667:
3664:
3661:
3656:
3652:
3648:
3643:
3639:
3635:
3632:
3627:
3622:
3617:
3612:
3609:
3606:
3603:
3600:
3597:
3594:
3589:
3584:
3579:
3567:
3554:
3547:
3542:
3539:
3536:
3531:
3527:
3523:
3518:
3513:
3508:
3503:
3500:
3497:
3492:
3488:
3484:
3481:
3478:
3475:
3472:
3469:
3464:
3460:
3456:
3451:
3447:
3443:
3440:
3435:
3430:
3425:
3420:
3417:
3414:
3411:
3408:
3405:
3402:
3397:
3392:
3387:
3375:
3362:
3355:
3350:
3347:
3344:
3339:
3335:
3331:
3326:
3321:
3316:
3311:
3308:
3305:
3300:
3296:
3292:
3289:
3286:
3283:
3280:
3277:
3272:
3268:
3264:
3259:
3255:
3251:
3248:
3243:
3238:
3233:
3228:
3225:
3222:
3219:
3216:
3213:
3210:
3205:
3200:
3195:
3183:
3170:
3163:
3158:
3155:
3152:
3147:
3143:
3139:
3134:
3129:
3124:
3119:
3116:
3113:
3108:
3104:
3100:
3097:
3094:
3091:
3088:
3085:
3080:
3076:
3072:
3067:
3063:
3059:
3056:
3051:
3046:
3041:
3036:
3033:
3030:
3027:
3024:
3021:
3018:
3013:
3008:
3003:
2991:
2978:
2971:
2966:
2963:
2960:
2955:
2951:
2947:
2942:
2937:
2932:
2927:
2922:
2918:
2914:
2911:
2908:
2905:
2900:
2895:
2890:
2885:
2882:
2879:
2876:
2873:
2870:
2867:
2862:
2857:
2852:
2840:
2827:
2820:
2815:
2812:
2809:
2804:
2800:
2796:
2791:
2786:
2781:
2776:
2771:
2767:
2763:
2760:
2757:
2754:
2749:
2744:
2739:
2734:
2731:
2728:
2725:
2722:
2719:
2716:
2711:
2706:
2701:
2689:
2676:
2669:
2662:
2655:
2651:
2647:
2644:
2641:
2638:
2633:
2628:
2623:
2618:
2615:
2610:
2603:
2599:
2595:
2592:
2589:
2586:
2581:
2576:
2571:
2566:
2561:
2556:
2551:
2544:
2537:
2533:
2529:
2526:
2523:
2520:
2515:
2510:
2505:
2500:
2495:
2488:
2484:
2480:
2477:
2474:
2471:
2466:
2461:
2456:
2449:
2442:
2437:
2432:
2425:
2421:
2417:
2412:
2408:
2404:
2401:
2398:
2395:
2390:
2385:
2380:
2368:
2355:
2348:
2341:
2337:
2333:
2330:
2327:
2324:
2319:
2314:
2309:
2304:
2299:
2292:
2288:
2284:
2281:
2278:
2275:
2270:
2265:
2260:
2253:
2248:
2243:
2236:
2232:
2228:
2223:
2219:
2215:
2212:
2209:
2206:
2201:
2196:
2191:
2179:
2166:
2159:
2152:
2148:
2144:
2141:
2138:
2135:
2130:
2125:
2120:
2115:
2110:
2103:
2099:
2095:
2092:
2089:
2086:
2081:
2076:
2071:
2064:
2059:
2054:
2047:
2043:
2039:
2034:
2030:
2026:
2023:
2020:
2017:
2012:
2007:
2002:
1990:
1977:
1970:
1963:
1959:
1955:
1952:
1949:
1946:
1941:
1936:
1931:
1926:
1921:
1914:
1910:
1906:
1903:
1900:
1897:
1892:
1887:
1882:
1875:
1870:
1865:
1858:
1854:
1850:
1845:
1841:
1837:
1834:
1831:
1828:
1823:
1818:
1813:
1801:
1788:
1783:
1780:
1777:
1774:
1771:
1766:
1761:
1756:
1751:
1746:
1741:
1738:
1735:
1732:
1729:
1726:
1721:
1716:
1711:
1699:
1686:
1681:
1678:
1675:
1672:
1669:
1666:
1661:
1656:
1651:
1646:
1643:
1640:
1637:
1634:
1629:
1624:
1619:
1607:
1594:
1589:
1586:
1583:
1580:
1577:
1572:
1567:
1562:
1557:
1552:
1547:
1544:
1541:
1538:
1535:
1530:
1525:
1520:
1495:
1475:
1472:
1469:
1466:
1463:
1458:
1453:
1425:
1406:is the set of
1395:
1375:
1372:
1369:
1349:
1346:
1343:
1323:
1320:
1317:
1314:
1311:
1308:
1305:
1302:
1297:
1275:
1255:
1252:
1249:
1246:
1242:
1221:
1201:
1198:
1195:
1191:
1187:
1184:
1181:
1178:
1173:
1155:
1152:
1150:
1147:
1146:
1145:
1127:
1106:
1086:
1069:
1030:model checking
1025:
1022:
1010:
1009:
1008:
1007:
982: –
971:
950: –
939:
930: –
922:
913: –
905:
877:
876:
875:
865:
847:
844:
827:
824:
822:
819:
790:
768:
746:
734:
733:
720:
715:
705:
700:
677:
676:
665:
662:
652:
649:
639:
618:
617:
588:
546:
536:
526:
516:
513:
510:
507:
504:
480:
469:
468:
453:
450:
440:
437:
427:
424:
421:
411:
408:
398:
395:
385:
382:
372:
369:
359:
356:
346:
343:
333:
330:
319:
316:
314:
312:
309:
306:
303:
300:
297:
294:
291:
288:
285:
282:
279:
276:
273:
270:
267:
264:
261:
258:
255:
252:
249:
246:
243:
240:
237:
234:
231:
228:
225:
222:
219:
216:
213:
210:
207:
204:
202:
200:
197:
196:
169:
166:
137:
134:
124:that includes
114:model checkers
85:
84:
39:
37:
30:
9:
6:
4:
3:
2:
5912:
5901:
5898:
5896:
5893:
5891:
5888:
5887:
5885:
5876:
5873:
5872:
5862:
5856:
5852:
5848:
5843:
5839:
5835:
5830:
5825:
5821:
5817:
5816:
5811:
5806:
5802:
5798:
5793:
5788:
5784:
5780:
5779:
5774:
5769:
5765:
5759:
5755:
5750:
5746:
5744:3-540-11212-X
5740:
5736:
5732:
5728:
5721:
5716:
5715:
5707:
5703:
5699:
5693:
5688:
5683:
5679:
5675:
5671:
5664:
5656:
5650:
5645:
5640:
5636:
5632:
5628:
5621:
5613:
5601:
5589:
5581:
5575:
5571:
5567:
5560:
5553:
5549:
5539:
5536:
5534:
5531:
5529:
5526:
5525:
5519:
5513:
5509:
5505:
5501:
5498:
5494:
5493:
5492:
5490:
5474:
5451:
5440:
5427:
5423:
5419:
5415:
5412:
5409:
5406:
5405:
5404:
5402:
5398:
5393:
5391:
5387:
5374:
5370:
5369:
5365:
5361:
5357:
5353:
5350:
5349:
5345:
5344:
5340:
5336:
5333:
5332:
5331:
5329:
5325:
5317:
5316:
5312:
5308:
5305:
5304:
5301:is infinite).
5300:
5296:
5295:
5291:
5287:
5284:
5283:
5279:
5278:
5274:
5271:
5270:
5266:
5265:
5261:
5258:
5257:
5256:
5228:
5225:
5222:
5216:
5213:
5210:
5207:
5204:
5198:
5195:
5192:
5186:
5183:
5180:
5174:
5167:
5147:
5144:
5141:
5135:
5132:
5129:
5126:
5123:
5117:
5114:
5111:
5105:
5102:
5099:
5093:
5086:
5072:
5069:
5066:
5063:
5060:
5057:
5054:
5051:
5048:
5045:
5042:
5035:
5021:
5018:
5015:
5012:
5009:
5006:
5003:
5000:
4997:
4994:
4991:
4984:
4970:
4967:
4964:
4961:
4958:
4955:
4952:
4949:
4946:
4943:
4940:
4933:
4919:
4916:
4913:
4910:
4907:
4904:
4901:
4898:
4895:
4892:
4889:
4882:
4881:
4880:
4878:
4873:
4856:
4853:
4850:
4847:
4844:
4841:
4838:
4835:
4809:
4806:
4803:
4800:
4797:
4774:
4771:
4748:
4742:
4739:
4736:
4733:
4730:
4727:
4717:
4703:
4697:
4694:
4691:
4688:
4685:
4682:
4672:
4658:
4652:
4649:
4646:
4643:
4640:
4637:
4627:
4626:
4625:
4623:
4618:
4571:
4546:
4482:
4469:
4466:
4463:
4443:
4423:
4416:The formulae
4409:
4395:
4343:
4339:
4335:
4327:
4323:
4319:
4303:
4300:
4297:
4281:
4269:
4265:
4261:
4253:
4249:
4245:
4218:
4207:
4203:
4199:
4196:
4187:
4179:
4175:
4166:
4162:
4130:
4126:
4122:
4117:
4113:
4106:
4103:
4097:
4094:
4070:
4033:
4029:
4025:
4017:
4013:
4009:
3993:
3990:
3987:
3971:
3959:
3955:
3951:
3943:
3939:
3935:
3908:
3897:
3893:
3889:
3886:
3877:
3869:
3865:
3856:
3852:
3820:
3816:
3812:
3807:
3803:
3796:
3793:
3787:
3784:
3760:
3732:
3729:
3721:
3717:
3713:
3693:
3682:
3678:
3674:
3671:
3662:
3654:
3650:
3641:
3637:
3610:
3607:
3604:
3601:
3595:
3592:
3568:
3540:
3537:
3529:
3525:
3521:
3501:
3490:
3486:
3482:
3479:
3470:
3462:
3458:
3449:
3445:
3418:
3415:
3412:
3409:
3403:
3400:
3376:
3348:
3345:
3337:
3333:
3329:
3309:
3298:
3294:
3290:
3287:
3278:
3270:
3266:
3257:
3253:
3226:
3223:
3220:
3217:
3211:
3208:
3184:
3156:
3153:
3145:
3141:
3137:
3117:
3106:
3102:
3098:
3095:
3086:
3078:
3074:
3065:
3061:
3034:
3031:
3028:
3025:
3019:
3016:
2992:
2964:
2961:
2953:
2949:
2945:
2920:
2916:
2909:
2883:
2880:
2877:
2874:
2868:
2865:
2841:
2813:
2810:
2802:
2798:
2794:
2769:
2765:
2758:
2732:
2729:
2726:
2723:
2717:
2714:
2690:
2653:
2649:
2645:
2639:
2636:
2613:
2601:
2597:
2593:
2587:
2584:
2554:
2535:
2531:
2527:
2521:
2518:
2498:
2486:
2482:
2478:
2472:
2469:
2423:
2419:
2410:
2406:
2402:
2396:
2393:
2369:
2339:
2335:
2331:
2325:
2322:
2302:
2290:
2286:
2282:
2276:
2273:
2234:
2230:
2221:
2217:
2213:
2207:
2204:
2180:
2150:
2146:
2142:
2136:
2133:
2113:
2101:
2097:
2093:
2087:
2084:
2045:
2041:
2037:
2032:
2028:
2024:
2018:
2015:
1991:
1961:
1957:
1953:
1947:
1944:
1924:
1912:
1908:
1904:
1898:
1895:
1856:
1852:
1848:
1843:
1839:
1835:
1829:
1826:
1802:
1781:
1778:
1772:
1769:
1739:
1733:
1727:
1724:
1700:
1676:
1670:
1667:
1664:
1644:
1641:
1635:
1632:
1608:
1584:
1578:
1575:
1555:
1542:
1536:
1533:
1509:
1508:
1507:
1493:
1470:
1467:
1464:
1461:
1444:
1439:
1413:
1409:
1393:
1373:
1370:
1367:
1347:
1344:
1341:
1318:
1315:
1309:
1306:
1300:
1273:
1253:
1250:
1247:
1244:
1219:
1196:
1193:
1185:
1182:
1176:
1161:
1143:
1139:
1135:
1131:
1128:
1125:
1121:
1117:
1113:
1110:
1107:
1105:
1101:
1097:
1093:
1090:
1087:
1084:
1080:
1076:
1073:
1070:
1067:
1064:
1060:
1056:
1053:
1050:
1049:
1048:
1045:
1043:
1039:
1035:
1031:
1021:
1019:
1015:
1005:
1001:
997:
993:
989:
985:
981:
978:
975:
972:
969:
965:
961:
957:
953:
949:
946:
943:
940:
937:
933:
929:
926:
923:
920:
916:
912:
909:
906:
903:
899:
895:
891:
887:
884:
881:
880:
878:
873:
869:
866:
863:
859:
856:
855:
853:
852:
851:
843:
841:
837:
833:
818:
816:
812:
808:
803:
713:
709: U
703:
682:
681:
680:
660:
647:
623:
622:
621:
616:
589:
587:
560:
559:
558:
534:
524:
514:
511:
508:
494:
478:
448:
444: U
438:
425:
419:
415: U
409:
396:
393:
383:
380:
370:
367:
357:
354:
344:
341:
331:
328:
317:
315:
304:
298:
292:
286:
280:
274:
268:
265:
262:
256:
250:
247:
244:
238:
232:
223:
220:
217:
211:
205:
203:
198:
187:
186:
185:
183:
179:
175:
168:Syntax of CTL
165:
161:
159:
155:
151:
147:
143:
133:
131:
127:
123:
119:
115:
111:
107:
103:
99:
95:
91:
81:
78:
70:
60:
56:
50:
49:
43:
38:
29:
28:
19:
5850:
5819:
5813:
5782:
5776:
5753:
5726:
5677:
5673:
5663:
5634:
5630:
5620:
5608:|title=
5552:
5517:
5488:
5439:second-order
5436:
5425:
5421:
5417:
5413:
5407:
5394:
5383:
5372:
5363:
5359:
5355:
5351:
5338:
5334:
5327:
5323:
5321:
5310:
5306:
5298:
5289:
5285:
5272:
5259:
5254:
4876:
4874:
4763:
4619:
4572:
4483:
4415:
4386:
1440:
1157:
1141:
1137:
1133:
1129:
1123:
1119:
1115:
1111:
1108:
1103:
1099:
1095:
1091:
1088:
1082:
1078:
1074:
1071:
1065:
1062:
1058:
1054:
1051:
1046:
1041:
1037:
1033:
1027:
1011:
1003:
999:
995:
991:
987:
983:
979:
976:
973:
967:
963:
959:
958:has to hold
955:
951:
947:
944:
941:
935:
931:
927:
924:
918:
914:
910:
907:
901:
897:
893:
889:
885:
882:
871:
867:
861:
857:
849:
829:
804:
735:
678:
619:
614:
586:(inevitably)
585:
470:
171:
162:
153:
149:
139:
93:
89:
88:
73:
67:October 2015
64:
45:
5785:(1): 1–24.
5512:undecidable
5420:.Q)∧(
986:eak until:
900:instead of
59:introducing
5884:Categories
5544:References
5433:Extensions
5424:¬Q))) and
1443:entailment
1154:Definition
1061:( because
615:(possibly)
42:references
5787:CiteSeerX
5706:195345645
5598:ignored (
5588:cite book
5472:∀
5449:∃
5229:ψ
5223:ϕ
5208:∧
5205:ϕ
5199:∨
5196:ψ
5193:≡
5187:ψ
5181:ϕ
5148:ψ
5142:ϕ
5127:∧
5124:ϕ
5118:∨
5115:ψ
5112:≡
5106:ψ
5100:ϕ
5073:ϕ
5058:∨
5055:ϕ
5052:≡
5049:ϕ
5022:ϕ
5007:∨
5004:ϕ
5001:≡
4998:ϕ
4971:ϕ
4956:∧
4953:ϕ
4950:≡
4947:ϕ
4920:ϕ
4905:∧
4902:ϕ
4899:≡
4896:ϕ
4749:ϕ
4746:¬
4737:≡
4734:ϕ
4725:¬
4704:ϕ
4701:¬
4692:≡
4689:ϕ
4680:¬
4659:ϕ
4656:¬
4647:≡
4644:ϕ
4635:¬
4558:Φ
4555:¬
4547:≡
4544:Φ
4536:¬
4470:ψ
4467:≡
4464:ϕ
4444:ψ
4424:ϕ
4340:ϕ
4336:⊨
4292:∀
4282:∧
4266:ϕ
4262:⊨
4216:∃
4191:⟩
4188:…
4185:→
4172:→
4159:⟨
4156:∃
4146:⇔
4127:ϕ
4114:ϕ
4104:⊨
4030:ϕ
4026:⊨
3982:∀
3972:∧
3956:ϕ
3952:⊨
3906:∃
3881:⟩
3878:…
3875:→
3862:→
3849:⟨
3846:∀
3836:⇔
3817:ϕ
3804:ϕ
3794:⊨
3733:ϕ
3730:⊨
3691:∃
3666:⟩
3663:…
3660:→
3647:→
3634:⟨
3631:∃
3621:⇔
3611:ϕ
3602:⊨
3541:ϕ
3538:⊨
3499:∃
3474:⟩
3471:…
3468:→
3455:→
3442:⟨
3439:∀
3429:⇔
3419:ϕ
3410:⊨
3349:ϕ
3346:⊨
3307:∀
3282:⟩
3279:…
3276:→
3263:→
3250:⟨
3247:∃
3237:⇔
3227:ϕ
3218:⊨
3157:ϕ
3154:⊨
3115:∀
3090:⟩
3087:…
3084:→
3071:→
3058:⟨
3055:∀
3045:⇔
3035:ϕ
3026:⊨
2965:ϕ
2962:⊨
2926:⟩
2913:→
2907:⟨
2904:∃
2894:⇔
2884:ϕ
2875:⊨
2814:ϕ
2811:⊨
2775:⟩
2762:→
2756:⟨
2753:∀
2743:⇔
2733:ϕ
2724:⊨
2650:ϕ
2646:⊨
2617:¬
2614:∧
2598:ϕ
2594:⊨
2565:¬
2555:∨
2532:ϕ
2528:⊨
2499:∧
2483:ϕ
2479:⊨
2436:⇔
2420:ϕ
2416:⇔
2407:ϕ
2403:⊨
2336:ϕ
2332:⊨
2303:∨
2287:ϕ
2247:⇔
2231:ϕ
2227:⇒
2218:ϕ
2214:⊨
2147:ϕ
2143:⊨
2114:∨
2098:ϕ
2094:⊨
2058:⇔
2042:ϕ
2038:∨
2029:ϕ
2025:⊨
1958:ϕ
1954:⊨
1925:∧
1909:ϕ
1905:⊨
1869:⇔
1853:ϕ
1849:∧
1840:ϕ
1836:⊨
1782:ϕ
1750:⇔
1740:ϕ
1737:¬
1734:⊨
1668:∈
1655:⇔
1642:⊨
1588:⊥
1556:∧
1546:⊤
1543:⊨
1494:ϕ
1471:ϕ
1468:⊨
1410:over the
1371:∈
1368:ϕ
1345:∈
1313:→
1251:×
1245:⊆
1241:→
1190:→
917:lobally:
821:Operators
805:CTL uses
651:⇒
512:∧
506:¬
449:ϕ
439:ϕ
426:∣
420:ϕ
410:ϕ
397:∣
394:ϕ
384:∣
381:ϕ
371:∣
368:ϕ
358:∣
355:ϕ
345:∣
342:ϕ
332:∣
329:ϕ
318:∣
305:ϕ
302:⇔
299:ϕ
293:∣
287:ϕ
284:⇒
281:ϕ
275:∣
269:ϕ
266:∨
263:ϕ
257:∣
251:ϕ
248:∧
245:ϕ
239:∣
233:ϕ
230:¬
224:∣
218:∣
215:⊤
212:∣
209:⊥
199:ϕ
106:tree-like
5838:52853200
5522:See also
5251:Examples
2283:⊭
1779:⊭
1585:⊭
1412:language
1386:, where
1212:, where
1136:∨
960:at least
934:inally:
692:EF
656:AF
643:EG
633:EF
389:EG
376:AG
363:EF
350:AF
337:EX
324:AX
174:language
5849:(ed.).
5392:(ATL).
1102:) == ¬
431:E
402:A
182:grammar
136:History
55:improve
5857:
5836:
5789:
5760:
5741:
5704:
5694:
5651:
5576:
5504:graphs
1360:, and
1132:== ¬(
954:ntil:
780:or an
471:where
44:, but
5834:S2CID
5723:(PDF)
5702:S2CID
5562:(PDF)
5426:AG.EF
5416:(P⇒((
1068:== )
840:false
104:is a
98:logic
5855:ISBN
5758:ISBN
5739:ISBN
5692:ISBN
5649:ISBN
5612:help
5600:help
5574:ISBN
5464:and
5373:some
5366:.Q))
4595:and
4506:and
4436:and
4301:<
3991:<
1118:== ¬
1094:== ¬
1077:== ¬
1018:CTL*
1014:CTL*
838:and
836:true
830:The
813:and
172:The
144:and
130:CTL*
102:time
5824:doi
5797:doi
5731:doi
5682:doi
5678:147
5639:doi
5566:doi
5497:MSO
5487:to
5401:LTL
5358:.P)
5330:):
5326:or
1414:of
1144:) )
1114:==
1057:==
1044:}.
1012:In
892:t:
802:.
206:::=
176:of
154:i.e
94:CTL
5886::
5832:.
5818:.
5812:.
5795:.
5783:30
5781:.
5737:.
5725:.
5700:.
5690:.
5672:.
5647:.
5635:59
5629:.
5604:;
5592::
5590:}}
5586:{{
5572:.
5422:EX
5418:EX
5414:AG
5408:FG
5364:AG
5356:EX
5354:((
5352:EF
5341:Q)
5337:(P
5335:AG
5313:.P
5311:AF
5307:EG
5292:.P
5290:EG
5286:AF
5275:.P
5273:EF
5262:.P
5260:AG
4617:.
4570:.
4408:.
1506::
1438:.
1140:(¬
1138:EG
1122:(¬
1120:EG
1109:AF
1098:(¬
1096:EF
1089:AG
1081:(¬
1079:EX
1072:AX
1052:EF
1042:EX
1040:,
1038:EU
1036:,
1034:EG
904:).
842:.
817:.
540:EU
530:AU
520:AX
184::
160:.
152:,
132:.
5863:.
5840:.
5826::
5820:8
5803:.
5799::
5766:.
5747:.
5733::
5708:.
5684::
5657:.
5641::
5614:)
5610:(
5602:)
5582:.
5568::
5514:.
5475:p
5452:p
5362:(
5360:U
5339:U
5328:E
5324:A
5309:.
5299:G
5288:.
5235:)
5232:]
5226:U
5220:[
5217:E
5214:X
5211:E
5202:(
5190:]
5184:U
5178:[
5175:E
5154:)
5151:]
5145:U
5139:[
5136:A
5133:X
5130:A
5121:(
5109:]
5103:U
5097:[
5094:A
5070:F
5067:E
5064:X
5061:E
5046:F
5043:E
5019:F
5016:A
5013:X
5010:A
4995:F
4992:A
4968:G
4965:E
4962:X
4959:E
4944:G
4941:E
4917:G
4914:A
4911:X
4908:A
4893:G
4890:A
4860:}
4857:U
4854:A
4851:,
4848:F
4845:A
4842:,
4839:G
4836:E
4833:{
4813:}
4810:X
4807:E
4804:,
4801:X
4798:A
4795:{
4775:U
4772:E
4743:X
4740:E
4731:X
4728:A
4698:G
4695:A
4686:F
4683:E
4653:G
4650:E
4641:F
4638:A
4604:F
4582:G
4551:E
4540:A
4515:E
4493:A
4396:s
4365:)
4358:)
4351:)
4344:1
4333:)
4328:j
4324:s
4320:,
4315:M
4310:(
4307:)
4304:i
4298:j
4295:(
4287:(
4277:)
4270:2
4259:)
4254:i
4250:s
4246:,
4241:M
4236:(
4231:(
4224:(
4219:i
4213:)
4208:1
4204:s
4200:=
4197:s
4194:(
4180:2
4176:s
4167:1
4163:s
4151:(
4141:)
4136:]
4131:2
4123:U
4118:1
4110:[
4107:E
4101:)
4098:s
4095:,
4090:M
4085:(
4080:(
4055:)
4048:)
4041:)
4034:1
4023:)
4018:j
4014:s
4010:,
4005:M
4000:(
3997:)
3994:i
3988:j
3985:(
3977:(
3967:)
3960:2
3949:)
3944:i
3940:s
3936:,
3931:M
3926:(
3921:(
3914:(
3909:i
3903:)
3898:1
3894:s
3890:=
3887:s
3884:(
3870:2
3866:s
3857:1
3853:s
3841:(
3831:)
3826:]
3821:2
3813:U
3808:1
3800:[
3797:A
3791:)
3788:s
3785:,
3780:M
3775:(
3770:(
3745:)
3738:)
3727:)
3722:i
3718:s
3714:,
3709:M
3704:(
3699:(
3694:i
3688:)
3683:1
3679:s
3675:=
3672:s
3669:(
3655:2
3651:s
3642:1
3638:s
3626:(
3616:)
3608:F
3605:E
3599:)
3596:s
3593:,
3588:M
3583:(
3578:(
3553:)
3546:)
3535:)
3530:i
3526:s
3522:,
3517:M
3512:(
3507:(
3502:i
3496:)
3491:1
3487:s
3483:=
3480:s
3477:(
3463:2
3459:s
3450:1
3446:s
3434:(
3424:)
3416:F
3413:A
3407:)
3404:s
3401:,
3396:M
3391:(
3386:(
3361:)
3354:)
3343:)
3338:i
3334:s
3330:,
3325:M
3320:(
3315:(
3310:i
3304:)
3299:1
3295:s
3291:=
3288:s
3285:(
3271:2
3267:s
3258:1
3254:s
3242:(
3232:)
3224:G
3221:E
3215:)
3212:s
3209:,
3204:M
3199:(
3194:(
3169:)
3162:)
3151:)
3146:i
3142:s
3138:,
3133:M
3128:(
3123:(
3118:i
3112:)
3107:1
3103:s
3099:=
3096:s
3093:(
3079:2
3075:s
3066:1
3062:s
3050:(
3040:)
3032:G
3029:A
3023:)
3020:s
3017:,
3012:M
3007:(
3002:(
2977:)
2970:)
2959:)
2954:1
2950:s
2946:,
2941:M
2936:(
2931:(
2921:1
2917:s
2910:s
2899:(
2889:)
2881:X
2878:E
2872:)
2869:s
2866:,
2861:M
2856:(
2851:(
2826:)
2819:)
2808:)
2803:1
2799:s
2795:,
2790:M
2785:(
2780:(
2770:1
2766:s
2759:s
2748:(
2738:)
2730:X
2727:A
2721:)
2718:s
2715:,
2710:M
2705:(
2700:(
2675:)
2668:)
2661:)
2654:2
2643:)
2640:s
2637:,
2632:M
2627:(
2622:(
2609:)
2602:1
2591:)
2588:s
2585:,
2580:M
2575:(
2570:(
2560:(
2550:)
2543:)
2536:2
2525:)
2522:s
2519:,
2514:M
2509:(
2504:(
2494:)
2487:1
2476:)
2473:s
2470:,
2465:M
2460:(
2455:(
2448:(
2441:(
2431:)
2424:2
2411:1
2400:)
2397:s
2394:,
2389:M
2384:(
2379:(
2354:)
2347:)
2340:2
2329:)
2326:s
2323:,
2318:M
2313:(
2308:(
2298:)
2291:1
2280:)
2277:s
2274:,
2269:M
2264:(
2259:(
2252:(
2242:)
2235:2
2222:1
2211:)
2208:s
2205:,
2200:M
2195:(
2190:(
2165:)
2158:)
2151:2
2140:)
2137:s
2134:,
2129:M
2124:(
2119:(
2109:)
2102:1
2091:)
2088:s
2085:,
2080:M
2075:(
2070:(
2063:(
2053:)
2046:2
2033:1
2022:)
2019:s
2016:,
2011:M
2006:(
2001:(
1976:)
1969:)
1962:2
1951:)
1948:s
1945:,
1940:M
1935:(
1930:(
1920:)
1913:1
1902:)
1899:s
1896:,
1891:M
1886:(
1881:(
1874:(
1864:)
1857:2
1844:1
1833:)
1830:s
1827:,
1822:M
1817:(
1812:(
1787:)
1776:)
1773:s
1770:,
1765:M
1760:(
1755:(
1745:)
1731:)
1728:s
1725:,
1720:M
1715:(
1710:(
1685:)
1680:)
1677:s
1674:(
1671:L
1665:p
1660:(
1650:)
1645:p
1639:)
1636:s
1633:,
1628:M
1623:(
1618:(
1593:)
1582:)
1579:s
1576:,
1571:M
1566:(
1561:(
1551:)
1540:)
1537:s
1534:,
1529:M
1524:(
1519:(
1474:)
1465:s
1462:,
1457:M
1452:(
1424:M
1394:F
1374:F
1348:S
1342:s
1322:)
1319:L
1316:,
1310:,
1307:S
1304:(
1301:=
1296:M
1274:L
1254:S
1248:S
1220:S
1200:)
1197:L
1194:,
1186:,
1183:S
1180:(
1177:=
1172:M
1142:ψ
1134:E
1130:A
1126:)
1124:φ
1116:A
1112:φ
1104:E
1100:φ
1092:φ
1085:)
1083:φ
1075:φ
1066:φ
1063:F
1059:E
1055:φ
1004:W
1000:ψ
996:U
992:ψ
988:φ
984:W
980:ψ
977:W
974:φ
968:ψ
964:ψ
956:φ
952:U
948:ψ
945:U
942:φ
936:φ
932:F
928:φ
925:F
919:φ
915:G
911:φ
908:G
902:X
898:N
894:φ
890:x
886:φ
883:X
872:E
868:E
862:A
858:A
789:E
767:A
745:U
719:)
714:q
704:r
699:(
664:)
661:r
648:p
638:(
599:E
570:A
545:}
535:,
525:,
515:,
509:,
503:{
479:p
452:]
436:[
423:]
407:[
308:)
296:(
290:)
278:(
272:)
260:(
254:)
242:(
236:)
227:(
221:p
92:(
80:)
74:(
69:)
65:(
51:.
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.