558:, but also in lots of other articles using CTL. In fact I came across this when I noticed someone using 'Computational Tree Logic' - I am a little suspicious that in fact Knowledge itself is spreading this! Think about it: it is a logic that follows the tree of a computation - that's where the name comes from. It's a not a logic of 'Computational Tres' (as such a thing does not exist to the the best of my knowledge(, and it is also not a computational version of some 'tree logic'.
151:
74:
53:
22:
399:
1399:
translate to "éventuel" (or "eventuell" in German), but more "enfin" (fr)/"schließlich" (de). So, "eventually φ" means that at some point φ will hold (although it's not important at which point exactly), which also is expressed by "trueUφ". But you're not alone with this, the same question was raised
811:
On all paths, there is some state after which p is always true, so FG.p holds. However, there is a path, specifically 1→1→1→1→1→…, on which no state satisfies AG.p (even though this path does satisfy G.p) since at state 1 we always have the possible path 1→2→3→3→…, which does not satisfy G.p. Thus
716:
My intention is to model the known information surrounding some topic of controversy, so as to better relate it and visualize it (and even perform operations on it) versus a flat representation or outline-form like wikipedia. This could integrate multiple viewpoints and remove bias in information
1420:
The AG(PUQ) example seems to be explained badly. PUQ must hold on every path forever. So one likes chocolate until it is warm outside, but once it is warm, and then becomes cold again, one still has to like chocolate until it is warm. The textual description does not make this at all clear.
696:
The minimal set satisfying the rules S1-3 and P1-3 forms the language $ CTL^*$ . The syntax of the logic $ CTL$ is obtained by restricting the syntax to disallow boolean combinations and nesting of linear time operators. Formally, the $ CTL$ syntax is obtained by replacing P1-3 with
797:
Now, I think the original erroneous example was a mis-copy of an example in Huth and Ryan. The example Huth and Ryan actually uses is GF.p→GF.q. Since I think this is what the original editor intended, perhaps this should be used in place of FG.p. I don't think it really matters.
172:
1221:
for logical implication to distinguish this from the notation used to represent the state transition function. This could equally be the other way round, so long as they're distinct, but it appears standard in the literature to use them this way.
520:
As written currently, the page defines the syntax before giving the interpretation of the operators, which is awkward if you haven't seen CTL before. If there are no objections, I'll swap the two sections and touch up the text (if necessary).
649:$ CTL^*$ is an extension of the language for propositional logic with temporal connectives. In particular we consider countably many propositional variables $ AP$ and the connectives $ \lnot, \land, A, E, X, {\cal U}$ . The ``Before
556:(Clarke, E. M., Emerson, E. A., and Sistla, A. P. (1986). "Automatic verification of finite-state concurrent systems using temporal logic specifications". ACM Transactions on Programming Languages and Systems 8 (2): 244–26)
801:
On the subject of Huth and Ryan though, if you're using it as reference, the examples seem to imply that FG.p is expressible as AF.AG.p, but this is not true. Consider the system of three states, with transitions
471:
Hi, I have a question about the examples. Are they supposed to be pure CTL, or CTL*? Because the last 2 are actually CTL* formulas. In order for them to be CTL, until operator needs to be path-quantified also.
616:
There are no state/path operators. There are temporal operators, temporal quantifiers (could be considered as operators also, I don't know), and state and path formulas. I corrected it in the article.
582:
I just came up with the terms "state operators" and "path operators" myself. If there is another "official" name for those or someone find something better, please edit... --] 02:00, 21 Jul 2004 (UTC)
196:
642:
I agree, the description of the syntax is a bit confusing. The main different between CTL and CTL* is that in CTL it is not possible to nest temporal operator using classical connectives.
812:
the model does not satisfy AF.AG.p. Huth and Ryan's examples for FG.p and AF.AG.p seem equivalent because it uses deadlock as p, and deadlock states tend to always satisfy AG.deadlock.
336:
660:(\bot \; {\cal B} \; \varphi)$ and $ {\cal F} \varphi := (\top \; {\cal U} \; \varphi)$ . Abbreviations $ \lor$ , $ \rightarrow$ , $ \leftrightarrow$ are defined in the usual way.
253:
191:
1273:
1249:
1219:
1199:
1231:
Somebody has turned it back at the definition (but not in the rest of the article), so I fixed it again to at least be consistent. However, I think this article should use
1456:
124:
114:
1138:
1115:
1095:
1073:
1049:
1027:
1003:
980:
960:
938:
914:
892:
1461:
663:
The class of state formulae (formulae that are true or false when evaluated in a state) and the class of path formulae (true or false of paths) are defined as:
536:
And by the way, I'm not sure if the correct name is "Computational tree logic" or "Computation tree logic". I've seen both. Which is the (more) correct one?
762:
satisfies AF.p Thus we have AF.p for any state on path π. Thus. π satisfies G.AF.p. Thus we have G.AF.p for all paths out of s. Thus, s satisfies AG.AF.p.
90:
1451:
298:
543:
As far As I know CTL is the "Computation tree logic", while CTL* is commonly referred as "Full
Computation tree logic" or "Full Branching time logic"
815:
272:
137:
81:
58:
1276:
633:
This description of CTL is wrong. Though the given examples are valid CTL-Formulas, the description doesn't distinct between CTL and CTL* --
361:
1380:
501:
713:
I'm interested in taking the wiki source code and extending it to be able to make trees like this, using the group editing model of wiki.
595:
It's easier to explain what CTL* is and then say CTL is the subset where every temporal operator must be preceeded by a path quantifier.
1428:
1304:
842:
244:
1165:
But below, only X is used. I'll exchange N and X in the definition (less work ;)). If anyone objects, just change every X to N below.
561:
So is there a quick way to update
Knowledge so that this page is called 'Computation Tree Logic'? I will change it on the page myself.
1141:
819:
485:
225:
734:
Here's a proof: Assume a model M and start state s satisfying GF.p Then take any computation path π out of s. Consider any state s
317:
448:
AF r? Both are possible and I'm going to edit the section to match the first variant. This variant has the advantage that it
282:
163:
33:
292:
206:
327:
89:
related articles on
Knowledge. If you would like to participate, please visit the project page, where you can join
354:
1280:
500:
You are right, I've just noticed it too. I'm going to edit the section and add a note that those two are CTL*.
1384:
505:
1432:
1308:
846:
1145:
823:
784:
was arbitrary, so all subpaths of π satisfy F.p. So π satisfies GF.p π was arbitrary, so s satisfies GF.p.
489:
1395:
Ok, from your IP you are French, but i know the same problem from German, too. Eventually in
English does
768:
Next assume a model M and start state s satisfying AG.AF.p. Take any path π out of s. Consider any state s
452:
a formula according to the grammar given. The other is not as the implication formally needs parentheses.
424:
1252:
634:
263:
39:
1168:
568:
1424:
1405:
1376:
1300:
1223:
838:
481:
21:
1335:
754:
paths out of s, we have F.p holds for the sub-path π'. Thus we have F.p holds for any path out of s
432:
1258:
1234:
1204:
1184:
1370:
but Fφ doesn't impose that φ have to be verified unlike which implies that φ will be verified.
1358:
U is define as "φ U ψ - Until: φ has to hold until at some position ψ holds. This implies that
1162:
N φ - Next: φ has to hold at the next state (this operator is sometimes noted X instead of N).
453:
1275:
is syntax, and state transition is at the meta level, so I don't think they will be confused.
431:
Please help fix the broken anchors. You can remove this template after fixing the problems. |
182:
834:
Sorry this paragraph is plain wrong, GF p is fairness. "start state s satisfying GF.p" =: -->
411:
234:
86:
602:
Should the article on CTL* parctically duplicate the definitions used here? (My answer: NO)
1401:
1123:
1100:
1080:
1058:
1034:
1012:
988:
965:
945:
923:
899:
877:
710:
Is there any software out there to make trees like this, at any level of implementation?
861:
There is no derivation of the weak until operators from the minimal set of operators. --
1331:
620:
606:
599:
Should there be only one page describing CTL, LTL, CTL* (unsure about the name though)?
457:
308:
150:
173:
Requested articles/Applied arts and sciences/Computer science, computing, and
Internet
1445:
1297:
The notation used in the slides linked is really bad. It's very unconventional.
1140:) . Maybe they are not obvious for beginners, should they be put on the main page?
862:
1436:
1409:
1388:
1339:
1312:
1284:
1226:
1171:
1149:
865:
850:
827:
808:
where p is true in states 1 and 3, but not in state 2. I assume 1 as start state.
637:
623:
572:
509:
493:
461:
446:
In the example it is not clear where to put the parentheses: is it EF(EG p =: -->
564:
215:
73:
52:
673:
S2 if $ p,q$ are state formulae then so are $ p \land q$ and $ \lnot q$
687:
P2 if $ p,q$ are path formulae then so are $ p \land q$ and $ \lnot q$
676:
S3 if $ p$ is a path formula then $ E p$ and $ A p$ are state formulae
690:
P3 if $ p,q$ are path formulae then so are $ X p$ and $ p {\cal U} q$
701:
P0 if $ p,q$ are path formulae the so are $ X p$ and $ p {\cal U} q$
419:
This article links to one or more target anchors that no longer exist.
1373:
Where is the bug? does Fφ means that φ has to hold (not eventually)?
1400:
in some of the lectures I attended that involved temporal logics ;-)
720:
Anyone who would wants to help with this please send me a comment!
794:
I've changed it to FG.p. This actually isn't expressible in CTL.
524:-- Gilbert (sorry I don't have a wikipedia account) 23 June 2009
1327:
1320:
1251:, since this is the notation used in all other logic articles (
835:
no, GF p is true or false of infinite traces, not of states.
393:
291:
Find pictures for the biographies of computer scientists (see
15:
772:
on this path. Since we have AG.AF.p, π satisfies G.AF.p, so s
658:
modality are defined, respectively, as $ {\cal G} \varphi :=
746:
is by construction reachable from s, π' is a sub-path of
731:
GF.p is expressible in CTL. It's equivalent to AG.AF.p.
1261:
1237:
1207:
1187:
1126:
1103:
1083:
1061:
1037:
1015:
991:
968:
948:
926:
902:
880:
776:
satisfies AF.p, so the subpath π' of π beginning at s
554:
You can look it up in the paper cited in the article
85:, a collaborative effort to improve the coverage of
790:So they're equivalent. GF.p is expressible in CTL.
742:π' is not necessarily a sub-path of π, but, since s
1267:
1243:
1213:
1193:
1132:
1109:
1089:
1067:
1043:
1021:
997:
974:
954:
932:
908:
886:
197:Computer science articles needing expert attention
1354:has to hold (somewhere on the subsequent path)."
738:on this path. And consider any path π' out of s
337:WikiProject Computer science/Unreferenced BLPs
670:S1 each atomic proposition is a state formula
8:
684:P1 each state formula is also a path formula
254:Computer science articles without infoboxes
192:Computer science articles needing attention
1422:
836:
706:Software for constructing/modeling a tree?
652:modality is defined as the dual of ``Until
158:Here are some tasks awaiting attention:
132:
47:
1326:Currently there isn't anything useful at
1260:
1236:
1206:
1186:
1125:
1102:
1082:
1060:
1036:
1014:
990:
967:
947:
925:
901:
879:
533:Does anybody know the full name for CTL*?
1457:Low-importance Computer science articles
1330:- I suggest turning it into a redirect.
49:
19:
1159:The "state operators" definition says
586:move to CTL & state/path operators
99:Knowledge:WikiProject Computer science
1462:WikiProject Computer science articles
423:] The anchor (#Vocabulary) has been
102:Template:WikiProject Computer science
7:
750:path out of s. Since GF.p holds for
79:This article is within the scope of
38:It is of interest to the following
1181:I've changed the article to using
273:Timeline of computing 2020–present
14:
1452:C-Class Computer science articles
1350:F is define as "F φ - Finally: φ
299:Computing articles needing images
1366:and it is said that : " Fφ == "
1360:ψ will be verified in the future
397:
149:
72:
51:
20:
447:AF r) or is it (EF EG p) =: -->
119:This article has been rated as
1262:
1238:
1208:
1188:
547:CTL = 'Computation Tree Logic'
1:
1410:04:08, 26 November 2010 (UTC)
1340:23:35, 13 December 2007 (UTC)
1313:01:21, 13 February 2009 (UTC)
619:I Always forget to sign :(((
573:12:37, 9 September 2008 (UTC)
550:not Computational Tree Logic!
540:--] 18:45, 20 Jul 2004 (UTC)
353:Tag all relevant articles in
93:and see a list of open tasks.
1437:09:13, 26 October 2020 (UTC)
1268:{\displaystyle \rightarrow }
1244:{\displaystyle \rightarrow }
1214:{\displaystyle \rightarrow }
1194:{\displaystyle \Rightarrow }
857:No derivation for weak until
851:20:03, 29 January 2016 (UTC)
645:What about something like :
510:12:38, 10 January 2013 (UTC)
494:12:35, 4 November 2012 (UTC)
362:WikiProject Computer science
138:WikiProject Computer science
82:WikiProject Computer science
462:16:39, 27 August 2014 (UTC)
293:List of computer scientists
1478:
1285:00:14, 24 March 2008 (UTC)
578:State & path operators
125:project's importance scale
624:17:06, 2 April 2006 (UTC)
355:Category:Computer science
131:
118:
105:Computer science articles
67:
46:
1389:13:20, 6 July 2010 (UTC)
1227:10:22, 4 June 2007 (UTC)
1150:13:24, 11 May 2010 (UTC)
656:modality and ``Sometimes
638:13:12, 6 July 2006 (UTC)
357:and sub-categories with
1172:16:20, 3 May 2007 (UTC)
1155:Inconsistent use of N/X
866:05:48, 3 May 2007 (UTC)
828:08:42, 2 May 2007 (UTC)
1269:
1245:
1215:
1195:
1134:
1111:
1091:
1069:
1045:
1023:
999:
976:
956:
934:
910:
888:
425:deleted by other users
318:Computer science stubs
28:This article is rated
1345:transformation of EFφ
1270:
1246:
1216:
1196:
1135:
1133:{\displaystyle \phi }
1112:
1110:{\displaystyle \lor }
1092:
1090:{\displaystyle \psi }
1070:
1068:{\displaystyle \phi }
1046:
1044:{\displaystyle \psi }
1024:
1022:{\displaystyle \phi }
1000:
998:{\displaystyle \phi }
977:
975:{\displaystyle \lor }
957:
955:{\displaystyle \psi }
935:
933:{\displaystyle \phi }
911:
909:{\displaystyle \psi }
889:
887:{\displaystyle \phi }
818:comment was added by
1416:Examples (once more)
1259:
1235:
1205:
1185:
1124:
1101:
1081:
1059:
1035:
1013:
989:
966:
946:
924:
900:
878:
612:state/path operators
136:Things you can help
805:1→1, 1→2, 2→3, 3→3
1265:
1241:
1211:
1191:
1130:
1107:
1087:
1065:
1041:
1019:
995:
972:
952:
930:
906:
884:
654:. The ``Generally
34:content assessment
1439:
1427:comment added by
1379:comment added by
1303:comment added by
853:
841:comment added by
831:
516:Reorder the Page?
484:comment added by
439:
438:
414:in most browsers.
392:
391:
388:
387:
384:
383:
380:
379:
376:
375:
1469:
1391:
1315:
1274:
1272:
1271:
1266:
1250:
1248:
1247:
1242:
1220:
1218:
1217:
1212:
1200:
1198:
1197:
1192:
1139:
1137:
1136:
1131:
1116:
1114:
1113:
1108:
1096:
1094:
1093:
1088:
1074:
1072:
1071:
1066:
1050:
1048:
1047:
1042:
1028:
1026:
1025:
1020:
1004:
1002:
1001:
996:
981:
979:
978:
973:
961:
959:
958:
953:
939:
937:
936:
931:
915:
913:
912:
907:
893:
891:
890:
885:
813:
787:So AG.AF.p→GF.p
780:satisfies F.p. s
765:So GF.p→AG.AF.p
667:State Formulae:
635:Neatlittleeraser
496:
442:Examples (again)
433:Reporting errors
401:
400:
394:
366:
360:
235:Computer science
164:Article requests
153:
146:
145:
133:
107:
106:
103:
100:
97:
96:Computer science
87:Computer science
76:
69:
68:
63:
59:Computer science
55:
48:
31:
25:
24:
16:
1477:
1476:
1472:
1471:
1470:
1468:
1467:
1466:
1442:
1441:
1418:
1374:
1347:
1324:
1298:
1295:
1277:220.157.232.180
1257:
1256:
1255:etc.). Logical
1233:
1232:
1203:
1202:
1183:
1182:
1179:
1157:
1122:
1121:
1099:
1098:
1079:
1078:
1057:
1056:
1033:
1032:
1011:
1010:
987:
986:
964:
963:
944:
943:
922:
921:
898:
897:
876:
875:
859:
814:—The preceding
783:
779:
775:
771:
761:
757:
745:
741:
737:
729:
708:
681:Path Formulae:
631:
614:
593:
588:
580:
530:
518:
479:
469:
444:
435:
417:
416:
415:
398:
372:
369:
364:
358:
346:Project-related
341:
322:
303:
277:
258:
239:
220:
201:
177:
104:
101:
98:
95:
94:
61:
32:on Knowledge's
29:
12:
11:
5:
1475:
1473:
1465:
1464:
1459:
1454:
1444:
1443:
1417:
1414:
1413:
1412:
1381:152.77.200.242
1368:
1367:
1364:
1363:
1356:
1355:
1346:
1343:
1323:
1317:
1294:
1293:Lecture slides
1291:
1289:
1264:
1240:
1210:
1190:
1178:
1175:
1156:
1153:
1129:
1106:
1086:
1064:
1040:
1018:
994:
971:
951:
929:
905:
883:
858:
855:
793:
781:
777:
773:
769:
759:
755:
743:
739:
735:
728:
725:
717:presentation.
707:
704:
703:
702:
694:
693:
692:
691:
688:
685:
679:
678:
677:
674:
671:
647:
630:
627:
613:
610:
604:
603:
600:
592:
589:
587:
584:
579:
576:
538:
537:
534:
529:
526:
517:
514:
513:
512:
502:62.245.100.121
468:
465:
443:
440:
437:
436:
430:
429:
428:
412:case-sensitive
406:
405:
404:
402:
390:
389:
386:
385:
382:
381:
378:
377:
374:
373:
371:
370:
368:
367:
350:
342:
340:
339:
333:
323:
321:
320:
314:
304:
302:
301:
296:
288:
278:
276:
275:
269:
259:
257:
256:
250:
240:
238:
237:
231:
221:
219:
218:
212:
202:
200:
199:
194:
188:
178:
176:
175:
169:
157:
155:
154:
142:
141:
129:
128:
121:Low-importance
117:
111:
110:
108:
91:the discussion
77:
65:
64:
62:Low‑importance
56:
44:
43:
37:
26:
13:
10:
9:
6:
4:
3:
2:
1474:
1463:
1460:
1458:
1455:
1453:
1450:
1449:
1447:
1440:
1438:
1434:
1430:
1429:78.27.127.183
1426:
1415:
1411:
1407:
1403:
1398:
1394:
1393:
1392:
1390:
1386:
1382:
1378:
1371:
1365:
1361:
1357:
1353:
1349:
1348:
1344:
1342:
1341:
1337:
1333:
1329:
1322:
1318:
1316:
1314:
1310:
1306:
1305:87.194.191.26
1302:
1292:
1290:
1287:
1286:
1282:
1278:
1254:
1229:
1228:
1225:
1176:
1174:
1173:
1170:
1166:
1163:
1160:
1154:
1152:
1151:
1147:
1143:
1127:
1119:
1104:
1084:
1077:
1062:
1054:
1038:
1031:
1016:
1008:
992:
984:
969:
949:
942:
927:
919:
903:
896:
881:
873:
868:
867:
864:
856:
854:
852:
848:
844:
843:81.64.148.250
840:
832:
829:
825:
821:
817:
809:
806:
803:
799:
795:
791:
788:
785:
766:
763:
753:
749:
732:
726:
724:
721:
718:
714:
711:
705:
700:
699:
698:
689:
686:
683:
682:
680:
675:
672:
669:
668:
666:
665:
664:
661:
659:
655:
651:
646:
643:
640:
639:
636:
628:
626:
625:
622:
617:
611:
609:
608:
601:
598:
597:
596:
590:
585:
583:
577:
575:
574:
570:
566:
562:
559:
557:
552:
551:
548:
544:
541:
535:
532:
531:
527:
525:
522:
515:
511:
507:
503:
499:
498:
497:
495:
491:
487:
483:
476:
473:
466:
464:
463:
459:
455:
451:
441:
434:
426:
422:
421:
420:
413:
409:
403:
396:
395:
363:
356:
352:
351:
349:
347:
343:
338:
335:
334:
332:
330:
329:
324:
319:
316:
315:
313:
311:
310:
305:
300:
297:
294:
290:
289:
287:
285:
284:
279:
274:
271:
270:
268:
266:
265:
260:
255:
252:
251:
249:
247:
246:
241:
236:
233:
232:
230:
228:
227:
222:
217:
214:
213:
211:
209:
208:
203:
198:
195:
193:
190:
189:
187:
185:
184:
179:
174:
171:
170:
168:
166:
165:
160:
159:
156:
152:
148:
147:
144:
143:
139:
135:
134:
130:
126:
122:
116:
113:
112:
109:
92:
88:
84:
83:
78:
75:
71:
70:
66:
60:
57:
54:
50:
45:
41:
35:
27:
23:
18:
17:
1423:— Preceding
1419:
1396:
1372:
1369:
1359:
1351:
1325:
1296:
1288:
1230:
1180:
1169:132.231.54.1
1167:
1164:
1161:
1158:
1117:
1075:
1052:
1029:
1006:
982:
940:
917:
894:
871:
869:
863:Marco Bakera
860:
837:— Preceding
833:
810:
807:
804:
800:
796:
792:
789:
786:
767:
764:
751:
747:
733:
730:
727:GF.p and CTL
722:
719:
715:
712:
709:
695:
662:
657:
653:
650:
648:
644:
641:
632:
629:This is CTL*
618:
615:
605:
594:
581:
563:
560:
555:
553:
549:
546:
545:
542:
539:
523:
519:
480:— Preceding
477:
474:
470:
449:
445:
418:
410:Anchors are
407:
345:
344:
328:Unreferenced
326:
325:
307:
306:
281:
280:
262:
261:
243:
242:
224:
223:
205:
204:
181:
180:
162:
161:
120:
80:
40:WikiProjects
1375:—Preceding
1319:Merge from
1299:—Preceding
1142:192.93.2.32
820:18.243.5.80
486:93.87.39.27
1446:Categories
1402:Thomas5388
1352:eventually
1224:Someguy137
870:There are
1332:Ripper234
758:. Thus, s
621:Ripper234
607:Ripper234
478:-- Krle
216:Computing
1425:unsigned
1377:unsigned
1301:unsigned
1177:Notation
839:unsigned
816:unsigned
482:unsigned
475:Cheers,
467:Examples
450:truly is
264:Maintain
207:Copyedit
723:-Aaron
427:before.
245:Infobox
183:Cleanup
123:on the
30:C-class
1005:) and
565:Cweise
528:Names?
226:Expand
36:scale.
1201:over
1051:] ==
916:] ==
309:Stubs
283:Photo
140:with:
1433:talk
1406:talk
1385:talk
1336:talk
1328:CTL*
1321:CTL*
1309:talk
1281:talk
1146:talk
847:talk
824:talk
748:some
591:Move
569:talk
506:talk
490:talk
458:talk
454:Xlae
408:Tip:
1397:not
1253:LTL
752:all
115:Low
1448::
1435:)
1408:)
1387:)
1362:."
1338:)
1311:)
1283:)
1263:→
1239:→
1222:--
1209:→
1189:⇒
1148:)
1128:ϕ
1118:EG
1105:∨
1097:]
1085:ψ
1063:ϕ
1039:ψ
1017:ϕ
993:ϕ
983:AG
970:∨
962:]
950:ψ
928:ϕ
904:ψ
882:ϕ
849:)
826:)
571:)
508:)
492:)
460:)
365:}}
359:{{
1431:(
1404:(
1383:(
1334:(
1307:(
1279:(
1144:(
1120:(
1076:U
1055:[
1053:E
1030:W
1009:[
1007:E
985:(
941:U
920:[
918:A
895:W
874:[
872:A
845:(
830:.
822:(
782:i
778:i
774:i
770:i
760:i
756:i
744:i
740:i
736:i
567:(
504:(
488:(
456:(
348::
331::
312::
295:)
286::
267::
248::
229::
210::
186::
167::
127:.
42::
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
