A survey on temporal logics for specifying and verifying real-time systems

Abstract

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.

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 / expressiveness

References

[1] Bellini P, Mattolini R, Nesi P. Temporal logics for real-time system specification. ACM Computing Surveys, 2000, 32(1): 12-42

[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

[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

[4] Øhrstrøm P, Hasle P F. Temporal logic: from ancient ideas to artificial intellgience. Dordrecht, The Netherlands: Kluwer Academic Publishers, 1995

[5] Hirshfeld Y, Rabinovich A. Logics for real time: decidability and complexity. Fundamenta Informaticae, 2004, 62(1): 1-28

[6] Chaochen Z, Hansen M. Duration calculus: a formal approach to realtime systems. EATCS Series of Monographs in Theoretical Computer Science. Springer, 2004

[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

[8] Guelev D, Van Hung D. On the completeness and decidability of duration calculus with iteration. Theoretical Computer Science, 2005, 337(1): 278-304

[9] Venema Y. Temporal logic. Blackwell Guide to Philosophical Logic, Blacwell Publishers, 1998

[10] Fiaderio J L, Maibaum T. Action refinement in a temporal logic of objects. In: Gabbay D, Ohlbach H, eds, Temporal Logic. Springer LNAI 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

[12] Schwartz R L, Melliar-Smith P M, Voght F H. An interval logic for higher-level temporal reasoning. In: Proceedings of the 2nd ACM Symposium on Principles of Distributed Computing. 1983, 173-186

[13] Moszkowski B. Reasoning about digital circuits. PhD thesis, Computer Science Department, Stanford University, 1983

[14] Ladkin P. Logical time pieces. AI Expert, 1987, 2(8): 58-67

[15] Melliar-Smith P M. Extending interval logic to real time systems. In: Melliar-Smith P M, ed, Temporal Logic in Specification. Springer, 1989, 224-242

[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

[17] Halpern J Y, Shoham Y. A propositional modal logic of time intervals. Journal of the ACM, 1991, 38(4): 935-962

[18] Allen J. Maintaining knowledge about temporal intervals. Communications of the ACM, 1983, 26(11): 832-843

[19] Venema Y. A modal logic for chopping intervals. Journal of Logic and Computation, 1991, 1(4): 453-476

[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

[21] Montanari A, Sciavicco G, Vitacolonna N. Decidability of interval temporal logics over split-frames via granularity. In: Proceedings of the 8th Europian Conference on Logics in AI. 2002, 259-270

[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

[24] Hamblin C. Instants and intervals. The Study of Time, 1972, 1: 324-331

[25] Humberstone I. Interval semantics for tense logic: some remarks. Journal of philosophical logic, 1979, 8(1): 171-196

[26] Dowty D. Word meaning and montague grammar. Dordrecht: Dff Reidel, 1979

[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

[29] Burgess J P. Axioms for tense logic 2: time periods. Notre Dame Journal of Formal Logic, 1982, 23(2): 375-383

[30] Benthem V J F. The logic of time. Kluwer Academic Publishers, Dordrecht, 1983

[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

[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

[36] Galton A. A critical examination of allen’s theory of action and time. Artificial Intelligence, 1990, 42(2): 159-188

[37] Roşsu G, Bensalem S. Allen linear (interval) temporal logic- translation to ltl andmonitor synthesis. In: Proceedings of the 18th International Conference on Computer Aided Verification. 2006, 263-277

[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. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. 1979, 93-100

[40] Harel D, Kozen D, Parikh R. Process logic: expressiveness, decidability, completeness. Journal of Computer and System Sciences, 1982, 25(2): 144-170

[41] Halpern J, Manna Z, Moszkowski B. A high-level semantics based on interval logic. In: Proceedings of the 10th International Conference on Automata, Languages and Programming (ICALP). 1983, 278-291

[42] Gabbay D, Hodkinson I, Reynolds M. Temporal logic: mathematical foundations and computational aspects. Volume 1. Clarendon Press, Oxford, 1994

[43] Prior A N. Time and modality. Oxford: Clarendon Press, 1957

[44] Prior A N. Past, present and future. Oxford University Press, 1967

[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. In: Proceedings of the 18th Annual IEEE Symposium on Foundations of Computer Science. 1977, 46-57

[48] Szalas A. Temporal logic of programs: a standard approach. In: Bolc L, Szalas A, eds, Time and Logic: A Computational Approach UCL Press, 1995, 1-50.

[49] Gabbay D M, Pnueli A, Shelah S, Stavi J. On the temporal analysis of fairness. In: Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages. 1980, 163-173

[50] Sistla A, Clarke E. The complexity of propositional linear temporal logics. Journal of the ACM, 1985, 32(3): 733-749

[51] Fisher M. A resolution method for temporal logic. In: Proceedings of 12th International Joint Conference on Artificial Intelligence. 1991, 99-104

[52] Fisher M, Dixon C, Peim M. Clausal temporal resolution. ACM Transactions on Computational Logic, 2001, 2(1): 12-56

[53] Lichtenstein O, Pnueli A, Zuck L. The glory of the past. In: Parikh R, ed, Logics of Programs. Springer Berlin Heidelberg, 1985, 196-218

[54] Lichtenstein O, Pnueli A. Propositional temporal logics: decidability and completeness. Logic Journal of the IGPL, 2000, 8(1): 55-85

[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

[56] Lutz C, Walther D, Wolter F. Quantitative temporal logics over the reals: PSPACE and below. Information and Computation, 2007, 205(1): 99-123

[57] Reynolds M. The complexity of temporal logic over the reals. Annals of Pure and Applied Logic, 2010, 161(8): 1063-1096

[58] McDermott D. A temporal logic for reasoning about processes and plans. Cognitive science, 1982, 6(2): 101-155

[59] Rao A, Georg e. M. A model-theoretic approach to the verification of situated reasoning systems. In: Proceedings of the 13th International Joint Conference on Artificial Intelligence. 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. In: Proceedings of the 8th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 1981, 164-176

[62] Clarke E M, Emerson E A. Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Workshop on Logic of Programs. 1982, 52-71

[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

[64] Laroussinie F, Schnoebelen P. A hierarchy of temporal logics with past. Theoretical Computer Science, 1995, 148(2): 303-324

[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. In: Proceedings of the 14th Annual ACM Symposium on Theory of Computing. 1982, 169-180

[67] Emerson E, Srinivasan J. Branching time temporal logic. In: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. Springer, 1989, 123-172

[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

[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

[70] Penczek W. Branching time and partial order in temporal logics. In: Bolc L, Szalas A, eds, Time and Logic: A Computational Approach. UCL Press, 1995, 179-228

[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

[72] Reynolds M. An axiomatization of full computation tree logic. Journal of Symbolic Logic, 2001, 66: 1011-1057

[73] Reynolds M. An axiomatization of PCTL. Information and Computation, 2005, 201(1): 72-119

[74] Laroussinie F, Schnoebelen P. Specification in CTL+past, verification in CTL. Information and Computation, 2000, 156(1): 236-263

[75] Bozzelli L. The complexity of CTL* + linear past. In: Amadio R, ed, Foundations of Software Science and Computational Structures. Springer, 2008, 186-200

[76] Pratt V R. On the composition of processes. In: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’82. 1982, 213-223

[77] Pinter S S, Wolper P. A temporal logic for reasoning about partially ordered computations (extended abstract). In: Proceedings of the 3rd Annual ACM Symposium on Principles of Distributed Computing. 1984, 28-37

[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

[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

[81] Alexander A, Reisig W. Compositional temporal logic based on partial order. In: Proceedings of the 11th International Symposium on Temporal Representation and Reasoning, TIME ’04. 2004, 125-132

[82] Lomuscio A, Penczek W, Qu H. Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems. In: Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems, AAMAS ’10. 2010, 659-666

[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. Logics for Databases and Information Systems, 1998, 31-70

[85] Abadi M. The power of temporal proofs. Theoretical Computer Science, 1989, 65(1): 35-83

[86] Andréka H, Németi I, Sain I. Mathematical foundations of computer science. Lecture Notes in Computer Science, 1979, 208-218

[87] Reynolds M. Axiomatising first-order temporal logic: until and since over linear time. Studia Logica, 1996, 57(2): 279-302

[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

[89] Chomicki J. Efficient checking of temporal integrity constraints using bounded history encoding. ACM Transactions on Database Systems, 1995, 20(2): 149-186

[90] Pliuskevicius R. On the completeness and decidability of a restricted first order linear temporal logic. In: Proceedings of the 5th Kurt Gödel Colloquium on Computational Logic and Proof Theory. 1997, 241-254

[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

[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

[93] Grädel E. On the restraining power of guards. Journal of Symbolic Logic, 1999, 64: 1719-1742

[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

[95] Börger E, Grädel E, Gurevich Y. The classical decision problem. Springer, 1997

[96] Hodkinson I M, Wolter F, Zakharyaschev M. Monodic fragments of first-order temporal logics: 2000-2001 A.D. In: Proceedings of the 2001 Artificial Intelligence on Logic for Programming, LPAR ’01. 2001, 1-23

[97] Gabbay D, Kurucz A, Wolter F, Zakharyaschev M. Many-dimensional modal logics: theory and applications. Elsevier, 2002

[98] Degtyarev A, Fisher M, Lisitsa A. Equality and monodic first-order temporal logic. Studia Logica, 2002, 72(2): 147-156

[99] Woltert P, Zakharyaschev M. Modal description logics: modalizing roles. Fundamenta Informaticae, 1999, 39(4): 411-438

[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

[101] Dixon C, Fisher M, Konev B, Lisitsa A. Practical first-order temporal reasoning. In: Proceedings of the 15th International Symposium on Temporal Representation and Reasoning, TIME ’08. 2008, 156-163

[102] Emerson E, Mok A, Sistla A, Srinivasan J. Quantitative temporal reasoning. Real-Time Systems, 1992, 4(4): 331-352

[103] Koymans R. Specifying real-time properties with metric temporal logic. Real-Time Systems, 1990, 2(4): 255-299

[104] Alur R, Henzinger T A. A really temporal logic. Journal of the ACM, 1994, 41(1): 181-203

[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. In: Proceedings of the 7th International Joint Conference Theory and Practice of Software Development. 1996, 189-200

[107] Laroussinie F, Meyer A, Petonnet E. Counting LTL. In: Proceedings of the 17th International Symposium on Temporal Representation and Reasoning. 2010, 51-58

[108] Ouaknine J, Worrell J. Some recent results in metric temporal logic. In: Proceedings of the 6th international conference on Formal Modeling and Analysis of Timed Systems, FORMATS ’08. 2008, 1-13

[109] Ouaknine J, Worrell J. On the decidability of metric temporal logic. In: Proceedings 20th Annual IEEE Symposium on Logic in Computer Science. 2005, 188-197

[110] Alur R, Feder T, Henzinger T A. The benefits of relaxing punctuality. Journal of the ACM, 1996, 43(1): 116-146

[111] Henzinger T A, Raskin J F, Schobbens P Y. The regular real-time languages. In: Proceedings of the 25th International Colloquium on Automata, Languages and Programming. 1998, 580-591

[112] Henzinger T A. It’s about time: real-time logics reviewed. In: Proceedings of the 9th International Conference on Concurrency Theory. 1998, 439-454

[113] Lasota S, Walukiewicz I. Alternating timed automata. ACM Transactions on Computational Logic, 2008, 9(2): 1-27

[114] Maler O, Nickovic D, Pnueli A. Real time temporal logic: past, present, future. In: Pettersson P, Yi W, eds, Formal Modeling and Analysis of Timed Systems. Springer-Verlag, 2005, 2-16

[115] Bouyer P, Markey N, Ouaknine J, Worrell J. On expressiveness and complexity in real-time model checking. In: Proceedings of the 35th international colloquium on Automata, Languages and Programming, Part II, ICALP ’08. 2008, 124-135

[116] Bouyer P, Chevalier F, Markey N. On the expressiveness of TPTL and MTL. In: Proceedings of the 25th International Conference on Foundations of Software Technology and Theoretical Computer Science. 2005, 432-443

[117] Alur R, Henzinger T A. Logics and models of real time: a survey. In: Proceedings of the Real-Time: Theory in Practice, REX Workshop. 1992, 74-106

[118] Alur R, Courcoubetis C, Dill D L. Model checking for real-time systems. In: Proceedings of the 5th Conference on Logic in Computer Science. 1990, 12-21

[119] Laroussinie F, Markey N, Schnoebelen P. Model checking timed automata with one or two clocks. In: Proceedings of the 15th International Conference on Concurrency Theory. 2004, 387

[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

[122] Laroussinie F, Meyer A, Petonnet E. Counting CTL. Foundations of Software Science and Computational Structures, 2010, 206-220

[123] Jahanian F, Mok A. Safety analysis of timing properties in real-time systems. IEEE Transactions on Software Engineering, 1986, 12(9): 890-904

[124] Jahanian F, Mok A. Modechart: a specification language for real-time systems. IEEE Transactions on Software Engineering, 1994, 20(12): 933-947

[125] Jahanian F, Stuart D. A method for verifying properties of modechart specifications. In: Proceedings of the 9th Real-time Systems Symposium. 1988, 12-21

[126] Andrei S, Cheng A M K. Faster verification of RTL-specified systems via decomposition and constraint extension. In: Proceedings of the 27th IEEE International Real-Time Systems Symposium. 2006, 67-76

[127] Andrei S, Cheng A M K. Verifying linear real-time logic specifications. In: Proceedings of the 28th IEEE International Real-Time Systems Symposium. 2007, 333-342

[128] Ostroff J S, Wonham W. Modeling and verifying real-time embedded computer systems. In: Proceedings of the 8th IEEE Real-Time Systems Symposium. 1987, 124-132

[129] Ostroff J S. Temporal logic for real-time systems. Advanced Software Development Series. Research Studies Press Limited, 1989

[130] Harel E, Lichtenstein O, Pnueli A. Explicit clock temporal logic. In: Proceedings of the 5th Annual Symposium on Logic in Computer Science. 1990, 402-413

[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

[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

[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. In: Proceedings of the 2nd IEEE International Conference on Engineering of Complex Computer Systems. 1996, 18-25

[135] Mattolini R, Nesi P. An interval logic for real-time system specification. IEEE Transactions on Software Engineering, 2001, 27(3): 208-227

[136] Paulson L C. Isabelle: a generic theorem prover. Springer LNCS 828, 1994

[137] Bellini P, Giotti A, Nesi P, Rogai D. TILCO temporal logic for realtime systems implementation in C++. In: Proceedings of the 15th International Conference on Software Engineering and Knowledge Engineering. 2003, 166-173

[138] Bellini P, Giotti A, Nesi P. Execution of TILCO temporal logic specifications. In: Proceedings of the 8th International Conference on Engineering of Complex Computer Systems, ICECCS ’02. 2002, 78-87

[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

[140] Bellini P, Nesi P, Rogai D. Validating component integration with C-TILCO. Electronic Notes in Theoretical Computer Science, 2005, 116: 241-52

[141] Marx M, Reynolds M. Undecidability of compass logic. Journal of Logic and Computation, 1999, 9(6): 897-914

[142] Marx D, Venema Y. Multi-dimensional modal logics. Kluwer Academic Press, 1997

[143] Lodaya K. Sharpening the undecidability of interval temporal logic. In: Proceedings of the 6th Asian Computing Science Conference. 2000, 290-298

[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. In: Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR ’08. 2008, 590-604

[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. In: Proceedings of the 2003 International Conference Tableaux. 2003, 102-116

[147] Hodkinson I, Montanari A, Sciavicco G. Non-finite axiomatizability and undecidability of interval temporal logics with C, D, and T. In: Proceedings of the 22nd International Workshop on Computer Science Logic. 2008, 308-322

[148] Chaochen Z, Hansen M. An adequate first order interval logic. In: Revised Lectures from the International Symposium on Compositionality: The Significant Difference. 1997, 584-608

[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. In: Proceedings of the 24th Annual Conference on Theoretical Aspects of Computer Science. 2007, 549-560

[151] Bresolin D, Goranko V, Montanari A, Sciavicco G. On decidability and expressiveness of propositional interval neighbourhood logics. In: Proceedings of the International Symposium on Logical Foundations of Computer Science. 2007, 84-99

[152] Bresolin D, Montanari A. A tableau-based decision procedure for right propositional neighborhood logic. In: Proceedings of the 14th international conference on Automated Reasoning with Analytic Tableaux and Related Methods. 2005, 63-77

[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

[154] Bresolin D, Della Monica D, Goranko V, Montanari A, Sciavicco G. Metric propositional neighborhood logics: expressiveness, decidability, and undecidability. In: Proceedings of the 19th European Conference on Artificial Intelligence. 2010, 695-700

[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

[156] Chagrov A V, Rybakov M N. How many variables does one need to prove PSPACE-hardness of modal logics? In: Advances in Modal Logic. 2003, 71-82

[157] Demri S, Gore R. An O((n. log n)3)time transformation from Grz into decidable fragments of classical first-order logic. In: Selected Papers from Automated Deduction in Classical and Non-Classical Logics. 2000, 153-167

[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

[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. In: Proceedings of the 17th International Symposium on Temporal Representation and Reasoning. 2010, 27-34

[160] Marcinkowski J, Michaliszyn J. The ultimate undecidability result for the Halpern-shoham logic. In: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science. 2011, 377-386

[161] Pratt-Hartmann I. Temporal prepositions and their logic. Artificial Intelligence, 2005, 166(1-2): 1-36

[162] Konur S. A decidable temporal logic for events and states. In: Proceedings of the 13th International Symposium on Temporal Representation and Reasoning. 2006, 36-41

[163] Chaochen Z, Hoare C, Ravn A. A calculus of durations. Information Processing Letters, 1991, 40(5): 269-276

[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. In: Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science. 2000, 242-251

[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. In: Proceedings of the IFIP TC2/WG2. 1/WG2. 2/WG2. 3 Working Conference on Programming Concepts, Methods and Calculi. 1994, 307-326

[168] Chaochen Z, Hansen M, Sestoft P. Decidability and undecidability results for duration calculus. In: Proceedings of the 10th Symposium on Theoretical Aspects of Computer Science. 1993, 58-68

[169] Rabinovich A. Non-elementary lower bound for propositional duration calculus. Information Processing Letters, 1998, 66(1): 7-11

[170] Fränzle M. Synthesizing controllers from duration calculus. In: Proceedings of the 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. 1996, 168-187

[171] Guelev D, Dang V H. On the completeness and decidability duration calculus with iteration. In: Thiagarajan P S, Yap R, eds, Advances in Computer Science. Springer, 1999, 139-150

[172] Chetcuti-Serandio N, Cerro L D. A mixed decision method for duration calculus. Journal of Logic and Computation, 2000, 10(6): 877-895

[173] Pandya P K. Specifying and deciding quantified discrete-time duration calculus formulas using DCVALID. In: Proceedings of the 2001 Workshop on Real-Time Tools. 2001

[174] Zhou C. Linear duration invariants. In: Proceedings of the 3rd International Symposium Organized Jointly with the Working Group Provably Correct Systems on Formal Techniques in Real-Time and Fault-Tolerant Systems. 1994, 86-109

[175] Xuandong L, Hung D. Checking linear duration invariants by linear programming. In: Proceedings of the 2nd Asian Computing Science Conference on Concurrency and Parallelism, Programming, Networking, and Security. 1996, 321-332

[176] Thai P H, Hung D V. Checking a regular class of duration calculus models for linear duration invariants. In: Proceedings of the International Symposium on Software Engineering for Parallel and Distributed Systems. 1998, 61-71

[177] Thai P, Van Hung D. Verifying linear duration constraints of timed automata. In: Proceedings of the 1st International Conference on Theoretical Aspects of Computing. 2004, 295-309

[178] Satpathy M, Hung D V, Pandya P K. Some decidability results for duration calculus under synchronous interpretation. In: Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. 1998, 186-197

[179] Fränzle M. Take it NP-easy: Bounded model construction for duration calculus. In: Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems: Cosponsored by IFIP WG 2.2. 2002, 245-264

[180] Biere A, Cimatti A, Clarke E M, Zhu Y. Symbolic model checking without BDDs. In: Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems. 1999, 193-207

[181] Fränzle M, Hansen M. Deciding an interval logic with accumulated durations. In: Proceedings of the 13th international conference on Tools and algorithms for the construction and analysis of systems. 2007, 201-215

[182] Hansen M R, Sharp R. Using interval logics for temporal analysis of security protocols. In: Proceedings of the 2003 ACM Workshop on Formal Methods in Security Engineering. 2003

[183] Barua R, Roy S, Chaochen Z. Completeness of neighbourhood logic. Journal of Logic and Computation, 2000, 10(2): 271-295

[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. Formal Methods for Real-Time Computing, 1996, 55-82

[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

[187] Bengtsson J, Larsen K, Larsson F, Pettersson P, Yi W. UPPAAL-a tool suite for automatic verification of real-time systems. In: Proceedings of the DIMACS/SYCON Workshop on Hybrid systems III : Verification and Control. 1996, 232-243

[188] Bozga M, Daws C, Maler O, Olivero A, Tripakis S, Yovine S. Kronos: a model-checking tool for real-time systems. In: Proceedings of the 10th International Conference on Computer Aided Verification. 1998, 546-550

[189] Pandya P. Interval duration logic: expressiveness and decidability. Electronic Notes in Theoretical Computer Science, 2002, 65(6): 254-272

[190] Sharma B, Pandya P, Chakraborty S. Bounded validity checking of interval duration logic. In: Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2005, 301-316

[191] Chakravorty G, Pandya P. Digitizing interval duration logic. In: Hunt JW, Somenzi F, eds, Computer Aided Verification. Springer Berlin Heidelberg, 2003, 167-179

[192] Filliâtre J, Owre S, Rueß H, Shankar N. ICS: integrated canonizer and solver. In: Proceedings of the 13th International Conference on Computer Aided Verification. 2001, 246-249

[193] Van Hung D, Chaochen Z. Probabilistic duration calculus for continuous time. Formal Aspects of Computing, 1999, 11(1): 21-44

[194] Fagin R, Halpern J Y. Reasoning about knowledge and probability. Journal of the ACM, 1994, 41(2): 340-367

[195] Marković Z, Ognjanović Z, Rašković M. A probabilistic extension of intuitionistic logic. Mathematical Logic Quarterly, 2003, 49(4): 415-424

[196] Hansson H, Jonsson B. A framework for reasoning about time and reliability. In: Proceedings of the 1999 Real Time Systems Symposium. 1989, 102-111

[197] Hansson H, Jonsson B. A logic for reasoning about time and reliability. Formal Aspects of Computing, 1994, 6(5): 512-535

[198] Brázdil T, Forejt V, Kretinsky J, Kucera A. The satisfiability problem for probabilistic CTLw. In: Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science. 2008, 391-402

[199] Aziz A, Singhal V, Balarin F. It usually works: the temporal logic of stochastic systems. In: Proceedings of the 7th International Conference on Computer Aided Verification. 1995, 155-165

[200] Bianco A, Alfaro L. Model checking of probabalistic and nondeterministic systems. In: Proceedings of the 15th Conference on Foundations of Software Technology and Theoretical Computer Science. 1995, 499-513

[201] Kwiatkowska M, Norman G, Segala R, Sproston J. Automatic verification of real-time systems with discrete probability distributions. In: Katoen J P, ed, Formal Methods for Real-Time and Probabilistic Systems. Springer, 1999, 75-95

[202] Kwiatkowska M, Norman G, Segala R, Sproston J. Verifying quantitative properties of continuous probabilistic timed automata. In: Proceedings of the 11th International Conference on Concurrency Theory. 2000, 123-137

[203] Jurdzinski M, Laroussinie F, Sproston J. Model checking probabilistic timed automata with one or two clocks. In: Abdulla P, Leino K, eds, Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2007, 170-184

[204] Ognjanović Z. Discrete linear-time probabilistic logics: completeness, decidability and complexity. Journal of Logic and Computation, 2006, 16(2): 257-285

[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. In: Proceedings of the 13th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications. 2007, 165-172

[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

[209] Guelev D P. Probabilistic neighbourhood logic. In: Proceedings of the 6th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. 2000, 264-275

[210] Guelev D. Probabilistic neighbourhood logic. Research Report 196, UNU/IIST, 2000

[211] Guelev D P. Probabilistic interval temporal logic. Technical Report 144, UNU/IIST, 1998

[212] Segerberg K. A completeness theorem in the modal logic of programs. In: Traczyk T, ed, Universal Algebra. Banach Centre Publications, 1982, 31-46

[213] Pippenger N, Fischer M J. Relations among complexity measures. Journal of the ACM, 1979, 26(2): 361-381

[214] Harel D, Tiuryn J, Kozen D. Dynamic Logic. Cambridge, MA, USA: MIT Press, 2000

[215] Lamport L. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 1994, 16(3): 872-923

[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

[217] Kowalski R, Sergot M. A logic-based calculus of events. New Generation Computing, 1986, 4(1): 67-95

[218] Shoham Y. Reasoning about Action and Change. MIT Press, 1987

[219] Reiter R. Proving properties of states in the situation calculus. Artificial Intelligence, 1993, 64(2): 337-351

[220] Gelfond M, Lifschitz V. Representing action and change by logic programs. The Journal of Logic Programming, 1993, 17(2): 301-321

[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. In: Proceedings of the 20th Annual Symposium on Foundations of Computer Science. 1979, 101-114

[223] Feldman Y A, Harel D. A probabilistic dynamic logic. In: Proceedings of the 14th Annual ACM Symposium on Theory of Computing. 1982, 181-195

[224] Pratt V R. Semantical consideratiosn on Floyd-Hoare logic. Technical Report, MIT, 1976

[225] Feidman Y A. A decidable propositional probabilistic dynamic logic. In: Proceedings of the 15th Annual ACM Symposium on Theory of Computing. 1983, 298-309

[226] Kozen D. A probabilistic PDL. In: Proceedings of the 15th annual ACM symposium on Theory of Computing. 1983, 291-297

[227] Feldman Y A. A decidable propositional dynamic logic with explicit probabilities. Information Control, 1984, 63(1): 11-38

[228] Segerberg K. Qualitative probability in a modal setting. In: Proceedings of the 2nd Scandinavian Logic Symposium. 1971, 575-604

[229] Guelev D. A propositional dynamic logic with qualitative probabilities. Journal of philosophical logic, 1999, 28(6): 575-604

[230] Cleaveland R, Iyer S, Narasimha M. Probabilistic temporal logics via the modalMu-Calculus. Theoretical Computer Science, 2005, 342(2): 316-350

[231] Konur S. An interval temporal logic for real-time system specification. PhD thesis, Department of Computer Science, University of Manchester, UK, 2008

RIGHTS & PERMISSIONS

2014 Higher Education Press and Springer-Verlag Berlin Heidelberg