2526:
2447:
1610:
1401:
2298:
1684:
1475:
2247:
2086:
1276:
2136:
1769:
1560:
1231:
1193:
738:
524:
1815:
1726:
1517:
1902:
2811:
1955:
1352:
1314:
863:
476:
1115:
2609:
1034:
2029:
1998:
1641:
1432:
399:
2773:
2721:
1856:
1150:
2679:
2161:
2631:
975:
293:
2365:
670:
594:
574:
335:
241:
146:
1001:
550:
361:
172:
2831:
2741:
2345:
2181:
1074:
903:
883:
785:
261:
212:
2851:
943:
825:
2207:
2651:
2546:
2318:
2106:
2049:
1054:
923:
805:
762:
690:
650:
622:
192:
86:
2452:
2373:
1567:
1358:
2897:
1076:
being a comparison operator such as <, ≤, =, ≥ or >: We first consider formulas whose main operator also belongs to LTL:
2370:
TPTL is strictly more expressive than MTL both over timed words and over signals. Over timed words, no MTL formula is equivalent to
36:(LTL) in which variables are introduced to measure times between two events. For example, while LTL allows to state that each event
2252:
2215:
2054:
1969:
is another extension of LTL that allows measurement of time. Instead of adding variables, it adds an infinity of operators
1237:
2111:
1198:
1157:
699:
481:
1776:
1646:
1437:
1863:
1731:
1522:
2778:
1907:
1319:
1281:
830:
446:
1082:
2989:
2984:
2873:
601:
2559:
693:
93:
65:
1006:
2324:
2003:
1972:
1966:
366:
61:
33:
2746:
2684:
1820:
1120:
2656:
1689:
1480:
2614:
2949:
2907:
948:
266:
103:
2350:
428:
is not considered to be a part of MTL syntax. It will instead be defined from other operators.
2893:
1615:
1406:
655:
579:
559:
302:
220:
125:
2958:
2940:
2885:
980:
529:
340:
151:
21:
2816:
2726:
2330:
2166:
1059:
888:
868:
770:
246:
197:
2919:
2836:
928:
810:
2877:
2186:
2141:
2636:
2531:
2303:
2091:
2034:
1039:
908:
790:
747:
675:
635:
607:
177:
113:
110:
71:
17:
2978:
2936:
2882:
FSTTCS 2005: Foundations of
Software Technology and Theoretical Computer Science
2521:{\displaystyle x.\Diamond (a\land x\leq 1\land \Box (x\leq 1\implies \neg b))}
2442:{\displaystyle \Box (a\implies x.\Diamond (b\land \Diamond (c\land x\leq 5)))}
597:
2878:"Developments in Data Structure Research During the First 25 Years of FSTTCS"
2267:
68:
variables can be introduced and compared to constants. Formally, given a set
2963:
2944:
2528:, which states that the last atomic proposition before time point 1 is an
1605:{\displaystyle \gamma ,t,\nu \models \phi \mathbin {\mathcal {S}} \psi }
1396:{\displaystyle \gamma ,t,\nu \models \phi \mathbin {\mathcal {U}} \psi }
2889:
2884:. Lecture Notes in Computer Science. Vol. 3821. p. 436.
2051:
an interval of non-negative number. The semantics of the formula
214:
a comparison operator such as <, ≤, =, ≥ or >.
2212:
TPTL is as least as expressive as MTL. Indeed, the MTL formula
2833:
is considered as a TPTL formula with non-strict operator, and
767:
We are now going to explain what it means for a TPTL formula
2229:
2225:
2120:
2068:
2064:
2010:
1979:
1594:
1385:
499:
2868:
2866:
2323:
It follows that any other operator introduced in the page
2108:
is essentially the same than the semantics of the formula
624:
is either a discrete subset or an interval containing 0.
2293:{\displaystyle x.\phi {\mathcal {(}}x\in I\land \psi )}
2449:. Over signal, there are no MTL formula equivalent to
2242:{\displaystyle \phi \mathbin {\mathcal {U_{I}}} \psi }
2081:{\displaystyle \phi \mathbin {\mathcal {U_{I}}} \psi }
2839:
2819:
2781:
2749:
2729:
2687:
2659:
2639:
2617:
2562:
2534:
2455:
2376:
2353:
2333:
2306:
2255:
2218:
2189:
2169:
2144:
2114:
2094:
2057:
2037:
2006:
1975:
1910:
1866:
1823:
1779:
1734:
1692:
1649:
1618:
1570:
1525:
1483:
1440:
1409:
1361:
1322:
1284:
1271:{\displaystyle \gamma ,t,\nu \models \phi \lor \psi }
1240:
1201:
1160:
1123:
1085:
1062:
1042:
1009:
983:
951:
931:
911:
891:
871:
833:
813:
793:
773:
750:
702:
678:
658:
638:
610:
582:
562:
532:
484:
449:
369:
343:
305:
269:
249:
223:
200:
180:
154:
128:
74:
2653:. We can consider such a word using the set of time
478:, which intuitively represents a set of times. Let
401:; and similarly for every other kind of intervals.
44:, TPTL furthermore allows to give a time limit for
2845:
2825:
2805:
2767:
2735:
2715:
2673:
2645:
2625:
2603:
2540:
2520:
2441:
2359:
2339:
2312:
2292:
2241:
2201:
2175:
2155:
2131:{\displaystyle \phi \mathbin {\mathcal {U}} \psi }
2130:
2100:
2080:
2043:
2023:
1992:
1949:
1896:
1850:
1809:
1763:
1720:
1678:
1635:
1604:
1554:
1511:
1469:
1426:
1395:
1346:
1308:
1270:
1225:
1187:
1144:
1109:
1068:
1048:
1028:
995:
969:
937:
917:
897:
877:
857:
819:
799:
779:
756:
732:
684:
664:
644:
616:
588:
568:
544:
518:
470:
393:
355:
329:
287:
255:
235:
206:
186:
166:
140:
80:
1226:{\displaystyle \gamma ,t,\nu \not \models \phi }
1188:{\displaystyle \gamma ,t,\nu \models \neg \phi }
2853:is the only function defined on the empty set.
733:{\displaystyle \nu :X\to \mathbb {R} _{\geq 0}}
556:. A model of a TPTL formula is such a function
519:{\displaystyle \gamma :T\to {\mathcal {P}}(AP)}
2876:; Chevalier, Fabrice; Markey, Nicolas (2005).
1810:{\displaystyle \gamma ,t,\nu \models x\sim c}
1679:{\displaystyle \gamma ,t'',\nu \models \psi }
1470:{\displaystyle \gamma ,t'',\nu \models \psi }
8:
1897:{\displaystyle \gamma ,t,\nu \models y.\xi }
1764:{\displaystyle \gamma ,t',\nu \models \phi }
1555:{\displaystyle \gamma ,t',\nu \models \phi }
964:
958:
282:
276:
2806:{\displaystyle \gamma ,i,\nu \models \phi }
1950:{\displaystyle \gamma ,t,\nu \models \phi }
1347:{\displaystyle \gamma ,t,\nu \models \psi }
1309:{\displaystyle \gamma ,t,\nu \models \phi }
858:{\displaystyle \gamma ,t,\nu \models \phi }
471:{\displaystyle T\subseteq \mathbb {R} _{+}}
2505:
2501:
2390:
2386:
526:a function that associates to each moment
435:is a formula over an empty set of clocks.
2962:
2838:
2818:
2780:
2748:
2728:
2707:
2686:
2667:
2666:
2658:
2638:
2619:
2618:
2616:
2586:
2573:
2561:
2533:
2454:
2375:
2352:
2332:
2305:
2266:
2265:
2254:
2228:
2223:
2222:
2217:
2188:
2168:
2143:
2119:
2118:
2113:
2093:
2067:
2062:
2061:
2056:
2036:
2015:
2009:
2008:
2005:
1984:
1978:
1977:
1974:
1909:
1865:
1822:
1778:
1733:
1691:
1648:
1617:
1593:
1592:
1569:
1524:
1482:
1439:
1408:
1384:
1383:
1360:
1321:
1283:
1239:
1200:
1159:
1122:
1084:
1061:
1041:
1017:
1016:
1008:
982:
950:
930:
910:
890:
870:
832:
812:
792:
772:
749:
721:
717:
716:
701:
677:
657:
637:
609:
581:
561:
531:
498:
497:
483:
462:
458:
457:
448:
368:
342:
304:
268:
248:
222:
199:
179:
153:
127:
73:
2931:
2929:
2862:
1110:{\displaystyle \gamma ,t,\nu \models l}
905:be two formulas over the set of clocks
2915:
2905:
2367:can also be defined as TPTL formulas.
2604:{\displaystyle w=a_{0},a_{1},\dots ,}
2138:, with the constraints that the time
1021:
1018:
363:is considered as an abbreviation for
7:
2556:A standard (untimed) infinite word
1029:{\displaystyle l\in {\mathtt {AP}}}
408:is built as the future fragment of
40:is eventually followed by an event
32:) is an extension of propositional
2506:
2249:is equivalent to the TPTL formula
2024:{\displaystyle {\mathcal {S}}_{I}}
1993:{\displaystyle {\mathcal {U}}_{I}}
1179:
394:{\displaystyle x>a\land x<b}
263:a TPTL formula with set of clocks
26:timed propositional temporal logic
14:
2183:must hold occurs in the interval
945:a formula over the set of clocks
217:a freeze quantification operator
88:of clocks, MTL is built up from:
2768:{\displaystyle w,i\models \phi }
2716:{\displaystyle \gamma (i)=a_{i}}
1851:{\displaystyle t-\nu (y)\sim c}
1145:{\displaystyle l\in \gamma (t)}
2697:
2691:
2674:{\displaystyle T=\mathbb {N} }
2515:
2512:
2502:
2489:
2465:
2436:
2433:
2430:
2412:
2400:
2387:
2380:
2287:
1938:
1932:
1926:
1839:
1833:
1721:{\displaystyle t''<t'<t}
1512:{\displaystyle t<t'<t''}
1139:
1133:
712:
513:
504:
494:
324:
312:
1:
2626:{\displaystyle \mathbb {N} }
424:Note that the next operator
416:the temporal modal operator
970:{\displaystyle X\cup \{y\}}
552:a set of propositions from
288:{\displaystyle X\cup \{x\}}
3006:
2743:an arbitrary LTL formula,
2945:"A really temporal logic"
2360:{\displaystyle \Diamond }
1636:{\displaystyle t''<t}
1427:{\displaystyle t<t''}
64:, in which furthermore,
60:is defined similarly to
1686:and such that for each
1477:and such that for each
665:{\displaystyle \gamma }
589:{\displaystyle \gamma }
569:{\displaystyle \gamma }
330:{\displaystyle I=(a,b)}
236:{\displaystyle x.\phi }
141:{\displaystyle x\sim c}
94:propositional variables
58:future fragment of TPTL
2847:
2827:
2807:
2769:
2737:
2717:
2675:
2647:
2627:
2605:
2542:
2522:
2443:
2361:
2341:
2314:
2294:
2243:
2203:
2177:
2157:
2132:
2102:
2082:
2045:
2025:
1994:
1951:
1898:
1852:
1811:
1765:
1722:
1680:
1637:
1612:holds if there exists
1606:
1556:
1513:
1471:
1428:
1403:holds if there exists
1397:
1348:
1310:
1272:
1227:
1189:
1146:
1111:
1070:
1050:
1030:
997:
996:{\displaystyle x\in X}
971:
939:
919:
899:
879:
859:
821:
801:
781:
758:
734:
686:
666:
646:
618:
590:
570:
546:
545:{\displaystyle t\in T}
520:
472:
395:
357:
356:{\displaystyle x\in I}
331:
289:
257:
237:
208:
188:
168:
167:{\displaystyle x\in X}
142:
82:
2964:10.1145/174644.174651
2848:
2828:
2826:{\displaystyle \phi }
2808:
2770:
2738:
2736:{\displaystyle \phi }
2718:
2676:
2648:
2628:
2606:
2543:
2523:
2444:
2362:
2342:
2340:{\displaystyle \Box }
2315:
2295:
2244:
2204:
2178:
2176:{\displaystyle \psi }
2158:
2133:
2103:
2083:
2046:
2026:
1995:
1967:Metric temporal logic
1962:Metric temporal logic
1952:
1899:
1853:
1812:
1766:
1723:
1681:
1638:
1607:
1557:
1514:
1472:
1429:
1398:
1349:
1311:
1273:
1228:
1190:
1147:
1112:
1071:
1069:{\displaystyle \sim }
1051:
1031:
998:
972:
940:
920:
900:
898:{\displaystyle \psi }
880:
878:{\displaystyle \phi }
860:
827:. This is denoted by
822:
802:
782:
780:{\displaystyle \phi }
759:
735:
687:
667:
647:
619:
591:
571:
547:
521:
473:
396:
358:
332:
290:
258:
256:{\displaystyle \phi }
238:
209:
207:{\displaystyle \sim }
189:
169:
143:
83:
62:linear temporal logic
34:linear temporal logic
2941:Henzinger, Thomas A.
2846:{\displaystyle \nu }
2837:
2817:
2779:
2747:
2727:
2723:. In this case, for
2685:
2657:
2637:
2615:
2560:
2532:
2453:
2374:
2351:
2331:
2304:
2253:
2216:
2187:
2167:
2142:
2112:
2092:
2055:
2035:
2004:
1973:
1908:
1864:
1821:
1777:
1732:
1690:
1647:
1616:
1568:
1523:
1481:
1438:
1407:
1359:
1320:
1282:
1238:
1199:
1158:
1121:
1083:
1060:
1040:
1007:
981:
949:
938:{\displaystyle \xi }
929:
909:
889:
869:
831:
820:{\displaystyle \nu }
811:
791:
771:
748:
700:
676:
656:
636:
608:
580:
560:
530:
482:
447:
367:
341:
303:
267:
247:
221:
198:
178:
152:
126:
72:
2681:, and the function
2611:is a function from
2552:Comparison with LTL
2320:is a new variable.
2202:{\displaystyle t+I}
2156:{\displaystyle t''}
122:a clock comparison
2950:Journal of the ACM
2890:10.1007/11590156_3
2843:
2823:
2803:
2765:
2733:
2713:
2671:
2643:
2623:
2601:
2538:
2518:
2439:
2357:
2337:
2310:
2290:
2239:
2199:
2173:
2153:
2128:
2098:
2078:
2041:
2021:
1990:
1947:
1894:
1848:
1807:
1761:
1718:
1676:
1633:
1602:
1552:
1509:
1467:
1424:
1393:
1344:
1306:
1268:
1223:
1185:
1142:
1107:
1066:
1046:
1026:
993:
967:
935:
915:
895:
875:
855:
817:
797:
777:
754:
730:
682:
662:
642:
614:
604:. In those cases,
586:
566:
542:
516:
468:
412:and also contains
391:
353:
327:
285:
253:
233:
204:
184:
164:
138:
78:
2899:978-3-540-30495-1
2646:{\displaystyle A}
2541:{\displaystyle a}
2313:{\displaystyle x}
2101:{\displaystyle t}
2044:{\displaystyle I}
1049:{\displaystyle c}
918:{\displaystyle X}
800:{\displaystyle t}
757:{\displaystyle X}
685:{\displaystyle X}
672:be as above. Let
645:{\displaystyle T}
617:{\displaystyle T}
299:Furthermore, for
187:{\displaystyle c}
104:logical operators
81:{\displaystyle X}
2997:
2969:
2968:
2966:
2933:
2924:
2923:
2917:
2913:
2911:
2903:
2874:Bouyer, Patricia
2870:
2852:
2850:
2849:
2844:
2832:
2830:
2829:
2824:
2812:
2810:
2809:
2804:
2774:
2772:
2771:
2766:
2742:
2740:
2739:
2734:
2722:
2720:
2719:
2714:
2712:
2711:
2680:
2678:
2677:
2672:
2670:
2652:
2650:
2649:
2644:
2632:
2630:
2629:
2624:
2622:
2610:
2608:
2607:
2602:
2591:
2590:
2578:
2577:
2547:
2545:
2544:
2539:
2527:
2525:
2524:
2519:
2448:
2446:
2445:
2440:
2366:
2364:
2363:
2358:
2346:
2344:
2343:
2338:
2319:
2317:
2316:
2311:
2299:
2297:
2296:
2291:
2271:
2270:
2248:
2246:
2245:
2240:
2235:
2234:
2233:
2232:
2208:
2206:
2205:
2200:
2182:
2180:
2179:
2174:
2162:
2160:
2159:
2154:
2152:
2137:
2135:
2134:
2129:
2124:
2123:
2107:
2105:
2104:
2099:
2087:
2085:
2084:
2079:
2074:
2073:
2072:
2071:
2050:
2048:
2047:
2042:
2030:
2028:
2027:
2022:
2020:
2019:
2014:
2013:
1999:
1997:
1996:
1991:
1989:
1988:
1983:
1982:
1956:
1954:
1953:
1948:
1903:
1901:
1900:
1895:
1857:
1855:
1854:
1849:
1816:
1814:
1813:
1808:
1770:
1768:
1767:
1762:
1748:
1727:
1725:
1724:
1719:
1711:
1700:
1685:
1683:
1682:
1677:
1663:
1642:
1640:
1639:
1634:
1626:
1611:
1609:
1608:
1603:
1598:
1597:
1561:
1559:
1558:
1553:
1539:
1518:
1516:
1515:
1510:
1508:
1497:
1476:
1474:
1473:
1468:
1454:
1433:
1431:
1430:
1425:
1423:
1402:
1400:
1399:
1394:
1389:
1388:
1353:
1351:
1350:
1345:
1315:
1313:
1312:
1307:
1278:holds if either
1277:
1275:
1274:
1269:
1232:
1230:
1229:
1224:
1194:
1192:
1191:
1186:
1151:
1149:
1148:
1143:
1116:
1114:
1113:
1108:
1075:
1073:
1072:
1067:
1055:
1053:
1052:
1047:
1035:
1033:
1032:
1027:
1025:
1024:
1002:
1000:
999:
994:
976:
974:
973:
968:
944:
942:
941:
936:
924:
922:
921:
916:
904:
902:
901:
896:
884:
882:
881:
876:
864:
862:
861:
856:
826:
824:
823:
818:
807:for a valuation
806:
804:
803:
798:
787:to hold at time
786:
784:
783:
778:
763:
761:
760:
755:
739:
737:
736:
731:
729:
728:
720:
691:
689:
688:
683:
671:
669:
668:
663:
651:
649:
648:
643:
623:
621:
620:
615:
595:
593:
592:
587:
575:
573:
572:
567:
551:
549:
548:
543:
525:
523:
522:
517:
503:
502:
477:
475:
474:
469:
467:
466:
461:
400:
398:
397:
392:
362:
360:
359:
354:
336:
334:
333:
328:
294:
292:
291:
286:
262:
260:
259:
254:
242:
240:
239:
234:
213:
211:
210:
205:
193:
191:
190:
185:
173:
171:
170:
165:
147:
145:
144:
139:
92:a finite set of
87:
85:
84:
79:
22:computer science
3005:
3004:
3000:
2999:
2998:
2996:
2995:
2994:
2975:
2974:
2973:
2972:
2935:
2934:
2927:
2914:
2904:
2900:
2872:
2871:
2864:
2859:
2835:
2834:
2815:
2814:
2777:
2776:
2775:if and only if
2745:
2744:
2725:
2724:
2703:
2683:
2682:
2655:
2654:
2635:
2634:
2613:
2612:
2582:
2569:
2558:
2557:
2554:
2530:
2529:
2451:
2450:
2372:
2371:
2349:
2348:
2329:
2328:
2302:
2301:
2251:
2250:
2224:
2214:
2213:
2185:
2184:
2165:
2164:
2145:
2140:
2139:
2110:
2109:
2090:
2089:
2063:
2053:
2052:
2033:
2032:
2007:
2002:
2001:
1976:
1971:
1970:
1964:
1906:
1905:
1862:
1861:
1819:
1818:
1775:
1774:
1741:
1730:
1729:
1704:
1693:
1688:
1687:
1656:
1645:
1644:
1619:
1614:
1613:
1566:
1565:
1532:
1521:
1520:
1501:
1490:
1479:
1478:
1447:
1436:
1435:
1416:
1405:
1404:
1357:
1356:
1318:
1317:
1280:
1279:
1236:
1235:
1197:
1196:
1156:
1155:
1119:
1118:
1081:
1080:
1058:
1057:
1038:
1037:
1005:
1004:
979:
978:
947:
946:
927:
926:
907:
906:
887:
886:
867:
866:
829:
828:
809:
808:
789:
788:
769:
768:
746:
745:
742:clock valuation
715:
698:
697:
674:
673:
654:
653:
634:
633:
630:
606:
605:
578:
577:
558:
557:
528:
527:
480:
479:
456:
445:
444:
441:
365:
364:
339:
338:
301:
300:
265:
264:
245:
244:
219:
218:
196:
195:
176:
175:
150:
149:
124:
123:
70:
69:
54:
12:
11:
5:
3003:
3001:
2993:
2992:
2990:Model checking
2987:
2985:Temporal logic
2977:
2976:
2971:
2970:
2957:(1): 181–203.
2925:
2916:|journal=
2898:
2861:
2860:
2858:
2855:
2842:
2822:
2802:
2799:
2796:
2793:
2790:
2787:
2784:
2764:
2761:
2758:
2755:
2752:
2732:
2710:
2706:
2702:
2699:
2696:
2693:
2690:
2669:
2665:
2662:
2642:
2621:
2600:
2597:
2594:
2589:
2585:
2581:
2576:
2572:
2568:
2565:
2553:
2550:
2537:
2517:
2514:
2511:
2508:
2504:
2500:
2497:
2494:
2491:
2488:
2485:
2482:
2479:
2476:
2473:
2470:
2467:
2464:
2461:
2458:
2438:
2435:
2432:
2429:
2426:
2423:
2420:
2417:
2414:
2411:
2408:
2405:
2402:
2399:
2396:
2393:
2389:
2385:
2382:
2379:
2356:
2336:
2309:
2289:
2286:
2283:
2280:
2277:
2274:
2269:
2264:
2261:
2258:
2238:
2231:
2227:
2221:
2198:
2195:
2192:
2172:
2151:
2148:
2127:
2122:
2117:
2097:
2077:
2070:
2066:
2060:
2040:
2018:
2012:
1987:
1981:
1963:
1960:
1959:
1958:
1946:
1943:
1940:
1937:
1934:
1931:
1928:
1925:
1922:
1919:
1916:
1913:
1893:
1890:
1887:
1884:
1881:
1878:
1875:
1872:
1869:
1859:
1847:
1844:
1841:
1838:
1835:
1832:
1829:
1826:
1806:
1803:
1800:
1797:
1794:
1791:
1788:
1785:
1782:
1772:
1760:
1757:
1754:
1751:
1747:
1744:
1740:
1737:
1717:
1714:
1710:
1707:
1703:
1699:
1696:
1675:
1672:
1669:
1666:
1662:
1659:
1655:
1652:
1632:
1629:
1625:
1622:
1601:
1596:
1591:
1588:
1585:
1582:
1579:
1576:
1573:
1563:
1551:
1548:
1545:
1542:
1538:
1535:
1531:
1528:
1507:
1504:
1500:
1496:
1493:
1489:
1486:
1466:
1463:
1460:
1457:
1453:
1450:
1446:
1443:
1422:
1419:
1415:
1412:
1392:
1387:
1382:
1379:
1376:
1373:
1370:
1367:
1364:
1354:
1343:
1340:
1337:
1334:
1331:
1328:
1325:
1305:
1302:
1299:
1296:
1293:
1290:
1287:
1267:
1264:
1261:
1258:
1255:
1252:
1249:
1246:
1243:
1233:
1222:
1219:
1216:
1213:
1210:
1207:
1204:
1184:
1181:
1178:
1175:
1172:
1169:
1166:
1163:
1153:
1141:
1138:
1135:
1132:
1129:
1126:
1106:
1103:
1100:
1097:
1094:
1091:
1088:
1065:
1045:
1023:
1020:
1015:
1012:
992:
989:
986:
966:
963:
960:
957:
954:
934:
914:
894:
874:
854:
851:
848:
845:
842:
839:
836:
816:
796:
776:
753:
727:
724:
719:
714:
711:
708:
705:
681:
661:
641:
629:
626:
613:
585:
565:
541:
538:
535:
515:
512:
509:
506:
501:
496:
493:
490:
487:
465:
460:
455:
452:
440:
437:
433:closed formula
422:
421:
390:
387:
384:
381:
378:
375:
372:
352:
349:
346:
326:
323:
320:
317:
314:
311:
308:
297:
296:
284:
281:
278:
275:
272:
252:
232:
229:
226:
215:
203:
183:
163:
160:
157:
137:
134:
131:
120:
114:modal operator
107:
100:
77:
53:
50:
18:model checking
13:
10:
9:
6:
4:
3:
2:
3002:
2991:
2988:
2986:
2983:
2982:
2980:
2965:
2960:
2956:
2952:
2951:
2946:
2942:
2938:
2932:
2930:
2926:
2921:
2909:
2901:
2895:
2891:
2887:
2883:
2879:
2875:
2869:
2867:
2863:
2856:
2854:
2840:
2820:
2800:
2797:
2794:
2791:
2788:
2785:
2782:
2762:
2759:
2756:
2753:
2750:
2730:
2708:
2704:
2700:
2694:
2688:
2663:
2660:
2640:
2598:
2595:
2592:
2587:
2583:
2579:
2574:
2570:
2566:
2563:
2551:
2549:
2535:
2509:
2498:
2495:
2492:
2486:
2483:
2480:
2477:
2474:
2471:
2468:
2462:
2459:
2456:
2427:
2424:
2421:
2418:
2415:
2409:
2406:
2403:
2397:
2394:
2391:
2383:
2377:
2368:
2354:
2334:
2326:
2321:
2307:
2284:
2281:
2278:
2275:
2272:
2262:
2259:
2256:
2236:
2219:
2210:
2196:
2193:
2190:
2170:
2149:
2146:
2125:
2115:
2095:
2088:at some time
2075:
2058:
2038:
2016:
1985:
1968:
1961:
1944:
1941:
1935:
1929:
1923:
1920:
1917:
1914:
1911:
1891:
1888:
1885:
1882:
1879:
1876:
1873:
1870:
1867:
1860:
1845:
1842:
1836:
1830:
1827:
1824:
1804:
1801:
1798:
1795:
1792:
1789:
1786:
1783:
1780:
1773:
1758:
1755:
1752:
1749:
1745:
1742:
1738:
1735:
1715:
1712:
1708:
1705:
1701:
1697:
1694:
1673:
1670:
1667:
1664:
1660:
1657:
1653:
1650:
1630:
1627:
1623:
1620:
1599:
1589:
1586:
1583:
1580:
1577:
1574:
1571:
1564:
1549:
1546:
1543:
1540:
1536:
1533:
1529:
1526:
1505:
1502:
1498:
1494:
1491:
1487:
1484:
1464:
1461:
1458:
1455:
1451:
1448:
1444:
1441:
1420:
1417:
1413:
1410:
1390:
1380:
1377:
1374:
1371:
1368:
1365:
1362:
1355:
1341:
1338:
1335:
1332:
1329:
1326:
1323:
1303:
1300:
1297:
1294:
1291:
1288:
1285:
1265:
1262:
1259:
1256:
1253:
1250:
1247:
1244:
1241:
1234:
1220:
1217:
1214:
1211:
1208:
1205:
1202:
1182:
1176:
1173:
1170:
1167:
1164:
1161:
1154:
1136:
1130:
1127:
1124:
1104:
1101:
1098:
1095:
1092:
1089:
1086:
1079:
1078:
1077:
1063:
1056:a number and
1043:
1013:
1010:
990:
987:
984:
961:
955:
952:
932:
912:
892:
872:
852:
849:
846:
843:
840:
837:
834:
814:
794:
774:
765:
751:
743:
725:
722:
709:
706:
703:
695:
679:
659:
639:
627:
625:
611:
603:
599:
583:
563:
555:
539:
536:
533:
510:
507:
491:
488:
485:
463:
453:
450:
438:
436:
434:
429:
427:
419:
415:
414:
413:
411:
407:
402:
388:
385:
382:
379:
376:
373:
370:
350:
347:
344:
337:an interval,
321:
318:
315:
309:
306:
279:
273:
270:
250:
230:
227:
224:
216:
201:
194:a number and
181:
161:
158:
155:
135:
132:
129:
121:
118:
115:
112:
108:
105:
101:
98:
95:
91:
90:
89:
75:
67:
63:
59:
51:
49:
47:
43:
39:
35:
31:
27:
23:
20:, a field of
19:
2954:
2948:
2943:(Jan 1994).
2937:Alur, Rajeev
2881:
2555:
2369:
2322:
2211:
1965:
766:
741:
692:be a set of
631:
596:is either a
553:
442:
432:
430:
425:
423:
417:
409:
405:
403:
298:
116:
106:¬ and ∨, and
96:
57:
55:
45:
41:
37:
29:
25:
15:
576:. Usually,
2979:Categories
2857:References
2327:, such as
1643:such that
1434:such that
598:timed word
404:The logic
48:to occur.
2918:ignored (
2908:cite book
2841:ν
2821:ϕ
2801:ϕ
2798:⊨
2795:ν
2783:γ
2763:ϕ
2760:⊨
2731:ϕ
2689:γ
2596:…
2507:¬
2503:⟹
2496:≤
2487:◻
2484:∧
2478:≤
2472:∧
2463:◊
2425:≤
2419:∧
2410:◊
2407:∧
2398:◊
2388:⟹
2378:◻
2355:◊
2335:◻
2285:ψ
2282:∧
2276:∈
2263:ϕ
2237:ψ
2220:ϕ
2171:ψ
2163:at which
2126:ψ
2116:ϕ
2076:ψ
2059:ϕ
1945:ϕ
1942:⊨
1933:→
1924:ν
1912:γ
1904:holds if
1892:ξ
1883:⊨
1880:ν
1868:γ
1843:∼
1831:ν
1828:−
1817:holds if
1802:∼
1796:⊨
1793:ν
1781:γ
1759:ϕ
1756:⊨
1753:ν
1736:γ
1674:ψ
1671:⊨
1668:ν
1651:γ
1600:ψ
1590:ϕ
1587:⊨
1584:ν
1572:γ
1550:ϕ
1547:⊨
1544:ν
1527:γ
1465:ψ
1462:⊨
1459:ν
1442:γ
1391:ψ
1381:ϕ
1378:⊨
1375:ν
1363:γ
1342:ψ
1339:⊨
1336:ν
1324:γ
1304:ϕ
1301:⊨
1298:ν
1286:γ
1266:ψ
1263:∨
1260:ϕ
1257:⊨
1254:ν
1242:γ
1221:ϕ
1215:ν
1203:γ
1195:holds if
1183:ϕ
1180:¬
1177:⊨
1174:ν
1162:γ
1131:γ
1128:∈
1117:holds if
1102:⊨
1099:ν
1087:γ
1064:∼
1014:∈
988:∈
956:∪
933:ξ
893:ψ
873:ϕ
853:ϕ
850:⊨
847:ν
835:γ
815:ν
775:ϕ
723:≥
713:→
704:ν
660:γ
628:Semantics
584:γ
564:γ
537:∈
495:→
486:γ
454:⊆
406:TPTL+Past
380:∧
348:∈
274:∪
251:ϕ
231:ϕ
202:∼
159:∈
133:∼
2813:, where
2150:″
1746:′
1709:′
1698:″
1661:″
1624:″
1537:′
1506:″
1495:′
1452:″
1421:″
1218:⊭
111:temporal
148:, with
2896:
2300:where
1957:holds.
865:. Let
696:. Let
694:clocks
602:signal
439:Models
243:, for
52:Syntax
744:over
600:or a
66:clock
2920:help
2894:ISBN
2347:and
2031:for
2000:and
1713:<
1702:<
1628:<
1499:<
1488:<
1414:<
885:and
652:and
632:Let
443:Let
386:<
374:>
109:the
102:the
56:The
30:TPTL
2959:doi
2886:doi
2633:to
2325:MTL
1728:,
1519:,
1316:or
1003:,
764:).
740:(a
410:TLS
16:In
2981::
2955:41
2953:.
2947:.
2939:;
2928:^
2912::
2910:}}
2906:{{
2892:.
2880:.
2865:^
2548:.
2209:.
1036:,
977:,
925:,
554:AP
431:A
174:,
97:AP
24:,
2967:.
2961::
2922:)
2902:.
2888::
2792:,
2789:i
2786:,
2757:i
2754:,
2751:w
2709:i
2705:a
2701:=
2698:)
2695:i
2692:(
2668:N
2664:=
2661:T
2641:A
2620:N
2599:,
2593:,
2588:1
2584:a
2580:,
2575:0
2571:a
2567:=
2564:w
2536:a
2516:)
2513:)
2510:b
2499:1
2493:x
2490:(
2481:1
2475:x
2469:a
2466:(
2460:.
2457:x
2437:)
2434:)
2431:)
2428:5
2422:x
2416:c
2413:(
2404:b
2401:(
2395:.
2392:x
2384:a
2381:(
2308:x
2288:)
2279:I
2273:x
2268:(
2260:.
2257:x
2230:I
2226:U
2197:I
2194:+
2191:t
2147:t
2121:U
2096:t
2069:I
2065:U
2039:I
2017:I
2011:S
1986:I
1980:U
1939:]
1936:t
1930:y
1927:[
1921:,
1918:t
1915:,
1889:.
1886:y
1877:,
1874:t
1871:,
1858:,
1846:c
1840:)
1837:y
1834:(
1825:t
1805:c
1799:x
1790:,
1787:t
1784:,
1771:,
1750:,
1743:t
1739:,
1716:t
1706:t
1695:t
1665:,
1658:t
1654:,
1631:t
1621:t
1595:S
1581:,
1578:t
1575:,
1562:,
1541:,
1534:t
1530:,
1503:t
1492:t
1485:t
1456:,
1449:t
1445:,
1418:t
1411:t
1386:U
1372:,
1369:t
1366:,
1333:,
1330:t
1327:,
1295:,
1292:t
1289:,
1251:,
1248:t
1245:,
1212:,
1209:t
1206:,
1171:,
1168:t
1165:,
1152:,
1140:)
1137:t
1134:(
1125:l
1105:l
1096:,
1093:t
1090:,
1044:c
1022:P
1019:A
1011:l
991:X
985:x
965:}
962:y
959:{
953:X
913:X
844:,
841:t
838:,
795:t
752:X
726:0
718:R
710:X
707::
680:X
640:T
612:T
540:T
534:t
514:)
511:P
508:A
505:(
500:P
492:T
489::
464:+
459:R
451:T
426:N
420:.
418:S
389:b
383:x
377:a
371:x
351:I
345:x
325:)
322:b
319:,
316:a
313:(
310:=
307:I
295:.
283:}
280:x
277:{
271:X
228:.
225:x
182:c
162:X
156:x
136:c
130:x
119:,
117:U
99:,
76:X
46:q
42:q
38:p
28:(
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.