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

doi:10.1007/s11704-013-2195-2

Front. Comput. Sci.

2013, Vol. 7

Issue (3) : 370-403 https://doi.org/10.1007/s11704-013-2195-2

REVIEW ARTICLE

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

Savas KONUR(

)

Department of Computer Science, the University of Liverpool, Liverpool L69 3BX, UK

Download: PDF(515 KB) HTML
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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

Corresponding Author(s): KONUR Savas,Email:konur@liverpool.ac.uk

Issue Date: 01 June 2013

Cite this article:

Savas KONUR. A survey on temporal logics for specifying and verifying real-time systems[J]. Front. Comput. Sci., 2013, 7(3): 370-403.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-013-2195-2
https://academic.hep.com.cn/fcs/EN/Y2013/V7/I3/370

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 doi: 10.1109/LICS.1990.113764
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
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 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 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. 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 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. In: Proceedings of the 2nd ACM Symposium on Principles of Distributed Computing . 1983, 173-186 doi: 10.1145/800221.806720
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 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 doi: 10.1145/115234.115351
18	Allen J. Maintaining knowledge about temporal intervals. Communications of the ACM , 1983, 26(11): 832-843 doi: 10.1145/182.358434
19	Venema Y. A modal logic for chopping intervals. Journal of Logic and Computation , 1991, 1(4): 453-476 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
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 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 doi: 10.1007/BF00258426
26	Dowty D. Word meaning and montague grammar. Dordrecht: Dff 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 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 doi: 10.1305/ndjfl/1093870150
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 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 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 doi: 10.1016/0004-3702(90)90053-3
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 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. 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 doi: 10.1016/0022-0000(82)90003-4
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 doi: 10.1007/BFb0036915
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 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. 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 doi: 10.1145/3828.3837
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 doi: 10.1145/371282.371311
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 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 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 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 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 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, 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 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 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 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. 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 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 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 doi: 10.1145/5397.5399
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 doi: 10.1137/S0097539793304741
72	Reynolds M. An axiomatization of full computation tree logic. Journal of Symbolic Logic , 2001, 66: 1011-1057 doi: 10.2307/2695091
73	Reynolds M. An axiomatization of PCTL. Information and Computation , 2005, 201(1): 72-119 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 doi: 10.1006/inco.1999.2817
75	Bozzelli L. The complexity of CTL* + linear past. In: Amadio R, ed, Foundations of Software Science and Computational Structures . Springer, 2008, 186-200 doi: 10.1007/978-3-540-78499-9_14
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 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
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 doi: 10.1006/inco.1998.2778
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 doi: 10.1016/0304-3975(89)90138-2
86	Andréka H, Németi I, Sain I. Mathematical foundations of computer science. Lecture Notes in Computer Science , 1979, 208-218 doi: 10.1007/3-540-09526-8_17
87	Reynolds M. Axiomatising first-order temporal logic: until and since over linear time. Studia Logica , 1996, 57(2): 279-302 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 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. In: Proceedings of the 5th Kurt G?del Colloquium on Computational Logic and Proof Theory . 1997, 241-254 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 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 doi: 10.1023/A:1004275029985
93	Gr?del E. On the restraining power of guards. Journal of Symbolic Logic , 1999, 64: 1719-1742 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 doi: 10.1016/S0168-0072(00)00018-X
95	B?rger E, Gr?del E, Gurevich Y. The classical decision problem. Springer , 1997 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. 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 doi: 10.1023/A:1021352309671
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 doi: 10.1023/A:1021308527417
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 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 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. 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 doi: 10.1145/227595.227602
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 doi: 10.1007/BFb0055086
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 doi: 10.1145/1342991.1342994
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 doi: 10.1007/11603009_2
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 doi: 10.1007/s002360050136
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 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. 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 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. 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 doi: 10.1109/32.910858
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 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-52 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 doi: 10.1093/logcom/9.6.897
142	Marx D, Venema Y. Multi-dimensional modal logics. Kluwer Academic Press , 1997 doi: 10.1007/978-94-011-5694-3
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 doi: 10.1007/978-3-540-87531-4_23
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 doi: 10.1007/978-3-540-72734-7_7
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 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 doi: 10.1007/s10817-006-9051-0
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 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? 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 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. 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 doi: 10.1016/j.artint.2005.04.003
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 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 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. 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 doi: 10.1016/S0020-0190(98)00027-1
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 doi: 10.1007/3-540-61648-9_40
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 doi: 10.1093/logcom/10.6.877
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 doi: 10.1007/BFb0027804
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 doi: 10.1007/BFb0055347
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 doi: 10.1007/3-540-49059-0_14
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 doi: 10.1007/978-3-540-71209-1_17
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 doi: 10.1145/1035429.1035432
183	Barua R, Roy S, Chaochen Z. Completeness of neighbourhood logic. Journal of Logic and Computation , 2000, 10(2): 271-295 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. 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 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. 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 doi: 10.1007/BFb0028779
189	Pandya P. Interval duration logic: expressiveness and decidability. Electronic Notes in Theoretical Computer Science , 2002, 65(6): 254-272 doi: 10.1016/S1571-0661(04)80480-8
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 doi: 10.1007/978-3-540-31980-1_20
191	Chakravorty G, Pandya P. Digitizing interval duration logic. In: Hunt JW, Somenzi F, eds, Computer Aided Verification. Springer Berlin Heidelberg , 2003, 167-179 doi: 10.1007/978-3-540-45069-6_17
192	Filliatre 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 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 doi: 10.1007/s001650050034
194	Fagin R, Halpern J Y. Reasoning about knowledge and probability. Journal of the ACM , 1994, 41(2): 340-367 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 doi: 10.1002/malq.200310044
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 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 doi: 10.1007/BF01211866
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 doi: 10.1007/3-540-60045-0_48
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 doi: 10.1007/3-540-60692-0_70
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 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. 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 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 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. 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 doi: 10.1016/S0304-3975(01)00046-9
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 doi: 10.1007/3-540-45352-0_22
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 doi: 10.1145/322123.322138
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 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 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 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. Artificial Intelligence , 1993, 64(2): 337-351 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 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. 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 doi: 10.1016/S0019-9958(84)80039-X
228	Segerberg K. Qualitative probability in a modal setting. In: Proceedings of the 2nd Scandinavian Logic Symposium . 1971, 575-604 doi: 10.1016/S0049-237X(08)70852-8
229	Guelev D. A propositional dynamic logic with qualitative probabilities. Journal of philosophical logic , 1999, 28(6): 575-604 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 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

