1357:
1350:
1444:
1509:
2096:). In this case, if there is an overlap in the set of ω-words accepted by the two automata, it implies that the model accepts some behaviors which violate the desired property. If there is no overlap, there are no property-violating behaviors which are accepted by the model. Formally, the intersection of the two non-deterministic Büchi automata is empty if and only if the model satisfies the specified property.
1145:
1437:
1196:
1275:
1094:
2154:)). For example, a safety property may require that an autonomous rover never drives over a cliff, or that a software product never allows a successful login with an incorrect password. A liveness property may require that the rover always continues to collect data samples, or that a software product repeatedly sends telemetry data.
2077:
LTL formulas are commonly used to express constraints, specifications, or processes that a system should follow. The field of model checking aims to formally verify whether a system meets a given specification. In the case of automata-theoretic model checking, both the system of interest and a
187:
ntil. Other than these fundamental operators, there are additional logical and temporal operators defined in terms of the fundamental operators, in order to write LTL formulas succinctly. The additional logical operators are ∧, →, ↔,
2082:, or automata, and then compared to evaluate whether the system is guaranteed to have the specified property. In computer science, this type of model checking is often used to verify that an algorithm is structured correctly.
2163:
has a finite prefix such that, however it is extended to an infinite path, it is still a counterexample. For liveness properties, on the other hand, every finite path can be extended to an infinite path that satisfies the
2091:
that is equivalent to the model (accepts an ω-word precisely if it is the model) and another one that is equivalent to the negation of the property (accepts an ω-word precisely it satisfies the negated property) (cf.
1976:, and ∧ to appear in the formula, which are not fundamental operators of LTL. Note that the transformation to the negation normal form does not blow up the length of the formula. This normal form is useful in
1492:
1405:
1322:
1251:
943:, is the dual of weak until. It is defined similar to the until operator, so that the release condition has to hold at some point. Therefore, it is stronger than the release operator.
1129:
1077:
1180:
2494:
2670:
1522:
Let φ, ψ, and ρ be LTL formulas. The following tables list some of the useful equivalences that extend standard equivalences among the usual logical operators.
804:, with semantics similar to that of the until operator but the stop condition is not required to occur (similar to release). It is sometimes useful since both
2340:
2093:
1977:
2244:
2377:
61:, e.g., a condition will eventually be true, a condition will be true until another fact becomes true, etc. It is a fragment of the more complex
2561:
2600:
2559:
Chakraborty, Souymodip; Katoen, Joost-Pieter (2014). Diaz, Josep; Lanese, Ivan; Sangiorgi, Davide (eds.). "Parametric LTL on Markov Chains".
2475:
2283:
2177:
78:
1989:
2522:
2514:
2425:
1356:
2645:
1443:
2455:
2543:
2212:
2650:
1964:
Using the above equivalences for negation propagation, it is possible to derive the normal form. This normal form allows
1349:
2371:
275:
1465:
1378:
1295:
1224:
1508:
1436:
2181:
2493:
A. Pnueli and R. Rosner. "On the synthesis of a reactive module" In
Proceedings of the 16th ACM SIGPLAN-SIGACT
2675:
2231:
2381:
2248:
1144:
2003:
105:
2207:
2079:
1993:
2641:
1111:
1059:
2580:
2061:
problems. LTL synthesis and the problem of verification of games against an LTL winning condition is
2366:
1162:
89:
58:
1195:
2606:
2570:
1997:
334:. Formally, the satisfaction relation ⊨ between a word and an LTL formula is defined as follows:
112:
66:
2088:
1274:
2596:
2535:
2518:
2471:
2421:
2279:
82:
2415:
2273:
1093:
2588:
2417:
Automata, Languages and
Programming: 37th International Colloquium, ICALP ... - Google Books
2346:
267:
2401:
Sec. 5.1.5 "Weak Until, Release, and
Positive Normal Form" of Principles of Model Checking.
2411:
2300:
2202:
2106:
2104:
There are two main types of properties that can be expressed using linear temporal logic:
2058:
1203:
1041:
54:
17:
2632:
2584:
2447:
2362:
2160:
2087:
To check LTL specifications on infinite system runs, a common technique is to obtain a
2054:
258:
119:
116:
50:
2664:
2459:
2451:
2269:
501:
271:
2610:
2463:
2193:
Parametric linear temporal logic extends LTL with variables on the until-modality.
2482:
2592:
2637:
2627:
2334:
93:
47:
2547:
1021:
The semantics for the temporal operators are pictorially presented as follows.
2173:
2025:
No formula in LTL can define the language that is defined by the CTL formulas
2497:(POPL '89). Association for Computing Machinery, New York, NY, USA, 179–190.
2014:
No formula in CTL can define the language that is defined by the LTL formula
2317:
2062:
2350:
2172:
One of the applications of linear temporal logic is the specification of
2124:
1504:
first becomes true, which must hold at the current or a future position.
2498:
1270:
becomes true, which must hold at the current or a future position.
2575:
2414:; Gavoille, Cyril; Kirchner, Claude; Spirakis, Paul (2010-06-30).
31:
2513:
Proceedings of the 8th Banff Higher Order
Workshop (Banff'94).
2232:
Logic in
Computer Science: Modelling and Reasoning about Systems
2007:
62:
2468:
25 years of model checking: history, achievements, perspectives
1934:
all negations appear only in front of the atomic propositions,
2159:
More generally, safety properties are those for which every
1475:
1388:
1305:
1234:
262:
by an infinite sequence of truth valuations of variables in
2546:, Volume 21, Issue 4, 1985, Pages 181-185, ISSN 0020-0190,
2006:(CTL) and linear temporal logic (LTL) are both a subset of
1140:
eventually has to hold (somewhere on the subsequent path).
53:
with modalities referring to time. In LTL, one can encode
574:
The additional logical operators are defined as follows:
266:. These sequences can be viewed as a word on a path of a
2511:
An
Automata-Theoretic Approach to Linear Temporal Logic.
2654:
2074:
Automata-theoretic linear temporal logic model checking
2275:
Many-dimensional modal logics: theory and applications
2101:
Expressing important properties in formal verification
27:
Modal temporal logic with modalities referring to time
1468:
1381:
1298:
1227:
1165:
1114:
1062:
1978:
translation from an LTL formula to a Büchi automaton
1500:has to be true until and including the point where
1333:has to be true until and including the point where
196:. Following are the additional temporal operators.
1486:
1399:
1316:
1245:
1174:
1123:
1071:
2517:, vol. 1043, pp. 238–266, Springer-Verlag, 1996.
2272:; A. Kurucz; F. Wolter; M. Zakharyaschev (2003).
2495:Symposium on Principles of programming languages
1926:All the formulas of LTL can be transformed into
1487:{\displaystyle \psi \;{\mathcal {M}}\,\varphi }
1400:{\displaystyle \psi \;{\mathcal {W}}\,\varphi }
1317:{\displaystyle \psi \;{\mathcal {R}}\,\varphi }
1246:{\displaystyle \psi \;{\mathcal {U}}\,\varphi }
81:, linear temporal logic (LTL) is a fragment of
65:, which additionally allows branching time and
2378:"Principles of Model Checking - the MIT Press"
2057:and satisfiability against an LTL formula are
2633:Linear-Time Temporal Logic and Büchi Automata
8:
2548:https://doi.org/10.1016/0020-0190(85)90056-0
2341:Symposium on Foundations of Computer Science
2324:(PhD). University of California Los Angeles.
527:}, which is the set of ω-words that satisfy
160:if ψ and φ are LTL formulas then ¬ψ, φ ∨ ψ,
1191:has to hold on the entire subsequent path.
812:can be defined in terms of the weak until:
2322:Tense Logic and the Theory of Linear Order
1472:
1385:
1302:
1231:
137:. Formally, the set of LTL formulas over
2574:
1988:LTL can be shown to be equivalent to the
1480:
1474:
1473:
1467:
1393:
1387:
1386:
1380:
1310:
1304:
1303:
1297:
1239:
1233:
1232:
1226:
1164:
1113:
1061:
2094:Linear temporal logic to Büchi automaton
2078:specification are expressed as separate
1789:
1651:
1524:
1023:
2569:. Springer Berlin Heidelberg: 207–221.
2224:
2671:Computer-related introductions in 1977
710:remains true until and including once
2565:. Lecture Notes in Computer Science.
2010:, but are incomparable. For example,
104:LTL is built up from a finite set of
7:
2651:LTL to Buchi translation algorithms
2499:https://doi.org/10.1145/75277.75293
2178:Planning Domain Definition Language
141:is inductively defined as follows:
2337:, The temporal logic of programs.
1990:monadic first-order logic of order
670:The additional temporal operators
25:
2653:a genealogy, from the website of
2515:Lecture Notes in Computer Science
2301:"First-order Definable Languages"
1124:{\displaystyle \Diamond \varphi }
1072:{\displaystyle \bigcirc \varphi }
2646:Free University of Bozen-Bolzano
1507:
1442:
1435:
1355:
1348:
1273:
1194:
1143:
1092:
2339:Proceedings of the 18th Annual
1089:has to hold at the next state.
88:LTL was first proposed for the
2544:Information Processing Letters
2213:Safety and liveness properties
2130:something good keeps happening
2110:properties usually state that
1:
2657:a library for model checking.
1992:, FO—a result known as
1937:only other logical operators
1175:{\displaystyle \Box \varphi }
792:Weak until and strong release
2593:10.1007/978-3-662-44602-7_17
2562:Theoretical Computer Science
2372:Principles of Model Checking
2245:"Linear-time Temporal Logic"
1948:only the temporal operators
1793:Special temporal properties
294:,... be such an ω-word. Let
71:propositional temporal logic
2112:something bad never happens
1996:— or equivalently to
1984:Relations with other logics
796:Some authors also define a
330:,..., which is a suffix of
2692:
2306:. University of Stuttgart.
1945:, ∧, and ∨ can appear, and
1432:must remain true forever.
1345:must remain true forever.
722:must remain true forever.
69:. LTL is sometimes called
40:linear-time temporal logic
18:Linear-time temporal logic
2182:preference-based planning
1792:
1654:
1527:
1202:
1040:
939:binary operator, denoted
800:binary operator, denoted
563:over alphabet 2, we have
539:if there exist an ω-word
488:satisfies an LTL formula
2278:. Elsevier. p. 46.
682:are defined as follows:
92:of computer programs by
1337:first becomes true; if
106:propositional variables
2169:Specification language
2128:properties state that
2050:Computational problems
2004:Computation tree logic
1488:
1401:
1318:
1247:
1176:
1125:
1073:
256:An LTL formula can be
125:(some literature uses
2628:A presentation of LTL
2208:Metric temporal logic
2080:finite-state machines
1655:Negation propagation
1489:
1402:
1319:
1248:
1177:
1126:
1074:
36:linear temporal logic
2351:10.1109/SFCS.1977.32
1928:negation normal form
1922:Negation normal form
1466:
1428:never becomes true,
1379:
1341:never becomes true,
1296:
1225:
1163:
1112:
1060:
787:always remains true)
718:never becomes true,
57:about the future of
2638:LTL Teaching slides
2585:2014arXiv1406.6683C
2367:Joost-Pieter Katoen
2180:for the purpose of
1998:star-free languages
559:if for each ω-word
168:ψ are LTL formulas.
90:formal verification
1484:
1397:
1314:
1243:
1172:
1121:
1069:
157:is an LTL formula;
2642:Alessandro Artale
2602:978-3-662-44602-7
2540:Defining Liveness
2536:Fred B. Schneider
2477:978-3-540-69849-4
2299:Diekert, Volker.
2285:978-0-444-50826-3
2063:2EXPTIME-complete
1919:
1918:
1788:
1787:
1650:
1649:
1515:
1514:
714:becomes true. If
484:We say an ω-word
472:must remain true
115:¬ and ∨, and the
113:logical operators
83:first-order logic
16:(Redirected from
2683:
2615:
2614:
2578:
2556:
2550:
2532:
2526:
2509:Moshe Y. Vardi.
2507:
2501:
2491:
2485:
2481:
2444:
2438:
2437:
2435:
2434:
2412:Abramsky, Samson
2408:
2402:
2399:
2393:
2392:
2390:
2389:
2380:. Archived from
2359:
2353:
2332:
2326:
2325:
2314:
2308:
2307:
2305:
2296:
2290:
2289:
2266:
2260:
2259:
2257:
2256:
2247:. Archived from
2241:
2235:
2229:
1790:
1652:
1525:
1511:
1496:Strong release:
1493:
1491:
1490:
1485:
1479:
1478:
1446:
1439:
1406:
1404:
1403:
1398:
1392:
1391:
1359:
1352:
1323:
1321:
1320:
1315:
1309:
1308:
1277:
1252:
1250:
1249:
1244:
1238:
1237:
1204:Binary operators
1198:
1181:
1179:
1178:
1173:
1147:
1130:
1128:
1127:
1122:
1096:
1078:
1076:
1075:
1070:
1024:
456:and for all 0 ≤
444:if there exists
268:Kripke structure
79:expressive power
21:
2691:
2690:
2686:
2685:
2684:
2682:
2681:
2680:
2661:
2660:
2624:
2619:
2618:
2603:
2558:
2557:
2553:
2533:
2529:
2508:
2504:
2492:
2488:
2478:
2446:
2445:
2441:
2432:
2430:
2428:
2410:
2409:
2405:
2400:
2396:
2387:
2385:
2376:
2360:
2356:
2345:, 1977, 46–57.
2333:
2329:
2316:
2315:
2311:
2303:
2298:
2297:
2293:
2286:
2268:
2267:
2263:
2254:
2252:
2243:
2242:
2238:
2230:
2226:
2221:
2203:Action language
2199:
2191:
2089:Büchi automaton
2071:
2059:PSPACE-complete
2052:
1986:
1924:
1860:ψ ≡ ψ ∨ ( φ ∧
1845:ψ ≡ ψ ∨ ( φ ∧
1528:Distributivity
1520:
1464:
1463:
1440:
1377:
1376:
1353:
1294:
1293:
1223:
1222:
1161:
1160:
1110:
1109:
1058:
1057:
1042:Unary operators
794:
786:
782:
774:
764:
755:
751:
741:
732:
725:
721:
717:
713:
709:
705:
698:
694:
688:
635:
631:
627:
623:
619:
615:
610:
606:
602:
598:
592:
588:
584:
580:
570:
554:
550:
534:
530:
526:
514:
510:
499:
491:
479:
471:
467:
455:
443:
437:
427:
419:
411:
399:
391:
383:
379:
370:
362:
329:
318:
307:
293:
289:
285:
254:
120:modal operators
102:
28:
23:
22:
15:
12:
11:
5:
2689:
2687:
2679:
2678:
2676:Temporal logic
2673:
2663:
2662:
2659:
2658:
2648:
2635:
2630:
2623:
2622:External links
2620:
2617:
2616:
2601:
2551:
2534:Bowen Alpern,
2527:
2502:
2486:
2476:
2450:(2008). "From
2448:Moshe Y. Vardi
2439:
2426:
2403:
2394:
2363:Christel Baier
2354:
2327:
2309:
2291:
2284:
2261:
2236:
2223:
2222:
2220:
2217:
2216:
2215:
2210:
2205:
2198:
2195:
2190:
2187:
2186:
2185:
2170:
2166:
2165:
2161:counterexample
2156:
2155:
2102:
2098:
2097:
2084:
2083:
2075:
2070:
2067:
2055:Model checking
2051:
2048:
2047:
2046:
2023:
1994:Kamp's theorem
1985:
1982:
1962:
1961:
1946:
1935:
1923:
1920:
1917:
1916:
1914:
1900:
1885:
1884:
1869:
1854:
1838:
1837:
1822:
1809:
1795:
1794:
1786:
1785:
1774:
1763:
1752:
1749:
1748:
1737:
1726:
1715:
1703:
1702:
1690:
1678:
1666:
1657:
1656:
1648:
1647:
1645:
1630:
1621:(φ ∨ ψ) ≡ (ρ
1614:
1613:
1611:
1597:
1582:
1581:
1559:
1545:
1530:
1529:
1519:
1516:
1513:
1512:
1505:
1494:
1483:
1477:
1471:
1461:
1449:
1448:
1433:
1407:
1396:
1390:
1384:
1374:
1362:
1361:
1346:
1324:
1313:
1307:
1301:
1291:
1279:
1278:
1271:
1253:
1242:
1236:
1230:
1220:
1208:
1207:
1200:
1199:
1192:
1182:
1171:
1168:
1158:
1149:
1148:
1141:
1131:
1120:
1117:
1107:
1098:
1097:
1090:
1079:
1068:
1065:
1055:
1046:
1045:
1038:
1037:
1034:
1031:
1028:
1019:
1018:
937:strong release
933:
932:
905:
876:
793:
790:
789:
788:
784:
780:
772:
762:
757:
753:
749:
739:
734:
730:
723:
719:
715:
711:
707:
703:
696:
692:
686:
668:
667:
658:
637:
633:
629:
625:
621:
617:
613:
611:
608:
604:
600:
596:
594:
590:
586:
582:
578:
568:
552:
548:
532:
528:
524:
512:
508:
497:
489:
482:
481:
477:
469:
465:
453:
448:≥ 0 such that
441:
435:
429:
425:
417:
409:
400:
397:
389:
381:
377:
371:
368:
360:
354:
324:
316:
305:
291:
287:
283:
253:
250:
249:
248:
238:
228:
218:
208:
170:
169:
158:
101:
98:
77:. In terms of
73:, abbreviated
51:temporal logic
26:
24:
14:
13:
10:
9:
6:
4:
3:
2:
2688:
2677:
2674:
2672:
2669:
2668:
2666:
2656:
2652:
2649:
2647:
2643:
2640:of professor
2639:
2636:
2634:
2631:
2629:
2626:
2625:
2621:
2612:
2608:
2604:
2598:
2594:
2590:
2586:
2582:
2577:
2572:
2568:
2564:
2563:
2555:
2552:
2549:
2545:
2541:
2537:
2531:
2528:
2524:
2523:3-540-60915-6
2520:
2516:
2512:
2506:
2503:
2500:
2496:
2490:
2487:
2484:
2479:
2473:
2469:
2465:
2461:
2460:Orna Grumberg
2457:
2454:and Prior to
2453:
2449:
2443:
2440:
2429:
2427:9783642141614
2423:
2419:
2418:
2413:
2407:
2404:
2398:
2395:
2384:on 2010-12-04
2383:
2379:
2374:
2373:
2368:
2364:
2358:
2355:
2352:
2348:
2344:
2342:
2336:
2331:
2328:
2323:
2319:
2313:
2310:
2302:
2295:
2292:
2287:
2281:
2277:
2276:
2271:
2270:Dov M. Gabbay
2265:
2262:
2251:on 2017-04-30
2250:
2246:
2240:
2237:
2233:
2228:
2225:
2218:
2214:
2211:
2209:
2206:
2204:
2201:
2200:
2196:
2194:
2188:
2183:
2179:
2175:
2171:
2168:
2167:
2162:
2158:
2157:
2153:
2150:
2146:
2142:
2138:
2135:
2131:
2127:
2126:
2121:
2117:
2113:
2109:
2108:
2103:
2100:
2099:
2095:
2090:
2086:
2085:
2081:
2076:
2073:
2072:
2068:
2066:
2064:
2060:
2056:
2049:
2044:
2040:
2036:
2032:
2028:
2024:
2021:
2017:
2013:
2012:
2011:
2009:
2005:
2001:
1999:
1995:
1991:
1983:
1981:
1979:
1975:
1971:
1967:
1959:
1955:
1951:
1947:
1944:
1940:
1936:
1933:
1932:
1931:
1929:
1921:
1915:
1912:
1908:
1904:
1901:
1898:
1894:
1890:
1887:
1886:
1882:
1878:
1875:ψ ≡ ψ ∧ (φ ∨
1874:
1870:
1867:
1863:
1859:
1855:
1852:
1848:
1844:
1840:
1839:
1835:
1831:
1827:
1823:
1820:
1817:
1813:
1810:
1807:
1804:
1800:
1797:
1796:
1791:
1783:
1779:
1775:
1772:
1768:
1764:
1761:
1757:
1753:
1751:
1750:
1746:
1742:
1738:
1735:
1731:
1727:
1724:
1720:
1716:
1713:
1709:
1705:
1704:
1701:
1699:
1695:
1691:
1689:
1687:
1683:
1679:
1677:
1675:
1671:
1667:
1665:
1663:
1659:
1658:
1653:
1646:
1643:
1639:
1635:
1631:
1628:
1624:
1620:
1616:
1615:
1612:
1609:
1605:
1601:
1598:
1595:
1591:
1587:
1584:
1583:
1579:
1575:
1571:
1567:
1563:
1560:
1557:
1553:
1549:
1546:
1543:
1539:
1535:
1532:
1531:
1526:
1523:
1517:
1510:
1506:
1503:
1499:
1495:
1481:
1469:
1462:
1460:
1457:
1454:
1451:
1450:
1447:
1445:
1438:
1434:
1431:
1427:
1423:
1419:
1415:
1411:
1408:
1394:
1382:
1375:
1373:
1370:
1367:
1364:
1363:
1360:
1358:
1351:
1347:
1344:
1340:
1336:
1332:
1328:
1325:
1311:
1299:
1292:
1290:
1287:
1284:
1281:
1280:
1276:
1272:
1269:
1265:
1261:
1257:
1254:
1240:
1228:
1221:
1219:
1216:
1213:
1210:
1209:
1205:
1201:
1197:
1193:
1190:
1186:
1183:
1169:
1166:
1159:
1157:
1154:
1151:
1150:
1146:
1142:
1139:
1135:
1132:
1118:
1115:
1108:
1106:
1103:
1100:
1099:
1095:
1091:
1088:
1084:
1080:
1066:
1063:
1056:
1054:
1051:
1048:
1047:
1043:
1039:
1035:
1032:
1029:
1026:
1025:
1022:
1016:
1012:
1008:
1005:
1001:
998:
994:
990:
987:
983:
980:
976:
973:
970:
966:
962:
959:
955:
952:
949:
946:
945:
944:
942:
938:
930:
926:
922:
919:
915:
912:
909:
906:
903:
900:
897:
893:
890:
886:
883:
880:
877:
874:
870:
866:
863:
859:
856:
852:
848:
845:
841:
838:
834:
831:
828:
824:
821:
818:
815:
814:
813:
811:
807:
803:
799:
791:
778:
771:
768:
761:
758:
756:becomes true)
748:
745:
738:
735:
728:
701:
691:
685:
684:
683:
681:
677:
673:
666:
662:
659:
657:
653:
649:
645:
641:
638:
612:
595:
577:
576:
575:
572:
566:
562:
558:
551:. A formula
546:
542:
538:
522:
518:
511:) defined by
506:
503:
495:
487:
480:becomes true)
475:
463:
459:
451:
447:
440:
433:
430:
428:must be true)
423:
415:
408:
404:
401:
395:
387:
375:
372:
366:
358:
355:
352:
348:
344:
340:
337:
336:
335:
333:
327:
323:
319:
312:
308:
301:
297:
281:
277:
273:
269:
265:
261:
260:
251:
247:ighty release
246:
242:
239:
236:
232:
229:
226:
222:
219:
216:
212:
209:
206:
202:
199:
198:
197:
195:
191:
186:
182:
178:
175:is read as ne
174:
167:
163:
159:
156:
152:
148:
144:
143:
142:
140:
136:
132:
128:
124:
121:
118:
114:
110:
107:
99:
97:
95:
91:
86:
84:
80:
76:
72:
68:
64:
60:
56:
52:
49:
45:
41:
37:
33:
19:
2566:
2560:
2554:
2539:
2530:
2510:
2505:
2489:
2470:. Springer.
2467:
2464:Helmut Veith
2442:
2431:. Retrieved
2416:
2406:
2397:
2386:. Retrieved
2382:the original
2375:, MIT Press
2370:
2361:Sec. 5.1 of
2357:
2338:
2330:
2321:
2312:
2294:
2274:
2264:
2253:. Retrieved
2249:the original
2239:
2227:
2192:
2151:
2148:
2144:
2140:
2136:
2133:
2129:
2123:
2119:
2115:
2111:
2105:
2069:Applications
2053:
2042:
2038:
2034:
2030:
2026:
2019:
2015:
2002:
1987:
1973:
1969:
1965:
1963:
1957:
1953:
1949:
1942:
1938:
1927:
1925:
1910:
1906:
1902:
1896:
1892:
1888:
1880:
1876:
1872:
1865:
1861:
1857:
1850:
1846:
1842:
1833:
1829:
1825:
1818:
1815:
1811:
1805:
1802:
1798:
1781:
1777:
1770:
1766:
1759:
1755:
1744:
1740:
1733:
1729:
1722:
1718:
1711:
1707:
1697:
1693:
1692:
1685:
1681:
1680:
1673:
1669:
1668:
1664:is self-dual
1661:
1660:
1641:
1637:
1633:
1626:
1622:
1618:
1607:
1603:
1602:(φ ∧ ψ) ≡ (
1599:
1593:
1589:
1588:(φ ∨ ψ) ≡ (
1585:
1577:
1573:
1569:
1565:
1561:
1555:
1551:
1550:(φ ∧ ψ) ≡ (
1547:
1541:
1537:
1536:(φ ∨ ψ) ≡ (
1533:
1521:
1518:Equivalences
1501:
1497:
1458:
1455:
1452:
1441:
1429:
1425:
1421:
1417:
1416:has to hold
1413:
1409:
1371:
1368:
1365:
1354:
1342:
1338:
1334:
1330:
1326:
1288:
1285:
1282:
1267:
1263:
1262:has to hold
1259:
1255:
1217:
1214:
1211:
1188:
1184:
1155:
1152:
1137:
1133:
1104:
1101:
1086:
1082:
1052:
1049:
1033:Explanation
1020:
1014:
1010:
1006:
1003:
999:
996:
992:
988:
985:
981:
978:
974:
971:
968:
964:
960:
957:
953:
950:
947:
940:
936:
934:
928:
924:
920:
917:
913:
910:
907:
901:
898:
895:
891:
888:
884:
881:
878:
872:
868:
864:
861:
857:
854:
850:
846:
843:
839:
836:
832:
829:
826:
822:
819:
816:
809:
805:
801:
797:
795:
776:
769:
766:
759:
752:(eventually
746:
743:
736:
726:
699:
689:
679:
675:
671:
669:
664:
660:
655:
651:
647:
643:
639:
573:
564:
560:
556:
544:
540:
536:
531:. A formula
520:
516:
504:
493:
485:
483:
473:
461:
457:
449:
445:
438:
431:
424:t time step
421:
413:
406:
402:
393:
385:
373:
364:
356:
350:
346:
342:
338:
331:
325:
321:
314:
310:
303:
299:
295:
279:
263:
257:
255:
244:
240:
234:
230:
224:
220:
214:
210:
204:
203:for always (
200:
193:
189:
184:
180:
176:
172:
171:
165:
161:
154:
150:
146:
138:
134:
130:
126:
122:
108:
103:
87:
74:
70:
43:
39:
35:
29:
2335:Amir Pnueli
2174:preferences
1960:can appear.
1412:eak until:
537:satisfiable
183:is read as
94:Amir Pnueli
67:quantifiers
2665:Categories
2433:2014-07-30
2388:2011-05-17
2318:Kamp, Hans
2255:2012-03-19
2234:: page 175
2219:References
2189:Extensions
2037:¬q) ) or
798:weak until
543:such that
502:ω-language
420:(in the ne
2576:1406.6683
2122:), while
1780:ψ) ≡ (¬φ
1769:ψ) ≡ (¬φ
1743:ψ) ≡ (¬φ
1732:ψ) ≡ (¬φ
1482:φ
1470:ψ
1395:φ
1383:ψ
1312:φ
1300:ψ
1241:φ
1229:ψ
1187:lobally:
1170:φ
1167:◻
1119:φ
1116:◊
1067:φ
1064:◯
1030:Symbolic
259:satisfied
252:Semantics
237:eak until
164:ψ, and φ
96:in 1977.
2611:12538495
2483:preprint
2466:(eds.).
2320:(1968).
2197:See also
2164:formula.
2125:liveness
1930:, where
1905:φ ≡ φ ∨
1891:φ ≡ φ ∧
1700:are dual
1688:are dual
1676:are dual
1640:ρ) ∧ (ψ
1636:ρ ≡ (φ
1632:(φ ∧ ψ)
1625:φ) ∨ (ρ
1418:at least
1329:elease:
1264:at least
1136:inally:
1036:Diagram
1027:Textual
729:eleases
650:, where
460:< i,
278:2). Let
276:alphabet
207:lobally)
117:temporal
55:formulae
2644:at the
2581:Bibcode
2176:in the
2029:( p → (
1828:ψ ≡ φ
500:. The
46:) is a
2609:
2599:
2521:
2474:
2458:". In
2452:Church
2424:
2343:(FOCS)
2282:
2152:ψ
2145:ϕ
2137:ψ
2120:ϕ
2118:¬
2107:safety
1956:, and
1606:φ) ∧ (
1592:φ) ∨ (
1568:ψ)≡ (
1554:φ) ∧ (
1540:φ) ∨ (
1420:until
1266:until
1258:ntil:
678:, and
628:) ∧ (
309:. Let
272:ω-word
227:elease
217:inally
192:, and
179:t and
133:) and
111:, the
100:Syntax
2607:S2CID
2571:arXiv
2304:(PDF)
2045:(p)).
1974:false
1943:false
1883:ψ) )
1776:¬ (φ
1765:¬ (φ
1739:¬ (φ
1728:¬ (φ
1424:; if
967:) ≡ (
956:≡ ¬(¬
860:) ≡
767:false
695:≡ ¬(¬
661:false
585:≡ ¬(¬
557:valid
492:when
476:ntil
274:over
194:false
153:then
59:paths
48:modal
32:logic
2655:Spot
2597:ISBN
2567:7908
2519:ISBN
2472:ISBN
2422:ISBN
2365:and
2280:ISBN
2033:q ∧
2008:CTL*
1970:true
1939:true
1868:ψ) )
1853:ψ) )
1814:φ ≡
1801:φ ≡
1784:¬ψ)
1758:φ ≡
1747:¬ψ)
1721:φ ≡
1710:φ ≡
1696:and
1684:and
1672:and
1002:) ≡
977:) ∧
935:The
835:) ∨
808:and
744:true
706:) (
665:true
640:true
515:is {
302:) =
270:(an
243:for
233:for
223:for
213:for
190:true
63:CTL*
2589:doi
2456:PSL
2347:doi
2139:or
2022:p).
1879:(φ
1864:(φ
1849:(φ
1836:ψ)
1832:(φ
1773:¬ψ)
1736:¬ψ)
1580:ψ)
1572:φ)
1564:(φ
1085:t:
894:∧ (
825:≡ (
775:≡ ¬
765:≡
742:≡
663:≡ ¬
646:∨ ¬
620:≡ (
603:≡ ¬
589:∨ ¬
555:is
535:is
412:if
392:or
384:if
363:if
359:⊨ ¬
353:(0)
345:if
282:= a
145:if
129:or
75:PTL
44:LTL
38:or
30:In
2667::
2605:.
2595:.
2587:.
2579:.
2542:,
2538:,
2462:;
2420:.
2369:,
2134:GF
2065:.
2043:EF
2039:AG
2035:EX
2031:EX
2027:AG
2000:.
1980:.
1972:,
1968:,
1952:,
1941:,
1913:φ)
1899:φ)
1871:φ
1856:φ
1841:φ
1824:φ
1762:¬φ
1725:¬φ
1714:¬φ
1644:ρ)
1629:ψ)
1617:ρ
1610:ψ)
1596:ψ)
1558:ψ)
1544:ψ)
1206::
1081:ne
1044::
1013:∧
995:∧
984:≡
927:∧
916:≡
887:≡
871:∨
853:∨
842:≡
733:.)
674:,
656:AP
654:∈
642:≡
632:→
624:→
616:↔
607:∨
599:→
581:∧
571:.
567:⊨
547:⊨
523:⊨
519:|
496:⊨
464:⊨
452:⊨
434:⊨
416:⊨
405:⊨
396:⊨
388:⊨
380:∨
376:⊨
367:⊭
349:∈
341:⊨
328:+1
313:=
290:,a
286:,a
264:AP
151:AP
149:∈
139:AP
109:AP
85:.
34:,
2613:.
2591::
2583::
2573::
2525:.
2480:.
2436:.
2391:.
2349::
2288:.
2258:.
2184:.
2149:F
2147:→
2143:(
2141:G
2132:(
2116:G
2114:(
2041:(
2020:G
2018:(
2016:F
1966:R
1958:R
1954:U
1950:X
1911:F
1909:(
1907:X
1903:F
1897:G
1895:(
1893:X
1889:G
1881:R
1877:X
1873:R
1866:W
1862:X
1858:W
1851:U
1847:X
1843:U
1834:U
1830:U
1826:U
1821:φ
1819:G
1816:G
1812:G
1808:φ
1806:F
1803:F
1799:F
1782:W
1778:M
1771:U
1767:R
1760:F
1756:G
1754:¬
1745:M
1741:W
1734:R
1730:U
1723:G
1719:F
1717:¬
1712:X
1708:X
1706:¬
1698:M
1694:W
1686:R
1682:U
1674:G
1670:F
1662:X
1642:U
1638:U
1634:U
1627:U
1623:U
1619:U
1608:G
1604:G
1600:G
1594:F
1590:F
1586:F
1578:X
1576:(
1574:U
1570:X
1566:U
1562:X
1556:X
1552:X
1548:X
1542:X
1538:X
1534:X
1502:ψ
1498:φ
1476:M
1459:φ
1456:M
1453:ψ
1430:ψ
1426:φ
1422:φ
1414:ψ
1410:W
1389:W
1372:φ
1369:W
1366:ψ
1343:φ
1339:ψ
1335:ψ
1331:φ
1327:R
1306:R
1289:φ
1286:R
1283:ψ
1268:φ
1260:ψ
1256:U
1235:U
1218:φ
1215:U
1212:ψ
1189:φ
1185:G
1156:φ
1153:G
1138:φ
1134:F
1105:φ
1102:F
1087:φ
1083:X
1053:φ
1050:X
1017:)
1015:φ
1011:ψ
1009:(
1007:U
1004:φ
1000:ψ
997:F
993:φ
991:(
989:R
986:ψ
982:ψ
979:F
975:φ
972:R
969:ψ
965:φ
963:¬
961:W
958:ψ
954:φ
951:M
948:ψ
941:M
931:)
929:ψ
925:φ
923:(
921:W
918:φ
914:φ
911:R
908:ψ
904:)
902:φ
899:W
896:ψ
892:φ
889:F
885:φ
882:U
879:ψ
875:)
873:ψ
869:φ
867:(
865:R
862:φ
858:ψ
855:G
851:φ
849:(
847:U
844:ψ
840:ψ
837:G
833:φ
830:U
827:ψ
823:φ
820:W
817:ψ
810:R
806:U
802:W
785:ψ
783:(
781:ψ
779:¬
777:F
773:ψ
770:R
763:ψ
760:G
754:ψ
750:ψ
747:U
740:ψ
737:F
731:φ
727:r
724:ψ
720:φ
716:ψ
712:ψ
708:φ
704:φ
702:¬
700:U
697:ψ
693:φ
690:R
687:ψ
680:G
676:F
672:R
652:p
648:p
644:p
636:)
634:φ
630:ψ
626:ψ
622:φ
618:ψ
614:φ
609:ψ
605:φ
601:ψ
597:φ
593:)
591:ψ
587:φ
583:ψ
579:φ
569:ψ
565:w
561:w
553:ψ
549:ψ
545:w
541:w
533:ψ
529:ψ
525:ψ
521:w
517:w
513:ψ
509:ψ
507:(
505:L
498:ψ
494:w
490:ψ
486:w
478:ψ
474:u
470:φ
468:(
466:φ
462:w
458:k
454:ψ
450:w
446:i
442:ψ
439:U
436:φ
432:w
426:ψ
422:x
418:ψ
414:w
410:ψ
407:X
403:w
398:ψ
394:w
390:φ
386:w
382:ψ
378:φ
374:w
369:ψ
365:w
361:ψ
357:w
351:w
347:p
343:p
339:w
332:w
326:i
322:a
320:,
317:i
315:a
311:w
306:i
304:a
300:i
298:(
296:w
292:2
288:1
284:0
280:w
245:m
241:M
235:w
231:W
225:r
221:R
215:f
211:F
205:g
201:G
185:u
181:U
177:x
173:X
166:U
162:X
155:p
147:p
135:U
131:N
127:O
123:X
42:(
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
