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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
@Article{McNaughton1966,
title={Testing and generating infinite sequences by a finite automaton},
author={McNaughton, Robert},
journal={Information and control},
volume={9},
number={5},
pages={521--530},
year={1966},
publisher={Elsevier}
}
@InProceedings{Maler1990,
title={Tight bounds on the complexity of cascaded decomposition of automata},
author={Maler, Oded and Pnueli, Amir},
booktitle={Foundations of Computer Science, 1990. Proceedings., 31st Annual Symposium on},
pages={672--682},
year={1990},
organization={IEEE}
}
@InProceedings{Maler1994,
title={On the Cascaded Decomposition of Automata, its Complexity and its Application to Logic},
author={Maler, Oded and Pnueli, Amir},
booktitle={ACTS Mobile Communication},
year={1994},
organization={Citeseer}
}
@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}
}
@article{Kupferman2001,
author = {Kupferman, Orna and Vardi, Moshe Y.},
title = {Model Checking of Safety Properties},
journal = {Formal Methods in System Design},
volume = 19,
issue = 3,
year = 2001,
pages = {291--314}
}
|