[1]	Yuanrui ZHANG, Frédéric MALLET, Yixiang CHEN. A verification framework for spatio-temporal consistency language with CCSL as a specification language[J]. Front. Comput. Sci., 2020, 14(1): 105-129.
[2]	Kazuhiro OGATA. A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions[J]. Front. Comput. Sci., 2019, 13(1): 51-72.
[3]	Anil Kumar KARNA, Yuting CHEN, Haibo YU, Hao ZHONG, Jianjun ZHAO. The role of model checking in software engineering[J]. Front. Comput. Sci., 2018, 12(4): 642-668.
[4]	Yu ZHOU, Nvqi ZHOU, Tingting HAN, Jiayi GU, Weigang WU. Probabilistic verification of hierarchical leader election protocol in dynamic systems[J]. Front. Comput. Sci., 2018, 12(4): 763-776.
[5]	Fei HE, Yuan GAO, Liangze YIN. Efficient software product-line model checking using induction and a SAT solver[J]. Front. Comput. Sci., 2018, 12(2): 264-279.
[6]	Laixiang SHAN,Xiaomin DU,Zheng QIN. Efficient approach of translating LTL formulae into Büchi automata[J]. Front. Comput. Sci., 2015, 9(4): 511-523.
[7]	Luxi CHEN,Linpeng HUANG,Chen LI,Tao ZAN. Integrating behavior analysis into architectural modeling[J]. Front. Comput. Sci., 2015, 9(1): 15-33.
[8]	Yuanjie SI, Jun SUN, Yang LIU, Jin Song DONG, Jun PANG, Shao Jie ZHANG, Xiaohu YANG. Model checking with fairness assumptions using PAT[J]. Front. Comput. Sci., 2014, 8(1): 1-16.
[9]	Anh Tuan LUU, Jun SUN, Yang LIU, Jin Song DONG, Xiaohong LI, Thanh Tho QUAN. SeVe: automatic tool for verification of security protocols[J]. Front Comput Sci, 2012, 6(1): 57-75.
[10]	Conghua ZHOU, Bo SUN, Zhifeng LIU. Abstraction for model checking multi-agent systems[J]. Front Comput Sci Chin, 2011, 5(1): 14-25.
[11]	Jiaqi ZHU, Hanpin WANG, Zhongyuan XU, Chunxiang XU, . A new model for model checking: cycle-weighted Kripke structure[J]. Front. Comput. Sci., 2010, 4(1): 78-88.
[12]	Wanwei LIU, Ji WANG, Huowang CHEN, Xiaodong MA, Zhaofei WANG. symbolic model checking APSL[J]. Front Comput Sci Chin, 2009, 3(1): 130-141.

Viewed

Full text

Abstract

Cited

Shared

Discussed