773:
51:). Fairness properties can be used to rule out unrealistic paths of a model. For instance, in a model of two traffic lights, the liveness property "both traffic lights are green infinitely often" may only be true under the unconditional fairness constraint "each traffic light changes colour infinitely often" (to exclude the case where one traffic light is "infinitely faster" than the other).
1137:
1982:
imposed on a system to rule out unrealistic traces. Unconditional fairness is of the form "every process gets its turn infinitely often". Strong fairness is of the form "every process gets its turn infinitely often if it is enabled infinitely often". Weak fairness is of the form "every process gets
1219:
An invariant property is a type of safety property in which the condition only refers to the current state. For instance, the ATM example is not an invariant because we cannot tell whether the property is violated by seeing that the current state is "dispense money", only by seeing that the current
1986:
In some systems, a fairness constraint is defined by a set of states, and a "fair path" is one that passes through some state in the fairness constraint infinitely often. If there are multiple fairness constraints, then a fair path must pass infinitely often through one state per constraint. A
1146:
bad prefix is a finite set of steps carried out in which money is dispensed in the last step and a PIN is not entered at any step. To verify a safety property, it is sufficient to consider only the finite traces of a Kripke structure and check whether any such trace is a bad prefix.
1683:
942:
at an intersection are represented by a Kripke structure then the atomic propositions may be the possible colours of each light and it may be desirable that the traces satisfy the LT property "the traffic lights cannot both be green at the same time" (to avoid car collisions).
762:
995:
989:(ATM) then such a property is "money should not be dispensed unless a PIN has been entered". Formally, a safety property is an LT property such that any word that violates the property has a "bad prefix", for which no word with that prefix satisfies the property. That is,
78:. An invariant for a system is something that is true or false for a particular state. Invariant properties describe an invariant that every reachable state of a model must satisfy, while persistence properties are of the form "eventually forever some invariant holds".
1362:
2022:(LTL) formulae are LT properties. By a counting argument, we see that any logic in which each formula is a finite string cannot represent all LT properties, as there must be countably many formulae but there are uncountably many LT properties.
1957:
2002:
A fairness property is realizable for a Kripke structure if every reachable state has a fair path starting from that state. So long as a set of fairness conditions are realizable, they are irrelevant to safety properties.
1220:
state is "dispense money" and no previous state was "read PIN". An example of an invariant is the traffic light condition "the traffic lights cannot both be green at the same time" above. Another is "the variable
607:
1542:
1132:{\displaystyle \forall \sigma \in (2^{AP})^{\omega }\setminus P\ \exists {\text{ a finite prefix}}\ {\hat {\sigma }}:P\cap \{\sigma '\mid {\hat {\sigma }}\ {\text{is a prefix of}}\ \sigma '\}=\emptyset }
619:
223:
444:
1487:
1233:
866:
1209:
2548:(1986). "Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends". In J. W. Bakker; W.-P. Roever; G. Rozenberg (eds.).
968:. This is useful in model checking to allow abstraction: if a simplified model of the system satisfies an LT property then the actual model of the system will satisfy it as well.
1818:
1734:
311:
491:
264:
810:
387:
343:
1764:
143:
1534:
1389:
924:
897:
1830:
62:
of "atomic propositions". That is, the property contains sequences of sets of propositions, each sequence known as a "word". Every property can be rewritten as "
1493:
infinitely often". No finite prefix of a word can prove that the word does not satisfy this property, as the word could continue on to have infinitely many
1489:
i.e. any finite string can be continued to a valid trace. An example of a liveness property is the previous LT property "the set of words that contain
2565:
1678:{\displaystyle P=\{A_{0}A_{1}...\in (2^{AP})^{\omega }\mid \exists N\in \mathbb {N} :\forall n\geq N:A_{n}\ {\text{satisfies}}\ \Phi \}}
511:
2429:
2399:
757:{\displaystyle {\mathit {closure}}(P):=\{\sigma \in (2^{AP})^{\omega }\mid {\mathit {pref}}(\sigma )\subseteq {\mathit {pref}}(P)\}}
1394:
A Kripke structure satisfies an invariant if and only if every reachable state satisfies the invariant, which can be checked by a
156:
1766:) is both a safety and a liveness property. Though not every property is a safety property or a liveness property (consider "
100:
1991:
with respect to a set of fairness conditions if for every path, either the path fails a fairness condition or it satisfies
1357:{\displaystyle P=\{A_{0}A_{1}....\in (2^{AP})^{\omega }\mid \forall j\in \mathbb {N} :A_{j}\ {\text{satisfies}}\ \Phi \}}
392:
2390:
1421:
986:
938:. LT properties then describe restrictions on the traces (outputs) of a Kripke structure. For instance, if two
819:
95:
linear-time properties and cannot handle predicates about program states, so it cannot define a property like:
1500:
In terms of computer programs, useful liveness properties include "the program eventually terminates" and, in
1157:
43:. Example properties include "the vending machine does not dispense a drink until money has been entered" (a
2584:
2351:
2015:
2444:
2019:
1780:
1696:
273:
97:
the current value of y determines the number of times that x toggles between 0 and 1 before termination.
92:
85:
1821:
1501:
1395:
931:
460:
2385:
2356:
1505:
1368:
2485:
Kern, Christoph; Greenstreet, Mark R. (1999). "Formal
Verification in Hardware Design: A Survey".
2510:
2464:
2369:
1399:
228:
1770:
occurs exactly once"), every property is the intersection of a safety and a liveness property.
2561:
2502:
2425:
2395:
48:
1952:{\displaystyle d(w,x):=\inf\{2^{-|s|}\mid s\in {\mathit {pref}}(w)\cap {\mathit {pref}}(x)\}}
985:
is informally of the form "a bad thing does not happen". For instance, if a system models an
783:
360:
316:
2553:
2529:
2494:
2456:
2409:
2361:
1739:
935:
777:
118:
32:
1519:
1374:
902:
875:
2440:
2417:
982:
44:
40:
2381:
2011:
772:
454:
81:
55:
28:
17:
2578:
2413:
939:
2514:
2468:
2373:
1979:
2476:
Finkbeiner, Bernd; Torfah, Hazem (2017). "The
Density of Linear-Time Properties".
1983:
its turn infinitely often if it is continuously enabled from a particular point".
2552:. Lecture Notes in Computer Science. Vol. 224. Springer. pp. 510–584.
2545:
2480:. Automated Technology for Verification and Analysis. Vol. 10482. Springer.
1963:
1516:
A persistence property is a liveness property of the form "eventually forever
2506:
2460:
2449:
IEEE Transactions on
Computer-Aided Design of Integrated Circuits and Systems
1967:
146:
59:
2498:
1774:
1414:
is informally of the form "something good eventually happens". Formally,
1411:
2342:
Alpern, B.; Schneider, F. B. (1987). "Recognizing safety and liveness".
2557:
2365:
2445:"A Survey of Automated Techniques for Formal Software Verification"
1402:. Safety properties can be verified inductively using invariants.
771:
602:{\displaystyle \{\{a\},\{a\}\{a,b\},\{a\}\{a,b\}\emptyset ,...\}}
2205:
2114:
2112:
313:
i.e. a set of words. An example of an LT property over the set
2153:
2151:
2087:
2085:
2083:
1932:
1929:
1926:
1923:
1904:
1901:
1898:
1895:
1436:
1433:
1430:
1427:
1181:
1178:
1175:
1172:
1169:
1166:
1163:
737:
734:
731:
728:
709:
706:
703:
700:
643:
640:
637:
634:
631:
628:
625:
2487:
ACM Transactions on Design
Automation of Electronic Systems
389:, which occurs infinitely often. A word not in this set is
153:) is an infinite sequence of sets of propositions, such as
218:{\displaystyle w:=\{a\}\{a,b\}\emptyset \{a,b\}^{\omega }}
88:
describe types of linear time properties using formulae.
812:. It does not satisfy the LT property "infinitely often
2289:
1224:
is never negative", in a model of a computer program.
2018:(CTL) can be used to specify some LT properties. All
1833:
1783:
1742:
1699:
1545:
1522:
1424:
1377:
1236:
1160:
998:
905:
878:
822:
786:
622:
514:
463:
395:
363:
319:
276:
231:
159:
121:
47:) or "the computer program eventually terminates" (a
934:, a program or computer system can be modelled by a
439:{\displaystyle x:=\{a\}(\{b\}\emptyset )^{\omega }}
1951:
1812:
1758:
1728:
1677:
1528:
1481:
1383:
1356:
1203:
1131:
918:
891:
860:
804:
756:
609:in the above case). The closure of an LT property
601:
485:
438:
381:
337:
305:
258:
217:
137:
39:are used to describe requirements of a model of a
868:. It does satisfy the property "infinitely often
2118:
1855:
1482:{\displaystyle {\mathit {pref}}(P)=(2^{AP})^{*}}
2325:
2265:
2181:
2091:
1689:Relation between safety and liveness properties
115:be a set of atomic propositions. A word over
8:
2206:D'Silva, Kroening & Weissenbacher (2008)
1946:
1858:
1672:
1552:
1351:
1243:
1120:
1075:
799:
787:
751:
660:
596:
578:
566:
563:
557:
551:
539:
536:
530:
524:
518:
515:
420:
414:
408:
402:
376:
364:
332:
320:
253:
241:
206:
193:
187:
175:
172:
166:
2313:
2301:
2277:
2253:
2241:
2229:
2217:
2193:
2169:
2157:
2142:
2130:
2103:
2074:
2062:
2050:
2038:
2493:(2). Association for Computing Machinery.
1987:program "fairly satisfies" an LT property
2355:
1922:
1921:
1894:
1893:
1877:
1869:
1865:
1832:
1804:
1791:
1782:
1747:
1741:
1720:
1707:
1698:
1661:
1652:
1626:
1625:
1607:
1594:
1569:
1559:
1544:
1521:
1473:
1460:
1426:
1425:
1423:
1376:
1340:
1331:
1320:
1319:
1301:
1288:
1260:
1250:
1235:
1162:
1161:
1159:
1104:
1090:
1089:
1055:
1054:
1046:
1028:
1015:
997:
910:
904:
883:
877:
861:{\displaystyle s_{1}s_{2}s_{3}^{\omega }}
852:
847:
837:
827:
821:
785:
727:
726:
699:
698:
689:
676:
624:
623:
621:
513:
474:
462:
430:
394:
362:
318:
297:
284:
275:
230:
209:
158:
126:
120:
2534:Handbook of Theoretical Computer Science
1204:{\displaystyle {\mathit {closure}}(P)=P}
972:Classification of linear time properties
2031:
1227:Formally, an invariant is of the form:
1034:
946:If every trace of the Kripke structure
54:Formally, a linear time property is an
2290:Clarke, Grumberg & Kroening (2018)
450:only occurs once (in the first set).
70:both occur" for some safety property
7:
2532:(1990). "Temporal and modal logic".
1536:". That is, a property of the form:
1154:is a safety property if and only if
872:", because all possible paths enter
266:). A linear time (LT) property over
99:The more general formalism used in
1813:{\displaystyle (2^{AP})^{\omega }}
1729:{\displaystyle (2^{AP})^{\omega }}
1669:
1633:
1616:
1523:
1378:
1348:
1310:
1126:
1043:
999:
581:
464:
423:
345:is "the set of words that contain
306:{\displaystyle (2^{AP})^{\omega }}
190:
25:
2478:Lecture Notes in Computer Science
1999:is satisfied for all fair paths.
2443:; Weissenbacher, Georg (2008).
2119:Finkbeiner & Torfah (2017)
1943:
1937:
1915:
1909:
1878:
1870:
1849:
1837:
1801:
1784:
1717:
1700:
1604:
1587:
1470:
1453:
1447:
1441:
1298:
1281:
1192:
1186:
1095:
1060:
1025:
1008:
748:
742:
720:
714:
686:
669:
654:
648:
486:{\displaystyle \Sigma =2^{AP}}
427:
411:
294:
277:
101:Safety and liveness properties
1:
2550:Current Trends in Concurrency
2326:Kern & Greenstreet (1999)
2266:Kern & Greenstreet (1999)
2182:Kern & Greenstreet (1999)
2092:Alpern & Schneider (1987)
1966:and a liveness property is a
225:(for the atomic propositions
2391:Principles of Model Checking
1962:Then a safety property is a
1508:must eventually be served".
957:then every LT property that
349:infinitely often". The word
1736:(the set of all words over
2601:
1693:No LT property other than
1418:is a liveness property if
964:satisfies is satisfied by
259:{\displaystyle AP=\{a,b\}}
2314:Baier & Katoen (2008)
2302:Baier & Katoen (2008)
2278:Baier & Katoen (2008)
2254:Baier & Katoen (2008)
2242:Baier & Katoen (2008)
2230:Baier & Katoen (2008)
2218:Baier & Katoen (2008)
2194:Baier & Katoen (2008)
2170:Baier & Katoen (2008)
2158:Baier & Katoen (2008)
2143:Baier & Katoen (2008)
2131:Baier & Katoen (2008)
2104:Baier & Katoen (2008)
2075:Baier & Katoen (2008)
2063:Baier & Katoen (2008)
2051:Baier & Katoen (2008)
2039:Baier & Katoen (2008)
1820:can be equipped with the
504:) the finite prefixes of
2461:10.1109/TCAD.2008.923410
1995:. That is, the property
1978:Fairness properties are
987:automated teller machine
353:is in this set, because
1777:, the set of all words
816:", because of the path
805:{\displaystyle \{p,q\}}
382:{\displaystyle \{a,b\}}
338:{\displaystyle \{a,b\}}
2016:computation tree logic
1953:
1814:
1760:
1759:{\displaystyle 2^{AP}}
1730:
1679:
1530:
1512:Persistence properties
1483:
1385:
1358:
1205:
1142:In the ATM example, a
1133:
927:
920:
893:
862:
806:
758:
603:
487:
440:
383:
339:
307:
260:
219:
139:
138:{\displaystyle 2^{AP}}
91:This article is about
74:and liveness property
37:linear time properties
18:Linear time properties
2499:10.1145/307988.307989
2344:Distributed Computing
2020:linear temporal logic
1954:
1815:
1761:
1731:
1680:
1531:
1529:{\displaystyle \Phi }
1484:
1386:
1384:{\displaystyle \Phi }
1359:
1206:
1134:
1048: a finite prefix
932:finite-state machines
921:
919:{\displaystyle s_{3}}
894:
892:{\displaystyle s_{1}}
863:
807:
775:
759:
604:
488:
453:An LT property is an
441:
384:
340:
308:
261:
220:
140:
86:linear temporal logic
2386:Katoen, Joost-Pieter
1831:
1781:
1740:
1697:
1543:
1520:
1502:concurrent computing
1422:
1396:breadth-first search
1375:
1234:
1215:Invariant properties
1158:
996:
930:Using the theory of
903:
876:
820:
784:
620:
512:
461:
393:
361:
317:
274:
229:
157:
119:
2316:, pp. 137–139.
2280:, pp. 126–127.
2268:, pp. 131–132.
2244:, pp. 123–124.
2172:, pp. 105–106.
1974:Fairness properties
1406:Liveness properties
1369:propositional logic
857:
2558:10.1007/BFb0027047
2366:10.1007/BF01782772
1949:
1810:
1756:
1726:
1675:
1526:
1479:
1400:depth-first search
1381:
1354:
1201:
1129:
928:
916:
889:
858:
843:
802:
754:
599:
493:(and vice versa).
483:
457:over the alphabet
436:
379:
335:
303:
256:
215:
135:
2567:978-3-540-16488-3
2530:Emerson, E. Allen
2410:Clarke, Edmund M.
2292:, pp. 32–33.
2065:, pp. 97–99.
2053:, pp. 97–98.
1668:
1664:
1660:
1412:liveness property
1347:
1343:
1339:
1111:
1107:
1103:
1098:
1063:
1053:
1049:
1042:
977:Safety properties
926:infinitely often.
103:can handle this.
49:liveness property
16:(Redirected from
2592:
2571:
2541:
2518:
2481:
2472:
2455:(7): 1165–1178.
2441:Kroening, Daniel
2439:D'Silva, Vijay;
2435:
2418:Kroening, Daniel
2405:
2377:
2359:
2329:
2323:
2317:
2311:
2305:
2299:
2293:
2287:
2281:
2275:
2269:
2263:
2257:
2251:
2245:
2239:
2233:
2227:
2221:
2215:
2209:
2203:
2197:
2191:
2185:
2179:
2173:
2167:
2161:
2155:
2146:
2140:
2134:
2128:
2122:
2116:
2107:
2101:
2095:
2089:
2078:
2072:
2066:
2060:
2054:
2048:
2042:
2036:
1958:
1956:
1955:
1950:
1936:
1935:
1908:
1907:
1883:
1882:
1881:
1873:
1819:
1817:
1816:
1811:
1809:
1808:
1799:
1798:
1765:
1763:
1762:
1757:
1755:
1754:
1735:
1733:
1732:
1727:
1725:
1724:
1715:
1714:
1684:
1682:
1681:
1676:
1666:
1665:
1662:
1658:
1657:
1656:
1629:
1612:
1611:
1602:
1601:
1574:
1573:
1564:
1563:
1535:
1533:
1532:
1527:
1488:
1486:
1485:
1480:
1478:
1477:
1468:
1467:
1440:
1439:
1390:
1388:
1387:
1382:
1363:
1361:
1360:
1355:
1345:
1344:
1341:
1337:
1336:
1335:
1323:
1306:
1305:
1296:
1295:
1265:
1264:
1255:
1254:
1210:
1208:
1207:
1202:
1185:
1184:
1138:
1136:
1135:
1130:
1119:
1109:
1108:
1105:
1101:
1100:
1099:
1091:
1085:
1065:
1064:
1056:
1051:
1050:
1047:
1040:
1033:
1032:
1023:
1022:
962:
955:
936:Kripke structure
925:
923:
922:
917:
915:
914:
898:
896:
895:
890:
888:
887:
867:
865:
864:
859:
856:
851:
842:
841:
832:
831:
811:
809:
808:
803:
778:Kripke structure
763:
761:
760:
755:
741:
740:
713:
712:
694:
693:
684:
683:
647:
646:
608:
606:
605:
600:
492:
490:
489:
484:
482:
481:
445:
443:
442:
437:
435:
434:
388:
386:
385:
380:
357:is contained in
344:
342:
341:
336:
312:
310:
309:
304:
302:
301:
292:
291:
265:
263:
262:
257:
224:
222:
221:
216:
214:
213:
144:
142:
141:
136:
134:
133:
33:computer science
21:
2600:
2599:
2595:
2594:
2593:
2591:
2590:
2589:
2575:
2574:
2568:
2544:
2528:
2525:
2523:Further reading
2484:
2475:
2438:
2432:
2408:
2402:
2382:Baier, Christel
2380:
2341:
2338:
2333:
2332:
2324:
2320:
2312:
2308:
2300:
2296:
2288:
2284:
2276:
2272:
2264:
2260:
2252:
2248:
2240:
2236:
2228:
2224:
2216:
2212:
2204:
2200:
2192:
2188:
2180:
2176:
2168:
2164:
2156:
2149:
2141:
2137:
2129:
2125:
2117:
2110:
2102:
2098:
2090:
2081:
2073:
2069:
2061:
2057:
2049:
2045:
2037:
2033:
2028:
2012:Temporal logics
2009:
1976:
1861:
1829:
1828:
1800:
1787:
1779:
1778:
1743:
1738:
1737:
1716:
1703:
1695:
1694:
1691:
1648:
1603:
1590:
1565:
1555:
1541:
1540:
1518:
1517:
1514:
1469:
1456:
1420:
1419:
1408:
1373:
1372:
1327:
1297:
1284:
1256:
1246:
1232:
1231:
1217:
1156:
1155:
1150:An LT property
1112:
1078:
1024:
1011:
994:
993:
983:safety property
979:
974:
960:
953:
906:
901:
900:
879:
874:
873:
833:
823:
818:
817:
782:
781:
770:
685:
672:
618:
617:
510:
509:
470:
459:
458:
426:
391:
390:
359:
358:
315:
314:
293:
280:
272:
271:
270:is a subset of
227:
226:
205:
155:
154:
122:
117:
116:
109:
82:Temporal logics
45:safety property
41:computer system
23:
22:
15:
12:
11:
5:
2598:
2596:
2588:
2587:
2585:Model checking
2577:
2576:
2573:
2572:
2566:
2542:
2524:
2521:
2520:
2519:
2482:
2473:
2436:
2430:
2422:Model Checking
2414:Grumberg, Orna
2406:
2400:
2378:
2357:10.1.1.20.5470
2337:
2334:
2331:
2330:
2328:, p. 127.
2318:
2306:
2304:, p. 132.
2294:
2282:
2270:
2258:
2256:, p. 124.
2246:
2234:
2232:, p. 121.
2222:
2220:, p. 197.
2210:
2198:
2196:, p. 119.
2186:
2184:, p. 135.
2174:
2162:
2160:, p. 105.
2147:
2145:, p. 113.
2135:
2133:, p. 112.
2123:
2108:
2106:, p. 109.
2096:
2079:
2077:, p. 102.
2067:
2055:
2043:
2041:, p. 126.
2030:
2029:
2027:
2024:
2008:
2007:Temporal logic
2005:
1975:
1972:
1960:
1959:
1948:
1945:
1942:
1939:
1934:
1931:
1928:
1925:
1920:
1917:
1914:
1911:
1906:
1903:
1900:
1897:
1892:
1889:
1886:
1880:
1876:
1872:
1868:
1864:
1860:
1857:
1854:
1851:
1848:
1845:
1842:
1839:
1836:
1807:
1803:
1797:
1794:
1790:
1786:
1753:
1750:
1746:
1723:
1719:
1713:
1710:
1706:
1702:
1690:
1687:
1686:
1685:
1674:
1671:
1655:
1651:
1647:
1644:
1641:
1638:
1635:
1632:
1628:
1624:
1621:
1618:
1615:
1610:
1606:
1600:
1597:
1593:
1589:
1586:
1583:
1580:
1577:
1572:
1568:
1562:
1558:
1554:
1551:
1548:
1525:
1513:
1510:
1476:
1472:
1466:
1463:
1459:
1455:
1452:
1449:
1446:
1443:
1438:
1435:
1432:
1429:
1407:
1404:
1380:
1365:
1364:
1353:
1350:
1334:
1330:
1326:
1322:
1318:
1315:
1312:
1309:
1304:
1300:
1294:
1291:
1287:
1283:
1280:
1277:
1274:
1271:
1268:
1263:
1259:
1253:
1249:
1245:
1242:
1239:
1216:
1213:
1200:
1197:
1194:
1191:
1188:
1183:
1180:
1177:
1174:
1171:
1168:
1165:
1140:
1139:
1128:
1125:
1122:
1118:
1115:
1106:is a prefix of
1097:
1094:
1088:
1084:
1081:
1077:
1074:
1071:
1068:
1062:
1059:
1045:
1039:
1036:
1031:
1027:
1021:
1018:
1014:
1010:
1007:
1004:
1001:
978:
975:
973:
970:
950:is a trace of
940:traffic lights
913:
909:
886:
882:
855:
850:
846:
840:
836:
830:
826:
801:
798:
795:
792:
789:
769:
766:
765:
764:
753:
750:
747:
744:
739:
736:
733:
730:
725:
722:
719:
716:
711:
708:
705:
702:
697:
692:
688:
682:
679:
675:
671:
668:
665:
662:
659:
656:
653:
650:
645:
642:
639:
636:
633:
630:
627:
598:
595:
592:
589:
586:
583:
580:
577:
574:
571:
568:
565:
562:
559:
556:
553:
550:
547:
544:
541:
538:
535:
532:
529:
526:
523:
520:
517:
480:
477:
473:
469:
466:
433:
429:
425:
422:
419:
416:
413:
410:
407:
404:
401:
398:
378:
375:
372:
369:
366:
334:
331:
328:
325:
322:
300:
296:
290:
287:
283:
279:
255:
252:
249:
246:
243:
240:
237:
234:
212:
208:
204:
201:
198:
195:
192:
189:
186:
183:
180:
177:
174:
171:
168:
165:
162:
132:
129:
125:
108:
105:
31:, a branch of
29:model checking
24:
14:
13:
10:
9:
6:
4:
3:
2:
2597:
2586:
2583:
2582:
2580:
2569:
2563:
2559:
2555:
2551:
2547:
2543:
2539:
2535:
2531:
2527:
2526:
2522:
2516:
2512:
2508:
2504:
2500:
2496:
2492:
2488:
2483:
2479:
2474:
2470:
2466:
2462:
2458:
2454:
2450:
2446:
2442:
2437:
2433:
2431:9780262038836
2427:
2424:. MIT Press.
2423:
2419:
2415:
2411:
2407:
2403:
2401:9780262026499
2397:
2394:. MIT Press.
2393:
2392:
2387:
2383:
2379:
2375:
2371:
2367:
2363:
2358:
2353:
2349:
2345:
2340:
2339:
2335:
2327:
2322:
2319:
2315:
2310:
2307:
2303:
2298:
2295:
2291:
2286:
2283:
2279:
2274:
2271:
2267:
2262:
2259:
2255:
2250:
2247:
2243:
2238:
2235:
2231:
2226:
2223:
2219:
2214:
2211:
2207:
2202:
2199:
2195:
2190:
2187:
2183:
2178:
2175:
2171:
2166:
2163:
2159:
2154:
2152:
2148:
2144:
2139:
2136:
2132:
2127:
2124:
2120:
2115:
2113:
2109:
2105:
2100:
2097:
2093:
2088:
2086:
2084:
2080:
2076:
2071:
2068:
2064:
2059:
2056:
2052:
2047:
2044:
2040:
2035:
2032:
2025:
2023:
2021:
2017:
2013:
2006:
2004:
2000:
1998:
1994:
1990:
1984:
1981:
1980:preconditions
1973:
1971:
1969:
1965:
1940:
1918:
1912:
1890:
1887:
1884:
1874:
1866:
1862:
1852:
1846:
1843:
1840:
1834:
1827:
1826:
1825:
1823:
1805:
1795:
1792:
1788:
1776:
1771:
1769:
1751:
1748:
1744:
1721:
1711:
1708:
1704:
1688:
1653:
1649:
1645:
1642:
1639:
1636:
1630:
1622:
1619:
1613:
1608:
1598:
1595:
1591:
1584:
1581:
1578:
1575:
1570:
1566:
1560:
1556:
1549:
1546:
1539:
1538:
1537:
1511:
1509:
1507:
1503:
1498:
1496:
1492:
1474:
1464:
1461:
1457:
1450:
1444:
1417:
1413:
1405:
1403:
1401:
1397:
1392:
1370:
1332:
1328:
1324:
1316:
1313:
1307:
1302:
1292:
1289:
1285:
1278:
1275:
1272:
1269:
1266:
1261:
1257:
1251:
1247:
1240:
1237:
1230:
1229:
1228:
1225:
1223:
1214:
1212:
1198:
1195:
1189:
1153:
1148:
1145:
1123:
1116:
1113:
1092:
1086:
1082:
1079:
1072:
1069:
1066:
1057:
1037:
1029:
1019:
1016:
1012:
1005:
1002:
992:
991:
990:
988:
984:
976:
971:
969:
967:
963:
956:
949:
944:
941:
937:
933:
911:
907:
884:
880:
871:
853:
848:
844:
838:
834:
828:
824:
815:
796:
793:
790:
779:
774:
767:
745:
723:
717:
695:
690:
680:
677:
673:
666:
663:
657:
651:
616:
615:
614:
612:
593:
590:
587:
584:
575:
572:
569:
560:
554:
548:
545:
542:
533:
527:
521:
507:
503:
499:
496:We denote by
494:
478:
475:
471:
467:
456:
451:
449:
431:
417:
405:
399:
396:
373:
370:
367:
356:
352:
348:
329:
326:
323:
298:
288:
285:
281:
269:
250:
247:
244:
238:
235:
232:
210:
202:
199:
196:
184:
181:
178:
169:
163:
160:
152:
148:
130:
127:
123:
114:
106:
104:
102:
98:
94:
93:propositional
89:
87:
83:
79:
77:
73:
69:
65:
61:
57:
52:
50:
46:
42:
38:
34:
30:
19:
2549:
2546:Pnueli, Amir
2537:
2533:
2490:
2486:
2477:
2452:
2448:
2421:
2389:
2347:
2343:
2321:
2309:
2297:
2285:
2273:
2261:
2249:
2237:
2225:
2213:
2208:, p. 5.
2201:
2189:
2177:
2165:
2138:
2126:
2121:, p. 4.
2099:
2070:
2058:
2046:
2034:
2010:
2001:
1996:
1992:
1988:
1985:
1977:
1961:
1772:
1767:
1692:
1515:
1499:
1494:
1490:
1415:
1409:
1393:
1366:
1226:
1221:
1218:
1151:
1149:
1143:
1141:
980:
965:
958:
951:
947:
945:
929:
869:
813:
768:Applications
610:
505:
501:
497:
495:
452:
447:
354:
350:
346:
267:
150:
112:
110:
96:
90:
80:
75:
71:
67:
63:
53:
36:
26:
2350:(3): 117.
2336:References
1964:closed set
455:ω-language
107:Definition
56:ω-language
2507:1084-4309
2352:CiteSeerX
1968:dense set
1919:∩
1891:∈
1885:∣
1867:−
1806:ω
1722:ω
1670:Φ
1663:satisfies
1640:≥
1634:∀
1623:∈
1617:∃
1614:∣
1609:ω
1585:∈
1524:Φ
1504:, "every
1475:∗
1379:Φ
1367:for some
1349:Φ
1342:satisfies
1317:∈
1311:∀
1308:∣
1303:ω
1279:∈
1127:∅
1114:σ
1096:^
1093:σ
1087:∣
1080:σ
1073:∩
1061:^
1058:σ
1044:∃
1035:∖
1030:ω
1006:∈
1003:σ
1000:∀
854:ω
724:⊆
718:σ
696:∣
691:ω
667:∈
664:σ
582:∅
465:Σ
432:ω
424:∅
299:ω
211:ω
191:∅
147:power set
60:power set
58:over the
2579:Category
2515:13994730
2420:(2018).
2388:(2008).
2014:such as
1775:topology
1371:formula
1117:′
1083:′
84:such as
2469:8921624
2374:9717112
1506:process
1144:minimal
2564:
2513:
2505:
2467:
2428:
2398:
2372:
2354:
1822:metric
1667:
1659:
1346:
1338:
1110:
1102:
1052:
1041:
508:(i.e.
2511:S2CID
2465:S2CID
2370:S2CID
2026:Notes
961:'
954:'
780:over
446:, as
145:(the
2562:ISBN
2503:ISSN
2426:ISBN
2396:ISBN
613:is:
498:pref
111:Let
66:and
2554:doi
2495:doi
2457:doi
2362:doi
1856:inf
1773:In
1497:s.
1398:or
899:or
149:of
27:In
2581::
2560:.
2536:.
2509:.
2501:.
2489:.
2463:.
2453:27
2451:.
2447:.
2416:;
2412:;
2384:;
2368:.
2360:.
2346:.
2150:^
2111:^
2082:^
1970:.
1853::=
1824::
1410:A
1391:.
1211:.
981:A
966:TS
959:TS
952:TS
948:TS
776:A
658::=
400::=
268:AP
164::=
151:AP
113:AP
35:,
2570:.
2556::
2540:.
2538:B
2517:.
2497::
2491:4
2471:.
2459::
2434:.
2404:.
2376:.
2364::
2348:2
2094:.
1997:P
1993:P
1989:P
1947:}
1944:)
1941:x
1938:(
1933:f
1930:e
1927:r
1924:p
1916:)
1913:w
1910:(
1905:f
1902:e
1899:r
1896:p
1888:s
1879:|
1875:s
1871:|
1863:2
1859:{
1850:)
1847:x
1844:,
1841:w
1838:(
1835:d
1802:)
1796:P
1793:A
1789:2
1785:(
1768:a
1752:P
1749:A
1745:2
1718:)
1712:P
1709:A
1705:2
1701:(
1673:}
1654:n
1650:A
1646::
1643:N
1637:n
1631::
1627:N
1620:N
1605:)
1599:P
1596:A
1592:2
1588:(
1582:.
1579:.
1576:.
1571:1
1567:A
1561:0
1557:A
1553:{
1550:=
1547:P
1495:a
1491:a
1471:)
1465:P
1462:A
1458:2
1454:(
1451:=
1448:)
1445:P
1442:(
1437:f
1434:e
1431:r
1428:p
1416:P
1352:}
1333:j
1329:A
1325::
1321:N
1314:j
1299:)
1293:P
1290:A
1286:2
1282:(
1276:.
1273:.
1270:.
1267:.
1262:1
1258:A
1252:0
1248:A
1244:{
1241:=
1238:P
1222:x
1199:P
1196:=
1193:)
1190:P
1187:(
1182:e
1179:r
1176:u
1173:s
1170:o
1167:l
1164:c
1152:P
1124:=
1121:}
1076:{
1070:P
1067::
1038:P
1026:)
1020:P
1017:A
1013:2
1009:(
912:3
908:s
885:1
881:s
870:p
849:3
845:s
839:2
835:s
829:1
825:s
814:q
800:}
797:q
794:,
791:p
788:{
752:}
749:)
746:P
743:(
738:f
735:e
732:r
729:p
721:)
715:(
710:f
707:e
704:r
701:p
687:)
681:P
678:A
674:2
670:(
661:{
655:)
652:P
649:(
644:e
641:r
638:u
635:s
632:o
629:l
626:c
611:P
597:}
594:.
591:.
588:.
585:,
579:}
576:b
573:,
570:a
567:{
564:}
561:a
558:{
555:,
552:}
549:b
546:,
543:a
540:{
537:}
534:a
531:{
528:,
525:}
522:a
519:{
516:{
506:w
502:w
500:(
479:P
476:A
472:2
468:=
448:a
428:)
421:}
418:b
415:{
412:(
409:}
406:a
403:{
397:x
377:}
374:b
371:,
368:a
365:{
355:a
351:w
347:a
333:}
330:b
327:,
324:a
321:{
295:)
289:P
286:A
282:2
278:(
254:}
251:b
248:,
245:a
242:{
239:=
236:P
233:A
207:}
203:b
200:,
197:a
194:{
188:}
185:b
182:,
179:a
176:{
173:}
170:a
167:{
161:w
131:P
128:A
124:2
76:Q
72:P
68:Q
64:P
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
