1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
|
@Article{Markey2003,
author = {Markey, Nicolas},
title = {Temporal logic with past is exponentially more succinct},
journal = {EATCS Bulletin},
year = {2003},
volume = {79},
pages = {122--128},
publisher = {European Association for Theoretical Computer Science},
}
@InProceedings{Gabbay1989,
author = {Gabbay, Dov},
title = {The declarative past and imperative future: executable temporal logic for interactive systems},
booktitle = {Temporal logic in specification},
year = {1989},
organization = {Springer},
pages = {409--448},
}
@phdthesis{Kamp1968,
title={Tense logic and the theory of linear order},
author={Kamp, Johan Anthony Wilem},
year={1968}
}
@InProceedings{Lichtenstein1985,
author = {Lichtenstein, Orna and Pnueli, Amir and Zuck, Lenore},
title = {The glory of the past},
booktitle = {Workshop on Logic of Programs},
year = {1985},
organization = {Springer},
pages = {196--218},
}
@InProceedings{Gabbay1980,
author = {Gabbay, Dov and Pnueli, Amir and Shelah, Saharon and Stavi, Jonathan},
title = {On the temporal analysis of fairness},
booktitle = {Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
year = {1980},
organization = {ACM},
pages = {163--173},
}
@Article{Moser1994,
author = {Moser, Louise E. and Melliar-Smith, PM and Kutty, George and Ramakrishna, YS},
title = {Completeness and soundness of axiomatizations for temporal logics without next},
journal = {Fundamenta Informaticae},
year = {1994},
volume = {21},
number = {4},
pages = {257--305},
publisher = {IOS Press},
}
@InProceedings{Laroussinie2002,
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and Schnoebelen, Philippe},
title = {Temporal logic with forgettable past},
booktitle = {Logic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on},
year = {2002},
organization = {IEEE},
pages = {383--392},
}
@Book{Prior1957,
author = {Prior, Arthur N},
title = {Time and modality},
year = {1957},
publisher = {Clarendon Press},
}
@inproceedings{FiterauBrostean2017,
author = {Fiterau-Brostean, Paul and Lenaerts, Toon and Poll, Erik and De Ruiter, Joeri and Vaandrager, Frits and Verleg, Patrick},
title = {Model Learning and Model Checking of SSH Implementations},
booktitle = {Proceedings 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 13--14 July 2017, Santa Barbara, USA},
year = 2017,
pages = {142--151}
}
@inproceedings{Havelund2002,
author = {Havelund, Klaus and Ro\c{s}u, Grigore},
title = {Synthesizing Monitors for Safety Properties},
booktitle = {International Conference on Tools and Algorithms for the Contruction and Analysis of Systems, TACAS 2002},
year = 2002,
pages = {342--356}
}
@article{Etessami2002,
author = {Etessami, Kousha and Vardi, Moshe Y. and Wilke, Thomas},
title = {First-Order Logic with Two Variables and Unary Temporal Logic},
journal = {Information and Computation},
volume = 179,
issue = 2,
year = 2002,
pages = {279--295}
}
@article{Sistla1985,
author = {Sistla, A. P. and Clarke, E. M.},
title = {The Complexity of Propositional Linear Temporal Logics},
journal = {Journal of the ACM},
volume = 32,
issue = 3,
year = 1985,
pages = {733--749}
}
|
