A survey on temporal logics for specifying and verifying real-time systems. (English) Zbl 1425.68258
Summary: Over the last two decades, there has been an extensive study of logical formalisms on specifying and verifying real-time systems. Temporal logics have been an important research subject within this direction. Although numerous logics have been introduced for formal specification of real-time and complex systems, an up to date survey of these logics does not exist in the literature. In this paper we analyse various temporal formalisms introduced for specification, including propositional/first-order linear temporal logics, branching temporal logics, interval temporal logics, real-time temporal logics and probabilistic temporal logics. We give decidability, axiomatizability, expressiveness, model checking results for each logic analysed. We also provide a comparison of features of the temporal logics discussed.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
Keywords:
propositional temporal logics; first-order linear temporal logics; branching temporal logics; interval temporal logics; real-time temporal logics; probabilistic temporal logics; decidability; model checking; expressivenessReferences:
| [1] | Bellini P, Mattolini R, Nesi P. Temporal logics for real-time system specification. ACM Computing Surveys, 2000, 32(1): 12-42 · doi:10.1145/349194.349197 |
| [2] | Alur R, Henzinger T A. Real-time logics: complexity and expressiveness. In: Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science. 1990, 390-401 · Zbl 0825.68599 |
| [3] | Ostroff J S. Formal methods for the specification and design of realtime safety critical systems. Journal of Systems and Software, 1992, 18(1): 33-60 · doi:10.1016/0164-1212(92)90045-L |
| [4] | Øhrstrøm P, Hasle P F. Temporal logic: from ancient ideas to artificial intellgience. Dordrecht, The Netherlands: Kluwer Academic Publishers, 1995 · Zbl 0855.03003 |
| [5] | Hirshfeld Y, Rabinovich A. Logics for real time: decidability and complexity. Fundamenta Informaticae, 2004, 62(1): 1-28 · Zbl 1127.03012 |
| [6] | Chaochen Z, Hansen M. Duration calculus: a formal approach to realtime systems. EATCS Series of Monographs in Theoretical Computer Science. Springer, 2004 · Zbl 1071.68062 |
| [7] | Goranko V, Montanari A, Sciavicco G. A road map of interval temporal logics and duration calculi. Journal of Applied Non-Classical Logics, 2004, 14(1-2): 9-54 · Zbl 1181.03012 · doi:10.3166/jancl.14.9-54 |
| [8] | Guelev D, Van Hung D. On the completeness and decidability of duration calculus with iteration. Theoretical Computer Science, 2005, 337(1): 278-304 · Zbl 1108.68074 · doi:10.1016/j.tcs.2005.01.017 |
| [9] | Venema Y. Temporal logic. Blackwell Guide to Philosophical Logic, Blacwell Publishers, 1998 |
| [10] | Fiaderio, J. L.; Maibaum, T.; Gabbay, D. (ed.); Ohlbach, H. (ed.), Action refinement in a temporal logic of objects, No. 927 (1994) |
| [11] | Schwartz R, Melliar-Smith P. From state machines to temporal logic: specification methods for protocol standards. IEEE Transactions on Communications, 1982, 30(12): 2486-2496 · doi:10.1109/TCOM.1982.1095451 |
| [12] | Schwartz, R. L.; Melliar-Smith, P. M.; Voght, F. H., An interval logic for higher-level temporal reasoning, 173-186 (1983) · doi:10.1145/800221.806720 |
| [13] | Moszkowski, B., Reasoning about digital circuits (1983) |
| [14] | Ladkin P. Logical time pieces. AI Expert, 1987, 2(8): 58-67 |
| [15] | Melliar-Smith, P. M.; Melliar-Smith, P. M (ed.), Extending interval logic to real time systems, 224-242 (1989) · doi:10.1007/3-540-51803-7_29 |
| [16] | Razouk R, Gorlick M. Real-time interval logic for reasoning about executions of real-time programs. ACM SIGSOFT Software Engineering Notes, 1989, 14(8): 10-19 · doi:10.1145/75309.75311 |
| [17] | Halpern J Y, Shoham Y. A propositional modal logic of time intervals. Journal of the ACM, 1991, 38(4): 935-962 · Zbl 0799.68175 · doi:10.1145/115234.115351 |
| [18] | Allen J. Maintaining knowledge about temporal intervals. Communications of the ACM, 1983, 26(11): 832-843 · Zbl 0519.68079 · doi:10.1145/182.358434 |
| [19] | Venema Y. A modal logic for chopping intervals. Journal of Logic and Computation, 1991, 1(4): 453-476 · Zbl 0744.03022 · doi:10.1093/logcom/1.4.453 |
| [20] | Benthem V J F. The logic of time: a model-theoretic investigation into the varieties of temporal ontology and temporal discourse. 2nd ed. Kluwer, 1991 · Zbl 0758.03012 |
| [21] | Montanari, A.; Sciavicco, G.; Vitacolonna, N., Decidability of interval temporal logics over split-frames via granularity, 259-270 (2002) · Zbl 1013.03013 |
| [22] | Vitacolonna N. Intervals: logics, algorithms and games. PhD thesis, Department of Mathematics and Computer Science, University of Udine, 2005 |
| [23] | Walker A. Durées et instants. Revue Scientifique, 1947, 85: 131-134 · Zbl 0029.19602 |
| [24] | Hamblin C. Instants and intervals. The Study of Time, 1972, 1: 324-331 · doi:10.1007/978-3-642-65387-2_23 |
| [25] | Humberstone I. Interval semantics for tense logic: some remarks. Journal of philosophical logic, 1979, 8(1): 171-196 · Zbl 0409.03012 · doi:10.1007/BF00258426 |
| [26] | Dowty D. Word meaning and montague grammar. Dordrecht: D. Reidel, 1979 · doi:10.1007/978-94-009-9473-7 |
| [27] | Kamp H. Events, instants and temporal reference. Semantics from Different Points of View, 1979, 376: 417 |
| [28] | Röper P. Intervals and tenses. Journal of Philosophical Logic, 1980, 9(4): 451-469 · Zbl 0451.03007 · doi:10.1007/BF00262866 |
| [29] | Burgess J P. Axioms for tense logic 2: time periods. Notre Dame Journal of Formal Logic, 1982, 23(2): 375-383 · Zbl 0452.03022 · doi:10.1305/ndjfl/1093870150 |
| [30] | Benthem V J F. The logic of time. Kluwer Academic Publishers, Dor-drecht, 1983 · Zbl 0508.03008 |
| [31] | Galton A. The logic of aspect. Claredon Press, Oxford, 1984 |
| [32] | Simons P. Parts, a study in ontology. Oxford: Claredon Press, 1987 |
| [33] | Allen J. Towards a general theory of action and time. Artificial intelligence, 1984, 23(2): 123-154 · Zbl 0567.68025 · doi:10.1016/0004-3702(84)90008-0 |
| [34] | Allen J F, Hayes J P. Moments and points in an interval-based temporal logic. In: Poole D, Mackworth A, Goebel R, eds, Computational Intelligence Blackwell Publishers. 1989, 225-238 |
| [35] | Allen J F, Ferguson G. Actions and events in interval temporal logic. Journal of Logic and Computation, 1994, 4(5): 531-579 · Zbl 0815.68100 · doi:10.1093/logcom/4.5.531 |
| [36] | Galton A. A critical examination of allen’s theory of action and time. Artificial Intelligence, 1990, 42(2): 159-188 · Zbl 0733.03017 · doi:10.1016/0004-3702(90)90053-3 |
| [37] | Roşu, G.; Bensalem, S., Allen linear (interval) temporal logic- translation to ltl andmonitor synthesis, 263-277 (2006) · Zbl 1188.68159 · doi:10.1007/11817963_25 |
| [38] | Parikh R. A decidability result for a second order process logic. In: Proceedings of the 19th Annual Symposium on Foundations of Computer Science. 1978, 177-183 |
| [39] | Pratt, V., Process logic: preliminary report, 93-100 (1979) |
| [40] | Harel D, Kozen D, Parikh R. Process logic: expressiveness, decidability, completeness. Journal of Computer and System Sciences, 1982, 25(2): 144-170 · Zbl 0494.03016 · doi:10.1016/0022-0000(82)90003-4 |
| [41] | Halpern, J.; Manna, Z.; Moszkowski, B., A high-level semantics based on interval logic, 278-291 (1983) · Zbl 0534.68025 · doi:10.1007/BFb0036915 |
| [42] | Gabbay D, Hodkinson I, Reynolds M. Temporal logic: mathematical foundations and computational aspects. Volume 1. Clarendon Press, Oxford, 1994 · Zbl 0921.03023 |
| [43] | Prior A N. Time and modality. Oxford: Clarendon Press, 1957 · Zbl 0079.00606 |
| [44] | Prior A N. Past, present and future. Oxford University Press, 1967 · Zbl 0169.29802 · doi:10.1093/acprof:oso/9780198243113.001.0001 |
| [45] | Prior A N. Papers on time and tense. Oxford University Press, 1968 |
| [46] | Kamp J A. Tense logic and the theory of linear order. PhD thesis, University of California, Los Angeles, 1968 |
| [47] | Pnueli, A., The temporal logic of programs, 46-57 (1977) |
| [48] | Szalas, A.; Bolc, L. (ed.); Szalas, A. (ed.), Temporal logic of programs: a standard approach, 1-50 (1995) |
| [49] | Gabbay, D. M.; Pnueli, A.; Shelah, S.; Stavi, J., On the temporal analysis of fairness, 163-173 (1980) |
| [50] | Sistla A, Clarke E. The complexity of propositional linear temporal logics. Journal of the ACM, 1985, 32(3): 733-749 · Zbl 0632.68034 · doi:10.1145/3828.3837 |
| [51] | Fisher, M., A resolution method for temporal logic, 99-104 (1991) · Zbl 0745.68091 |
| [52] | Fisher M, Dixon C, Peim M. Clausal temporal resolution. ACM Transactions on Computational Logic, 2001, 2(1): 12-56 · Zbl 1365.03017 · doi:10.1145/371282.371311 |
| [53] | Lichtenstein, O.; Pnueli, A.; Zuck, L.; Parikh, R. (ed.), The glory of the past, 196-218 (1985) · Zbl 0586.68028 · doi:10.1007/3-540-15648-8_16 |
| [54] | Lichtenstein O, Pnueli A. Propositional temporal logics: decidability and completeness. Logic Journal of the IGPL, 2000, 8(1): 55-85 · Zbl 1033.03009 · doi:10.1093/jigpal/8.1.55 |
| [55] | Reynolds M. The complexity of the temporal logic with “until” over general linear time. Journal of Computer and System Sciences, 2003, 66(2): 393-426 · Zbl 1019.03014 · doi:10.1016/S0022-0000(03)00005-9 |
| [56] | Lutz C, Walther D, Wolter F. Quantitative temporal logics over the reals: PSPACE and below. Information and Computation, 2007, 205(1): 99-123 · Zbl 1109.03012 · doi:10.1016/j.ic.2006.08.006 |
| [57] | Reynolds M. The complexity of temporal logic over the reals. Annals of Pure and Applied Logic, 2010, 161(8): 1063-1096 · Zbl 1235.03052 · doi:10.1016/j.apal.2010.01.002 |
| [58] | McDermott D. A temporal logic for reasoning about processes and plans. Cognitive science, 1982, 6(2): 101-155 · doi:10.1207/s15516709cog0602_1 |
| [59] | Rao, A.; Georgeff, M., A model-theoretic approach to the verification of situated reasoning systems (1993) |
| [60] | Abrahamson K. Decidability and expressiveness of logics of programs. PhD thesis, University of Washington, 1980 |
| [61] | Ben-Ari, M.; Manna, Z.; Pnueli, A., The temporal logic of branching time, 164-176 (1981) |
| [62] | Clarke, E. M.; Emerson, E. A., Design and synthesis of synchronization skeletons using branching-time temporal logic, 52-71 (1982) · Zbl 0546.68014 · doi:10.1007/BFb0025774 |
| [63] | Emerson E A, Halpern J. “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. Journal of the ACM, 1986, 33(1): 151-178 · Zbl 0629.68020 · doi:10.1145/4904.4999 |
| [64] | Laroussinie F, Schnoebelen P. A hierarchy of temporal logics with past. Theoretical Computer Science, 1995, 148(2): 303-324 · Zbl 0873.68068 · doi:10.1016/0304-3975(95)00035-U |
| [65] | Clarke E M, Grumberg O, Peled D A. Model Checking. MIT Press, 2000 |
| [66] | Emerson, E. A.; Halpern, J. Y., Decision procedures and expressiveness in the temporal logic of branching time, 169-180 (1982) |
| [67] | Emerson, E.; Srinivasan, J., Branching time temporal logic, 123-172 (1989) · Zbl 0683.68013 · doi:10.1007/BFb0013022 |
| [68] | Emerson E A, Clarke E M. Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer programming, 1982, 2(3): 241-266 · Zbl 0514.68032 · doi:10.1016/0167-6423(83)90017-5 |
| [69] | Clarke E M, Emerson E A, Sistla A P. Automatic verification of finite state concurrent systems using temporal logic. ACM Transactions on Programming Languages and Systems, 1986, 2(8): 244-263 · Zbl 0591.68027 · doi:10.1145/5397.5399 |
| [70] | Penczek, W.; Bolc, L. (ed.); Szalas, A. (ed.), Branching time and partial order in temporal logics, 179-228 (1995) |
| [71] | Emerson E A, Jutla C S. The complexity of tree automata and logics of programs. SIAM Journal of Compututation, 2000, 29(1): 132-158 · Zbl 0937.68074 · doi:10.1137/S0097539793304741 |
| [72] | Reynolds M. An axiomatization of full computation tree logic. Journal of Symbolic Logic, 2001, 66: 1011-1057 · Zbl 1002.03015 · doi:10.2307/2695091 |
| [73] | Reynolds M. An axiomatization of PCTL. Information and Computation, 2005, 201(1): 72-119 · Zbl 1099.03013 · doi:10.1016/j.ic.2005.03.005 |
| [74] | Laroussinie F, Schnoebelen P. Specification in CTL+past, verification in CTL. Information and Computation, 2000, 156(1): 236-263 · Zbl 1046.68599 · doi:10.1006/inco.1999.2817 |
| [75] | Bozzelli, L.; Amadio, R. (ed.), The complexity of CTL* + linear past, 186-200 (2008) · Zbl 1139.68037 · doi:10.1007/978-3-540-78499-9_14 |
| [76] | Pratt, V. R., On the composition of processes, 213-223 (1982) · doi:10.1145/582153.582177 |
| [77] | Pinter, S. S.; Wolper, P., A temporal logic for reasoning about partially ordered computations (extended abstract), 28-37 (1984) · doi:10.1145/800222.806733 |
| [78] | Kornatzky Y, Pinter S. An extension to partial order temporal logic (POTL). Research Report 596, Department of Electrical Engineering, Technion-Israel Institute of Technology, 1986 |
| [79] | Bhat G, Peled D. Adding partial orders to linear temporal logic. Fundamenta Informaticae, 1998, 36(1): 1-21 · Zbl 0930.68063 |
| [80] | Gerth R, Kuiper R, Peled D, Penczek W. A partial order approach to branching time logic model checking. Information and Computation, 1999, 150(2): 132-152 · Zbl 1045.68588 · doi:10.1006/inco.1998.2778 |
| [81] | Alexander, A.; Reisig, W., Compositional temporal logic based on partial order, 125-132 (2004) |
| [82] | Lomuscio, A.; Penczek, W.; Qu, H., Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems, 659-666 (2010) · Zbl 1213.68382 |
| [83] | Fagin R, Halpern J, Moses Y, Vardi M. Reasoning about knowledge. MIT Press, 1996 |
| [84] | Chomicki, J.; Toman, D., Temporal logic in information systems, 31-70 (1998) · Zbl 0955.03513 · doi:10.1007/978-1-4615-5643-5_3 |
| [85] | Abadi M. The power of temporal proofs. Theoretical Computer Science, 1989, 65(1): 35-83 · Zbl 0669.03010 · doi:10.1016/0304-3975(89)90138-2 |
| [86] | Andréka, H.; Németi, I.; Sain, I., Mathematical foundations of computer science, 208-218 (1979) · Zbl 0411.03017 |
| [87] | Reynolds M. Axiomatising first-order temporal logic: until and since over linear time. Studia Logica, 1996, 57(2): 279-302 · Zbl 0864.03015 · doi:10.1007/BF00370836 |
| [88] | Merz S. Decidability and incompleteness results for first-order temporal logics of linear time. Journal of Applied Non-Classical Logics, 1992, 2(2): 139-156 · Zbl 0790.03019 · doi:10.1080/11663081.1992.10510779 |
| [89] | Chomicki J. Efficient checking of temporal integrity constraints using bounded history encoding. ACM Transactions on Database Systems, 1995, 20(2): 149-186 · doi:10.1145/210197.210200 |
| [90] | Pliuskevicius, R., On the completeness and decidability of a restricted first order linear temporal logic, 241-254 (1997) · Zbl 0885.03020 · doi:10.1007/3-540-63385-5_47 |
| [91] | Wolter F, Zakharyaschev M. Axiomatizing the monodic fragment of first-order temporal logic. Annals of Pure and Applied logic, 2002, 118(1): 133-145 · Zbl 1031.03023 · doi:10.1016/S0168-0072(01)00124-5 |
| [92] | Andréka H, Németi I, Benthem V J. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 1998, 27(3): 217-274 · Zbl 0919.03013 · doi:10.1023/A:1004275029985 |
| [93] | Grädel E. On the restraining power of guards. Journal of Symbolic Logic, 1999, 64: 1719-1742 · Zbl 0958.03027 · doi:10.2307/2586808 |
| [94] | Hodkinson I, Wolter F, Zakharyaschev M. Decidable fragments of first-order temporal logics. Annals of Pure and Applied logic, 2000, 106(1): 85-134 · Zbl 0999.03015 · doi:10.1016/S0168-0072(00)00018-X |
| [95] | Börger E, Grädel E, Gurevich Y. The classical decision problem. Springer, 1997 · Zbl 0865.03004 · doi:10.1007/978-3-642-59207-2 |
| [96] | Hodkinson, I. M.; Wolter, F.; Zakharyaschev, M., Monodic fragments of first-order temporal logics: 2000-2001 A.D, 1-23 (2001) · Zbl 1275.03088 · doi:10.1007/3-540-45653-8_1 |
| [97] | Gabbay D, Kurucz A, Wolter F, Zakharyaschev M. Many-dimensional modal logics: theory and applications. Elsevier, 2002 · Zbl 1051.03001 |
| [98] | Degtyarev A, Fisher M, Lisitsa A. Equality and monodic first-order temporal logic. Studia Logica, 2002, 72(2): 147-156 · Zbl 1011.03007 · doi:10.1023/A:1021352309671 |
| [99] | Woltert P, Zakharyaschev M. Modal description logics: modalizing roles. Fundamenta Informaticae, 1999, 39(4): 411-438 · Zbl 0951.03011 |
| [100] | Lutz C, Sturm H, Wolter F, Zakharyaschev M. A tableau decision algorithm for modalized ALC with constant domains. Studia Logica, 2002, 72(2): 199-232 · Zbl 1010.03012 · doi:10.1023/A:1021308527417 |
| [101] | Dixon, C.; Fisher, M.; Konev, B.; Lisitsa, A., Practical first-order temporal reasoning, 156-163 (2008) |
| [102] | Emerson E, Mok A, Sistla A, Srinivasan J. Quantitative temporal reasoning. Real-Time Systems, 1992, 4(4): 331-352 · doi:10.1007/BF00355298 |
| [103] | Koymans R. Specifying real-time properties with metric temporal logic. Real-Time Systems, 1990, 2(4): 255-299 · doi:10.1007/BF01995674 |
| [104] | Alur R, Henzinger T A. A really temporal logic. Journal of the ACM, 1994, 41(1): 181-203 · Zbl 0807.68065 · doi:10.1145/174644.174651 |
| [105] | Henzinger T A. The temporal specification and verification of realtime systems. PhD thesis, Department of Computer Science, Stanford University, 1991 |
| [106] | Emerson, E. A.; Trefler, R. J., Generalized quantitative temporal reasoning: an automata theoretic-approach, 189-200 (1996) |
| [107] | Laroussinie, F.; Meyer, A.; Petonnet, E., Counting LTL, 51-58 (2010) |
| [108] | Ouaknine, J.; Worrell, J., Some recent results in metric temporal logic, 1-13 (2008) · Zbl 1171.68553 · doi:10.1007/978-3-540-85778-5_1 |
| [109] | Ouaknine, J.; Worrell, J., On the decidability of metric temporal logic, 188-197 (2005) |
| [110] | Alur R, Feder T, Henzinger T A. The benefits of relaxing punctuality. Journal of the ACM, 1996, 43(1): 116-146 · Zbl 0882.68021 · doi:10.1145/227595.227602 |
| [111] | Henzinger, T. A.; Raskin, J. F.; Schobbens, P. Y., The regular real-time languages, 580-591 (1998) · doi:10.1007/BFb0055086 |
| [112] | Henzinger, T. A., It’s about time: real-time logics reviewed, 439-454 (1998) · Zbl 0928.03019 |
| [113] | Lasota S, Walukiewicz I. Alternating timed automata. ACM Transactions on Computational Logic, 2008, 9(2): 1-27 · Zbl 1367.68172 · doi:10.1145/1342991.1342994 |
| [114] | Maler, O.; Nickovic, D.; Pnueli, A.; Pettersson, P. (ed.); Yi, W. (ed.), Real time temporal logic: past, present, future, 2-16 (2005) · Zbl 1175.03009 · doi:10.1007/11603009_2 |
| [115] | Bouyer, P.; Markey, N.; Ouaknine, J.; Worrell, J., On expressiveness and complexity in real-time model checking, 124-135 (2008) · Zbl 1155.68426 · doi:10.1007/978-3-540-70583-3_11 |
| [116] | Bouyer, P.; Chevalier, F.; Markey, N., On the expressiveness of TPTL and MTL, 432-443 (2005) · Zbl 1140.03303 |
| [117] | Alur, R.; Henzinger, T. A., Logics and models of real time: a survey, 74-106 (1992) · doi:10.1007/BFb0031988 |
| [118] | Alur, R.; Courcoubetis, C.; Dill, D. L., Model checking for real-time systems, 12-21 (1990) |
| [119] | Laroussinie, F.; Markey, N.; Schnoebelen, P., Model checking timed automata with one or two clocks, 387 (2004) · Zbl 1099.68057 |
| [120] | Hansson H A. Time and probability in formal design and distributed systems. PhD thesis, Department of Computer Science, Uppsala University, Sweden, 1991 |
| [121] | Beauquier D, Slissenko A. Polytime model checking for timed probabilistic computation tree logic. Acta Informatica, 1998, 35: 645-664 · Zbl 0910.68201 · doi:10.1007/s002360050136 |
| [122] | Laroussinie, F.; Meyer, A.; Petonnet, E., Counting CTL, 206-220 (2010) · Zbl 1284.03149 · doi:10.1007/978-3-642-12032-9_15 |
| [123] | Jahanian F, Mok A. Safety analysis of timing properties in real-time systems. IEEE Transactions on Software Engineering, 1986, 12(9): 890-904 · doi:10.1109/TSE.1986.6313045 |
| [124] | Jahanian F, Mok A. Modechart: a specification language for real-time systems. IEEE Transactions on Software Engineering, 1994, 20(12): 933-947 · doi:10.1109/32.368134 |
| [125] | Jahanian, F.; Stuart, D., A method for verifying properties of modechart specifications, 12-21 (1988) |
| [126] | Andrei, S.; Cheng, A. M K., Faster verification of RTL-specified systems via decomposition and constraint extension, 67-76 (2006) |
| [127] | Andrei, S.; Cheng, A. M K., Verifying linear real-time logic specifications, 333-342 (2007) |
| [128] | Ostroff, J. S.; Wonham, W., Modeling and verifying real-time embedded computer systems, 124-132 (1987) |
| [129] | Ostroff, J. S., Temporal logic for real-time systems. Advanced Software Development Series (1989) |
| [130] | Harel, E.; Lichtenstein, O.; Pnueli, A., Explicit clock temporal logic, 402-413 (1990) · doi:10.1109/LICS.1990.113765 |
| [131] | Harel D, Lachover H, Naamad A, Pnueli A, Politi M, Sherman R, et al. Statemate: a working environment for the development of complex reactive systems. IEEE Transactions on Software Engineering, 1990, 16(4): 403-414 · doi:10.1109/32.54292 |
| [132] | Ghezzi C, Mandrioli D, Morzenti A. TRIO: a logic language for executable specifications of real-time systems. Journal of Systems and Software, 1990, 12(2): 107-123 · doi:10.1016/0164-1212(90)90074-V |
| [133] | Mattolini R. TILCO: a temporal logic for the specification of real-time systems. PhD thesis, University of Florence, 1996 |
| [134] | Mattolini, R.; Nesi, P., Using TILCO for specifying real-time systems, 18-25 (1996) |
| [135] | Mattolini R, Nesi P. An interval logic for real-time system specification. IEEE Transactions on Software Engineering, 2001, 27(3): 208-227 · doi:10.1109/32.910858 |
| [136] | Paulson L C. Isabelle: a generic theorem prover. Springer LNCS 828, 1994 · Zbl 0825.68059 |
| [137] | Bellini, P.; Giotti, A.; Nesi, P.; Rogai, D., TILCO temporal logic for realtime systems implementation in C++, 166-173 (2003) |
| [138] | Bellini, P.; Giotti, A.; Nesi, P., Execution of TILCO temporal logic speci- fications, 78-87 (2002) |
| [139] | Bellini P, Nesi P, Rogai D. Reply to comments on “an interval logic for real-time system specification”. IEEE Transactions on Software Engineering, 2006, 32(6): 428-431 · doi:10.1109/TSE.2006.57 |
| [140] | Bellini P, Nesi P, Rogai D. Validating component integration with C-TILCO. Electronic Notes in Theoretical Computer Science, 2005, 116: 241-252 · doi:10.1016/j.entcs.2004.02.080 |
| [141] | Marx M, Reynolds M. Undecidability of compass logic. Journal of Logic and Computation, 1999, 9(6): 897-914 · Zbl 0941.03018 · doi:10.1093/logcom/9.6.897 |
| [142] | Marx D, Venema Y. Multi-dimensional modal logics. Kluwer Academic Press, 1997 · Zbl 0942.03029 · doi:10.1007/978-94-011-5694-3 |
| [143] | Lodaya, K., Sharpening the undecidability of interval temporal logic, 290-298 (2000) · Zbl 0987.03015 |
| [144] | Bresolin, D.; Monica, D.; Goranko, V.; Montanari, A.; Sciavicco, G., Decidable and undecidable fragments of halpern and shoham’s interval temporal logic: towards a complete classification, 590-604 (2008) · Zbl 1182.03037 · doi:10.1007/978-3-540-89439-1_41 |
| [145] | Bresolin D. Proof methods for interval temporal logics. PhD thesis, University of Udine, 2007 |
| [146] | Goranko, V.; Montanari, A.; Sciavicco, G., A general tableau method for propositional interval temporal logics, 102-116 (2003) · Zbl 1274.03033 |
| [147] | Hodkinson, I.; Montanari, A.; Sciavicco, G., Non-finite axiomatizability and undecidability of interval temporal logics with C, D, and T, 308-322 (2008) · Zbl 1156.03321 · doi:10.1007/978-3-540-87531-4_23 |
| [148] | Chaochen, Z.; Hansen, M., An adequate first order interval logic, 584-608 (1997) |
| [149] | Goranko V, Montanari A, Sciavicco G. Propositional interval neighbourhood temporal logics. Journal of Universal Computer Science, 2003, 9(9): 1137-1167 |
| [150] | Bresolin, D.; Montanari, A.; Sala, P., An optimal tableau-based decision algorithm for propositional neighborhood logic, 549-560 (2007) · Zbl 1141.03308 |
| [151] | Bresolin, D.; Goranko, V.; Montanari, A.; Sciavicco, G., On decidability and expressiveness of propositional interval neighbourhood logics, 84-99 (2007) · Zbl 1132.03335 · doi:10.1007/978-3-540-72734-7_7 |
| [152] | Bresolin, D.; Montanari, A., A tableau-based decision procedure for right propositional neighborhood logic, 63-77 (2005) · Zbl 1141.03307 · doi:10.1007/11554554_7 |
| [153] | Bresolin D, Montanari A, Sciavicco G. An optimal tableau-based decision procedure for right propositional neighbourhood logic. Journal of Automated Reasoning, 2007, 38: 173-199 · Zbl 1121.03027 · doi:10.1007/s10817-006-9051-0 |
| [154] | Bresolin, D.; Monica, D.; Goranko, V.; Montanari, A.; Sciavicco, G., Metric propositional neighborhood logics: expressiveness, decidability, and undecidability, 695-700 (2010) · Zbl 1211.68397 |
| [155] | Bresolin D, Goranko V, Montanari A, Sciavicco G. Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions. Annals of Pure and Applied Logic, 2009, 161(3): 289-304 · Zbl 1221.03022 · doi:10.1016/j.apal.2009.07.003 |
| [156] | Chagrov, A. V.; Rybakov, M. N., How many variables does one need to prove PSPACE-hardness of modal logics?, 71-82 (2003) · Zbl 1076.03012 |
| [157] | Demri, S.; Gore, R., An O((n. log n)3)− time transformation from Grz into decidable fragments of classical first-order logic, 153-167 (2000) |
| [158] | Bresolin D, Goranko V, Montanari A, Sala P. Tableaux for logics of subinterval structures over dense orderings. Journal of Logic and Computation, 2010, 20(1): 133-166 · Zbl 1188.03009 · doi:10.1093/logcom/exn063 |
| [159] | Montanari, A.; Pratt-Hartmann, I.; Sala, P., Decidability of the logics of the reflexive sub-interval and super-interval relations over finite linear orders, 27-34 (2010) |
| [160] | Marcinkowski, J.; Michaliszyn, J., The ultimate undecidability result for the Halpern-shoham logic, 377-386 (2011) |
| [161] | Pratt-Hartmann I. Temporal prepositions and their logic. Artificial Intelligence, 2005, 166(1-2): 1-36 · Zbl 1132.03334 · doi:10.1016/j.artint.2005.04.003 |
| [162] | Konur, S., A decidable temporal logic for events and states, 36-41 (2006) · doi:10.1109/TIME.2006.1 |
| [163] | Chaochen Z, Hoare C, Ravn A. A calculus of durations. Information Processing Letters, 1991, 40(5): 269-276 · Zbl 0743.68097 · doi:10.1016/0020-0190(91)90122-X |
| [164] | Dutertre B. On first-order interval temporal logic. Technical Report CSD-TR-94-3, Department of Computer Science, Royal Holloway College, University of London, 1995 |
| [165] | Moszkowski, B., A complete axiomatization of interval temporal logic with infinite time, 242-251 (2000) |
| [166] | Guelev D P. A complete proof system for first order interval temporal logic with projection. Technical Report 202, UNU/IIST, 2000 |
| [167] | Moszkowski, B., Some very compositional temporal properties, 307-326 (1994) |
| [168] | Chaochen, Z.; Hansen, M.; Sestoft, P., Decidability and undecidability results for duration calculus, 58-68 (1993) · Zbl 0811.68115 |
| [169] | Rabinovich A. Non-elementary lower bound for propositional duration calculus. Information Processing Letters, 1998, 66(1): 7-11 · Zbl 0925.68062 · doi:10.1016/S0020-0190(98)00027-1 |
| [170] | Fränzle, M., Synthesizing controllers from duration calculus, 168-187 (1996) · doi:10.1007/3-540-61648-9_40 |
| [171] | Guelev, D.; Dang, V. H.; Thiagarajan, P. S (ed.); Yap, R. (ed.), On the completeness and decidability duration calculus with iteration, 139-150 (1999) |
| [172] | Chetcuti-Serandio N, Cerro L D. A mixed decision method for duration calculus. Journal of Logic and Computation, 2000, 10(6): 877-895 · Zbl 0965.03013 · doi:10.1093/logcom/10.6.877 |
| [173] | Pandya, P. K., Specifying and deciding quantified discrete-time duration calculus formulas using DCVALID (2001) |
| [174] | Zhou, C., Linear duration invariants, 86-109 (1994) |
| [175] | Xuandong, L.; Hung, D., Checking linear duration invariants by linear programming, 321-332 (1996) · Zbl 1541.68229 · doi:10.1007/BFb0027804 |
| [176] | Thai, P. H.; Hung, D. V., Checking a regular class of duration calculus models for linear duration invariants, 61-71 (1998) |
| [177] | Thai, P.; Hung, D., Verifying linear duration constraints of timed automata, 295-309 (2004) · Zbl 1109.68070 |
| [178] | Satpathy, M.; Hung, D. V.; Pandya, P. K., Some decidability results for duration calculus under synchronous interpretation, 186-197 (1998) · doi:10.1007/BFb0055347 |
| [179] | Fränzle, M., Take it NP-easy: Bounded model construction for duration calculus, 245-264 (2002) · Zbl 1278.68170 · doi:10.1007/3-540-45739-9_16 |
| [180] | Biere, A.; Cimatti, A.; Clarke, E. M.; Zhu, Y., Symbolic model checking without BDDs, 193-207 (1999) · doi:10.1007/3-540-49059-0_14 |
| [181] | Fränzle, M.; Hansen, M., Deciding an interval logic with accumulated durations, 201-215 (2007) · Zbl 1186.03055 · doi:10.1007/978-3-540-71209-1_17 |
| [182] | Hansen, M. R.; Sharp, R., Using interval logics for temporal analysis of security protocols (2003) |
| [183] | Barua R, Roy S, Chaochen Z. Completeness of neighbourhood logic. Journal of Logic and Computation, 2000, 10(2): 271-295 · Zbl 0999.03017 · doi:10.1093/logcom/10.2.271 |
| [184] | Barua R, Chaochen Z. Neighbourhood logics. Research Report 120, UNU/IIST, 1997 |
| [185] | Alur, R.; Dill, D., Automata-theoretic verification of real-time systems, 55-82 (1996) |
| [186] | Alur R, Henzinger T A, Ho P H. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering, 1996, 22(3): 181-201 · doi:10.1109/32.489079 |
| [187] | Bengtsson, J.; Larsen, K.; Larsson, F.; Pettersson, P.; Yi, W., UPPAAL-a tool suite for automatic verification of real-time systems, 232-243 (1996) · doi:10.1007/BFb0020949 |
| [188] | Bozga, M.; Daws, C.; Maler, O.; Olivero, A.; Tripakis, S.; Yovine, S., Kronos: a model-checking tool for real-time systems, 546-550 (1998) · doi:10.1007/BFb0028779 |
| [189] | Pandya P. Interval duration logic: expressiveness and decidability. Electronic Notes in Theoretical Computer Science, 2002, 65(6): 254-272 · Zbl 1270.68175 · doi:10.1016/S1571-0661(04)80480-8 |
| [190] | Sharma, B.; Pandya, P.; Chakraborty, S., Bounded validity checking of interval duration logic, 301-316 (2005) · Zbl 1087.68061 · doi:10.1007/978-3-540-31980-1_20 |
| [191] | Chakravorty, G.; Pandya, P.; Hunt, JW (ed.); Somenzi, F. (ed.), Digitizing interval duration logic, 167-179 (2003) · Zbl 1278.68161 · doi:10.1007/978-3-540-45069-6_17 |
| [192] | Filliâtre, J.; Owre, S.; Rueß, H.; Shankar, N., ICS: integrated canonizer and solver, 246-249 (2001) · Zbl 0996.68559 · doi:10.1007/3-540-44585-4_22 |
| [193] | Van Hung D, Chaochen Z. Probabilistic duration calculus for continuous time. Formal Aspects of Computing, 1999, 11(1): 21-44 · Zbl 0937.68079 · doi:10.1007/s001650050034 |
| [194] | Fagin R, Halpern J Y. Reasoning about knowledge and probability. Journal of the ACM, 1994, 41(2): 340-367 · Zbl 0806.68098 · doi:10.1145/174652.174658 |
| [195] | Marković Z, Ognjanović Z, Rašković M. A probabilistic extension of intuitionistic logic. Mathematical Logic Quarterly, 2003, 49(4): 415-424 · Zbl 1022.03011 · doi:10.1002/malq.200310044 |
| [196] | Hansson, H.; Jonsson, B., A framework for reasoning about time and reliability, 102-111 (1989) · doi:10.1109/REAL.1989.63561 |
| [197] | Hansson H, Jonsson B. A logic for reasoning about time and reliability. Formal Aspects of Computing, 1994, 6(5): 512-535 · Zbl 0820.68113 · doi:10.1007/BF01211866 |
| [198] | Brázdil, T.; Forejt, V.; Kretinsky, J.; Kucera, A., The satisfiability problem for probabilistic CTLw, 391-402 (2008) |
| [199] | Aziz, A.; Singhal, V.; Balarin, F., It usually works: the temporal logic of stochastic systems, 155-165 (1995) · doi:10.1007/3-540-60045-0_48 |
| [200] | Bianco, A.; Alfaro, L., Model checking of probabalistic and nondeterministic systems, 499-513 (1995) · Zbl 1354.68167 · doi:10.1007/3-540-60692-0_70 |
| [201] | Kwiatkowska, M.; Norman, G.; Segala, R.; Sproston, J.; Katoen, J. P (ed.), Automatic verification of real-time systems with discrete probability distributions, 75-95 (1999) · doi:10.1007/3-540-48778-6_5 |
| [202] | Kwiatkowska, M.; Norman, G.; Segala, R.; Sproston, J., Verifying quantitative properties of continuous probabilistic timed automata, 123-137 (2000) · Zbl 0999.68125 |
| [203] | Jurdzinski, M.; Laroussinie, F.; Sproston, J.; Abdulla, P. (ed.); Leino, K. (ed.), Model checking probabilistic timed automata with one or two clocks, 170-184 (2007) · Zbl 1186.68295 · doi:10.1007/978-3-540-71209-1_15 |
| [204] | Ognjanović Z. Discrete linear-time probabilistic logics: completeness, decidability and complexity. Journal of Logic and Computation, 2006, 16(2): 257-285 · Zbl 1102.03022 · doi:10.1093/logcom/exi077 |
| [205] | Liu Z, Ravn A P, Sorensen E V, Zhou C. A probabilistic duration calculus. Technical Report, University of Warwick, 1992 |
| [206] | Hung, D. V.; Zhang, M., On verification of probabilistic timed automata against probabilistic duration properties, 165-172 (2007) |
| [207] | Choe Changil D V H. Model checking durational probabilistic systems against probabilistic linear duration invariants. Research Report 337, UNU/IIST, 2006 |
| [208] | Kwiatkowska M, Norman G, Segala R, Sproston J. Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science, 2002, 282(1): 101-150 · Zbl 1050.68094 · doi:10.1016/S0304-3975(01)00046-9 |
| [209] | Guelev, D. P., Probabilistic neighbourhood logic, 264-275 (2000) · Zbl 0986.03025 · doi:10.1007/3-540-45352-0_22 |
| [210] | Guelev D. Probabilistic neighbourhood logic. Research Report 196, UNU/IIST, 2000 · Zbl 0986.03025 |
| [211] | Guelev D P. Probabilistic interval temporal logic. Technical Report 144, UNU/IIST, 1998 |
| [212] | Segerberg, K.; Traczyk, T. (ed.), A completeness theorem in the modal logic of programs, 31-46 (1982) · Zbl 0546.03011 |
| [213] | Pippenger N, Fischer M J. Relations among complexity measures. Journal of the ACM, 1979, 26(2): 361-381 · Zbl 0405.68041 · doi:10.1145/322123.322138 |
| [214] | Harel D, Tiuryn J, Kozen D. Dynamic Logic. Cambridge, MA, USA: MIT Press, 2000 · Zbl 0976.68108 |
| [215] | Lamport L. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 1994, 16(3): 872-923 · doi:10.1145/177492.177726 |
| [216] | Giordano L, Martelli A, Schwind C. Reasoning about actions in dynamic linear time temporal logic. Logic Journal of IGPL, 2001, 9(2): 273-288 · Zbl 0979.03015 · doi:10.1093/jigpal/9.2.273 |
| [217] | Kowalski R, Sergot M. A logic-based calculus of events. New Generation Computing, 1986, 4(1): 67-95 · Zbl 1356.68221 · doi:10.1007/BF03037383 |
| [218] | Shoham Y. Reasoning about Action and Change. MIT Press, 1987 |
| [219] | Reiter R. Proving properties of states in the situation calculus. Artifi- cial Intelligence, 1993, 64(2): 337-351 · Zbl 0788.68139 · doi:10.1016/0004-3702(93)90109-O |
| [220] | Gelfond M, Lifschitz V. Representing action and change by logic programs. The Journal of Logic Programming, 1993, 17(2): 301-321 · Zbl 0783.68024 · doi:10.1016/0743-1066(93)90035-F |
| [221] | Belnap N D. Facing the future: agents and choices in our indeterminist world. Oxford University Press, USA, 2001 |
| [222] | Kozen, D., Semantics of probabilistic programs, 101-114 (1979) |
| [223] | Feldman, Y. A.; Harel, D., A probabilistic dynamic logic, 181-195 (1982) |
| [224] | Pratt V R. Semantical consideratiosn on Floyd-Hoare logic. Technical Report, MIT, 1976 |
| [225] | Feidman, Y. A., A decidable propositional probabilistic dynamic logic, 298-309 (1983) |
| [226] | Kozen, D., A probabilistic PDL, 291-297 (1983) |
| [227] | Feldman Y A. A decidable propositional dynamic logic with explicit probabilities. Information Control, 1984, 63(1): 11-38 · Zbl 0592.68031 · doi:10.1016/S0019-9958(84)80039-X |
| [228] | Segerberg, K., Qualitative probability in a modal setting, 575-604 (1971) |
| [229] | Guelev D. A propositional dynamic logic with qualitative probabilities. Journal of philosophical logic, 1999, 28(6): 575-604 · Zbl 0939.03028 · doi:10.1023/A:1004602621885 |
| [230] | Cleaveland R, Iyer S, Narasimha M. Probabilistic temporal logics via the modalMu-Calculus. Theoretical Computer Science, 2005, 342(2): 316-350 · Zbl 1077.68058 · doi:10.1016/j.tcs.2005.03.048 |
| [231] | Konur S. An interval temporal logic for real-time system specification. PhD thesis, Department of Computer Science, University of Manchester, UK, 2008 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
