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
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
|
@Article{Meyer1969,
title={A note on star-free events},
author={Meyer, Albert R},
journal={Journal of the ACM (JACM)},
volume={16},
number={2},
pages={220--225},
year={1969},
publisher={ACM}
}
@Article{Krohn1965,
title={Algebraic theory of machines. I. Prime decomposition theorem for finite semigroups and machines},
author={Krohn, Kenneth and Rhodes, John},
journal={Transactions of the American Mathematical Society},
volume={116},
pages={450--464},
year={1965},
publisher={JSTOR}
}
@InCollection{Maler2010,
title={On the krohn-rhodes cascaded decomposition theorem},
author={Maler, Oded},
booktitle={Time for verification},
pages={260--278},
year={2010},
publisher={Springer}
}
@InCollection{Roggenbach2002,
title={Determinization of B{\"u}chi-automata},
author={Roggenbach, Markus},
booktitle={Automata logics, and infinite games},
pages={43--60},
year={2002},
publisher={Springer}
}
@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}
}
@inproceedings{Latvala2003,
author = {Latvala, Timo},
title = {Efficient Model Checking of Safety Properties},
booktitle = {Model Checking Software. SPIN 2003},
editor = {Ball, Thomas and Rajamani, Sriram K.},
year = 2003,
pages = {74--88}
}
@inproceedings{Safra1988,
author = {Safra, S.},
title = {On The Complexity of $\omega$-Automata},
booktitle = {29th Annual Symposium on Foundations of Computer Science},
pages = {319--327},
year = 1988
}
|
