tl.bib 6.66 KB
Newer Older
1

2
3
4
5
6
7
8
9
10
11
12
13
14
@InProceedings{	  babiak.12.tacas,
  author	= {Thom{\'a}{\v{s}} Babiak and Mojm{\'i}r
		  K{\v{r}}et{\'i}nsk{\'y} and Vojt{\v{e}}ch {\v{R}e}eh{\'a}k
		  and Jan Strej{\v c}ek},
  title		= {{LTL} to {B\"u}chi Automata Translation: Fast and More
		  Deterministic},
  year		= 2012,
  booktitle	= {Proceedings of the 18th International Conference on Tools
		  and Algorithms for the Construction and Analysis of Systems
		  (TACAS'12)},
  note		= {To appear}
}

15
16
17
18
19
20
@InProceedings{	  beer.01.cav,
  author	= {Ilan Beer and Shoham Ben-David and Cindy Eisner and Dana
		  Fisman and Anna Gringauze and Yoav Rodeh},
  title		= {The Temporal Logic Sugar},
  booktitle	= {Proceedings of the 13th international conferance on
		  Computer Aided Verification (CAV'01)},
21
  series	= {Lecture Notes in Computer Science},
22
23
24
25
26
27
28
29
30
  editor	= {Berry, Gérard and Comon, Hubert and Finkel, Alain},
  publisher	= {Springer},
  isbn		= {978-3-540-42345-4},
  pages		= {363--367},
  volume	= {2102},
  year		= {2001},
  month		= jul
}

31
32
33
34
35
36
37
38
39
@Article{	  bruggeman.96.tcs,
  author	= {Anne Br{\"u}ggemann-Klein},
  title		= {Regular Expressions into Finite Automata},
  journal	= {Theoretical Computer Science},
  year		= {1996},
  volume	= {120},
  pages		= {87--98}
}

40
41
42
43
44
45
46
47
48
49
50
51
52
@InProceedings{	  cerna.03.mfcs,
  author	= {Ivana {\v{C}}ern{\'a} and Radek Pel{\'a}nek},
  title		= {Relating Hierarchy of Temporal Properties to Model
		  Checking},
  booktitle	= {Proceedings of the 28th International Symposium on
		  Mathematical Foundations of Computer Science (MFCS'03)},
  pages		= {318--327},
  year		= {2003},
  editor	= {Branislav Rovan and Peter Vojt{\'a}{\v{a}}},
  volume	= {2747},
  series	= {Lecture Notes in Computer Science},
  address	= {Bratislava, Slovak Republic},
  month		= aug,
53
54
55
  publisher	= {Springer-Verlag}
}

56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
@InProceedings{	  chang.92.icalp,
  author	= {Edward Y. Chang and Zohar Manna and Amir Pnueli},
  title		= {Characterization of Temporal Property Classes},
  booktitle	= {Proceedings of the 19th International Colloquium on
		  Automata, Languages and Programming (ICALP'92)},
  year		= {1992},
  pages		= {474--486},
  publisher	= {Springer-Verlag},
  address	= {London, UK}
}

@Article{	  cimatti.08.tcad,
  author	= {Alessandro Cimatti and Marco Roveri and Stefano Tonetta},
  journal	= {IEEE Transactions on Computer Aided Design of Integrated
		  Circuits and Systems},
  number	= 10,
  pages		= {1737--1750},
  title		= {Symbolic Compilation of PSL},
  volume	= 27,
  year		= 2008,
  date		= {2009-03-20},
  note		= {\url{https://es.fbk.eu/people/tonetta/tests/tcad07/}}
}

80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
@InProceedings{	  duret.11.vecos,
  author	= {Alexandre Duret-Lutz},
  title		= {{LTL} Translation Improvements in {Spot}},
  booktitle	= {Proceedings of the 5th International Workshop on
		  Verification and Evaluation of Computer and Communication
		  Systems (VECoS'11)},
  year		= {2011},
  series	= {Electronic Workshops in Computing},
  address	= {Tunis, Tunisia},
  month		= sep,
  publisher	= {British Computer Society},
  abstract	= {Spot is a library of model-checking algorithms. This paper
		  focuses on the module translating LTL formul{\ae} into
		  automata. We discuss improvements that have been
		  implemented in the last four years, we show how Spot's
		  translation competes on various benchmarks, and we give
		  some insight into its implementation.},
  url		= {http://ewic.bcs.org/category/15853}
}

100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
@Book{		  eisner.06.psl,
  author	= {Cindy Eisner and Dana Fisman},
  title		= {A Practical Introduction to {PSL}},
  publisher	= {Springer},
  year		= {2006},
  series	= {Series on Integrated Circuits and Systems}
}

@InCollection{	  eisner.08.hvc,
  author	= {Cindy Eisner and Dana Fisman},
  title		= {Structural Contradictions},
  booktitle	= {Proceedings of the 4th International Haifa Verification
		  Conference (HVC'2008)},
  series	= {Lecture Notes in Computer Science},
  editor	= {Hana Chockler and Alan Hu},
  publisher	= {Springer},
  isbn		= {978-3-642-01701-8},
  pages		= {164--178},
  volume	= {5394},
  year		= {2009},
  month		= oct
}

123
124
125
126
127
128
129
130
131
132
133
134
@InProceedings{	  etessami.00.concur,
  author	= {Kousha Etessami and Gerard J. Holzmann},
  title		= {Optimizing {B\"u}chi Automata},
  booktitle	= {Proceedings of the 11th International Conference on
		  Concurrency Theory (Concur'00)},
  pages		= {153--167},
  year		= {2000},
  editor	= {C. Palamidessi},
  volume	= {1877},
  series	= {Lecture Notes in Computer Science},
  address	= {Pennsylvania, USA},
  publisher	= {Springer-Verlag},
135
136
137
138
139
140
141
  note		= {Beware of a typo in the version from the proceedings: $f
		  \U g$ is purely eventual if both operands are purely
		  eventual. The revision of the paper available at
		  \url{http://www.bell-labs.com/project/TMP/} is fixed. We
		  fixed the bug in Spot in 2005, thanks to LBTT. See also
		  \url{http://arxiv.org/abs/1011.4214v2} for a discussion
		  about this problem.}
142
143
}

144
145
146
147
148
149
150
151
152
153
@InProceedings{	  manna.87.podc,
  author	= {Zohar Manna and Amir Pnueli},
  title		= {A hierarchy of temporal properties},
  booktitle	= {Proceedings of the sixth annual ACM Symposium on
		  Principles of distributed computing (PODC'90)},
  year		= {1990},
  location	= {Quebec City, Canada},
  pages		= {377--410},
  publisher	= {ACM},
  address	= {New York, NY, USA}
154
155
}

156
157
158
159
160
161
@Book{		  psl.04.lrm,
  title		= {Property Specification Language Reference Manual v1.1},
  publisher	= {Accellera},
  year		= {2004},
  month		= jun,
  note		= {\url{http://www.eda.org/vfv/}}
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
}

@InProceedings{	  schneider.01.lpar,
  author	= {Klaus Schneider},
  title		= {Improving Automata Generation for Linear Temporal Logic by
		  Considering the Automaton Hierarchy},
  booktitle	= {Proceedings of the 8th International Conference on Logic
		  for Programming, Artificial Intelligence and Reasoning},
  pages		= {39--54},
  year		= {2001},
  volume	= {2250},
  series	= {Lecture Notes in Artificial Intelligence},
  address	= {Havana, Cuba},
  publisher	= {Springer-Verlag}
}

178
179
180
181
182
183
184
185
186
187
188
189
190
@InProceedings{	  somenzi.00.cav,
  author	= {Fabio Somenzi and Roderick Bloem},
  title		= {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}},
  booktitle	= {Proceedings of the 12th International Conference on
		  Computer Aided Verification (CAV'00)},
  pages		= {247--263},
  year		= {2000},
  volume	= {1855},
  series	= {Lecture Notes in Computer Science},
  address	= {Chicago, Illinois, USA},
  publisher	= {Springer-Verlag}
}

191
192
193
194
195
196
197
198
199
200
201
202
203
204
@TechReport{	  tauriainen.03.a83,
  author	= {Heikki Tauriainen},
  title		= {On Translating Linear Temporal Logic into Alternating and
		  Nondeterministic Automata},
  institution	= {Helsinki University of Technology, Laboratory for
		  Theoretical Computer Science},
  address	= {Espoo, Finland},
  month		= dec,
  number	= {A83},
  pages		= {132},
  type		= {Research Report},
  year		= {2003},
  note		= {Reprint of Licentiate's thesis}
}