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
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
|
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0//EN">
<HTML><HEAD>
<TITLE>LBT: LTL to Bchi converter</TITLE>
<LINK REV=MADE HREF="mailto:msmakela@tcs.hut.fi">
</HEAD>
<BODY>
<H1>LBT: LTL to Bchi conversion</H1>
<P>This piece of software provides a C++ implementation for an
algorithm that converts a linear temporal logic formula to a
generalised Bchi automaton. The algorithm comes from</P>
<BLOCKQUOTE><P>R. Gerth, D. Peled, Y. Vardi, and
<A HREF="http://www.montefiore.ulg.ac.be/%7Epw/">P. Wolper</A>.
<BR>
<EM><A HREF="http://www.montefiore.ulg.ac.be/%7Epw/papers/psfiles/GPVW95.ps">Simple on-the-fly automatic verification of linear temporal logic.</A></EM>
PSTV'95, Fifteenth International Symposium on PROTOCOL SPECIFICATION, TESTING AND VERIFICATION, Warsaw, Poland, 1995.</P></BLOCKQUOTE>
<P>The resulting automaton may be used, for instance, in model
checking, where it represents a property to be verified from a model
(e.g. a Petri net).</P>
<H2>Copyright</H2>
<P>The implementation is Copyright 1999 <A
HREF="http://staff.cs.utu.fi/%7Emronkko/PROJECT/LTL2BUCHI/abstract.html">Mauno
Rnkk</A> <mauno.ronkko@cs.utu.fi>. The original copyright
statement follows:</P>
<BLOCKQUOTE><P>This product contains free software; you can
redistribute it and/or modify it under the terms of the <A
HREF="http://www.fsf.org/copyleft/gpl.html">GNU General Public
License</A> as published by the <A HREF="http://www.fsf.org/">Free
Software Foundation</A>; either version 2 of the License, or (at your
option) any later version. These terms also apply to any hardware
schemas and any other information presented in the www-pages
below.</P>
<P>This product information is distributed in the hope that it will
be useful, but WITHOUT ANY WARRANTY; without even the implied warranty
of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. This also
applies to any hardware schemas and any other information described in
the www-pages below. See the GNU General Public License for more
details. You should be able to read the GNU General Public License
via the above link; if not, write to the Free Software Foundation,
Inc., 675 Mass Ave, Cambridge, MA 02139, USA.</P></BLOCKQUOTE>
<P>Enhancements and packaging are 1999-2001,2004 Heikki Tauriainen
<heikki.tauriainen@hut.fi>, and 2001,2002,2004 Marko Mkel
<marko.makela@hut.fi>.</P>
<H1>Interfacing the Translator</H1>
<P>The translator is designed to be invoked as a subprocess. It
parses a linear temporal logic from standard input and writes a
corresponding generalised Bchi automaton to standard output, and
exits. Both the input and output format are based on prefix notation
that facilitate straightforward recursive-descent parsing.</P>
<H2>Grammar Definitions</H2>
<P>The grammar is presented in Backus-Naur Form, one grammar rule per
line. Comments delimited by the symbols <EM>/*</EM> and <EM>*/</EM>
are not part of the formal grammar. Non-terminal symbols are enclosed
within single quotes or presented as <A
HREF="http://www.gnu.org/software/flex/flex.html">Flex</A>-style
regular-expressions.</P>
<H3>Input format for LTL formulae</H3>
<H4>Propositional operators</H4>
<TABLE>
<TR>
<TD><A NAME="f"><f></A> ::=</TD>
<TD><CODE>'t'</CODE></TD>
<TD><EM>/* true */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'f'</CODE></TD>
<TD><EM>/* false */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'p'[0-9]+</CODE></TD>
<TD><EM>/* proposition */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'!'</CODE>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* negation */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'|'</CODE>
<<A HREF="#f">f</A>>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* disjunction */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'&'</CODE>
<<A HREF="#f">f</A>>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* conjunction */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'i'</CODE>
<<A HREF="#f">f</A>>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* implication:
<CODE>"i <f1> <f2>"</CODE> is short-hand for
<CODE>"| ! <f1> <f2>"</CODE> */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'e'</CODE>
<<A HREF="#f">f</A>>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* equivalence */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'^'</CODE>
<<A HREF="#f">f</A>>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* exclusive disjunction (xor) */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>[ \t\n\r\v\f]</CODE> <<A HREF="#f">f</A>></TD>
<TD><EM>/* white space is ignored */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><<A HREF="#f">f</A>> <CODE>[ \t\n\r\v\f]</CODE></TD>
<TD><EM>/* white space is ignored */</EM></TD>
</TR>
</TABLE>
<H4>Temporal operators</H4>
<TABLE>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'X'</CODE>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* next */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'F'</CODE>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* finally, eventually */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'G'</CODE>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* globally, henceforth */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'U'</CODE>
<<A HREF="#f">f</A>>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* until */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'V'</CODE>
<<A HREF="#f">f</A>>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* release */</EM></TD>
</TR>
</TABLE>
<H2>Output format for generalised Bchi automata</H2>
<TABLE>
<TR>
<TD><A NAME="space"><space></A> ::=</TD>
<TD><CODE>[ \n]+</CODE></TD>
</TR>
<TR>
<TD><A NAME="gba"><gba></A> ::=</TD>
<TD><CODE>[0-9]+</CODE> <<A HREF="#space">space</A>>
<CODE>[0-9]+</CODE>
<<A HREF="#states">states</A>>
</TD>
<TD><EM>/* first the number of states, then the number of acceptance sets
(if 0, all states are accepting) */</EM></TD>
</TR>
<TR>
<TD><A NAME="states"><states></A> ::=</TD>
<TD><EM>/* empty */</EM></TD>
</TR>
<TR>
<TD><states> ::=</TD>
<TD><<A HREF="#states">states</A>> <<A HREF="#space">space</A>>
<<A HREF="#state">state</A>></TD>
</TR>
<TR>
<TD><A NAME="state"><state></A> ::=</TD>
<TD><CODE>[0-9]+</CODE> <<A HREF="#space">space</A>>
<<A HREF="#initial">initial?</A>> <<A HREF="#space">space</A>>
<<A HREF="#acceptance sets">acceptance sets</A>> '-1'
<<A HREF="#transitions">transitions</A>> '-1'</TD>
<TD><EM>/* state identifiers can be arbitrary unsigned integers */</EM></TD>
</TR>
<TR>
<TD><A NAME="initial"><initial?></A> ::=</TD>
<TD><CODE>'0'</CODE></TD>
<TD><EM>/* not an initial state */</EM></TD>
</TR>
<TR>
<TD><initial?> ::=</TD>
<TD><CODE>'1'</CODE></TD>
<TD><EM>/* initial state (exactly one state must be initial) */</EM></TD>
</TR>
<TR>
<TD><A NAME="acceptance sets"><acceptance sets></A> ::=</TD>
<TD><EM>/* empty */</EM></TD>
</TR>
<TR>
<TD><acceptance sets> ::=</TD>
<TD><<A HREF="#acceptance sets">acceptance sets</A>>
<CODE>[0-9]+</CODE> <<A HREF="#space">space</A>></TD>
<TD><EM>/* acceptance set identifiers can be arbitrary unsigned integers */</EM></TD>
</TR>
<TR>
<TD><A NAME="transitions"><transitions></A> ::=</TD>
<TD><EM>/* empty */</EM></TD>
</TR>
<TR>
<TD><transitions> ::=</TD>
<TD><<A HREF="#transitions">transitions</A>>
<<A HREF="#space">space</A>>
<<A HREF="#transition">transition</A>></TD>
</TR>
<TR>
<TD><A NAME="transition"><transition></A> ::=</TD>
<TD><CODE>[0-9]+</CODE> <<A HREF="#space">space</A>>
<CODE>'t'</CODE></TD>
<TD><EM>/* constantly enabled transition to
a <A HREF="#state">state</A> */</EM></TD>
</TR>
<TR>
<TD><A NAME="transition"><transition></A> ::=</TD>
<TD><CODE>[0-9]+</CODE> <<A HREF="#space">space</A>>
<<A HREF="#gate">gate</A>></TD>
<TD><EM>/* conditionally enabled transition to
a <A HREF="#state">state</A> */</EM></TD>
</TR>
<TR>
<TD><A NAME="gate"><gate></A> ::=</TD>
<TD><CODE>'p'[0-9]+</CODE></TD>
<TD><EM>/* proposition */</EM></TD>
</TR>
<TR>
<TD><gate> ::=</TD>
<TD><CODE>'!'</CODE> <<A HREF="#space">space</A>>
<<A HREF="#gate">gate</A>></TD>
<TD><EM>/* negation */</EM></TD>
</TR>
<TR>
<TD><gate> ::=</TD>
<TD><CODE>'|'</CODE> <<A HREF="#space">space</A>>
<<A HREF="#gate">gate</A>> <<A HREF="#space">space</A>>
<<A HREF="#gate">gate</A>></TD>
<TD><EM>/* disjunction */</EM></TD>
</TR>
<TR>
<TD><gate> ::=</TD>
<TD><CODE>'&'</CODE> <<A HREF="#space">space</A>>
<<A HREF="#gate">gate</A>> <<A HREF="#space">space</A>>
<<A HREF="#gate">gate</A>></TD>
<TD><EM>/* conjunction */</EM></TD>
</TR>
</TABLE>
<P>Note that currently LBT does not generate disjunctions on gate
conditions. Also, the initial state is always numbered 0.</P>
<H2>Visualising the Output</H2>
<P>A simple tool, lbt2dot, converts the generalised Bchi automata
descriptions output by the translator to a format viewable with <A
HREF="http://www.graphviz.org/">GraphViz</A>, a visualisation tool for
directed graphs. Gate expressions are presented as edge labels, and
state and acceptance set identifiers are presented as node labels.
The node corresponding to the initial state is shaded.</P>
<P>Here is a sample run involving the filter: <CODE>echo '! G p0' |
lbt | lbt2dot | dotty -</CODE>.<BR>
<IMG SRC="notgp0.png" ALT="[Generalised Bchi Automaton of ! G p0]"><BR>
In the picture above, constructed with the command <CODE>echo '! G p0'
| lbt | lbt2dot | dot -Tpng -Grankdir=LR -Nfontname=Verdana
-Efontname=Verdana > notgp0.png</CODE>, the automaton has 4 states,
identified by the numbers 0, 2, 3, and 4. The initial state is 0, and
there is one acceptance set, identified by the number 0. All states
except states 0 and 4 belong to this acceptance set.</P>
<P>The above example illustrates that the translation generates
unnecessary states. The algoritm never generates loops to the initial
state. Clearly, this automaton could be reduced to two states with
<CODE>t</CODE>-labeled self-loops:<BR>
<IMG SRC="notgp0-opt.png" ALT="[Optimised Generalised Bchi Automaton of ! G p0]"></P>
<H1>Obtaining the Code</H1>
<P>You can download the code from <A
HREF="http://www.tcs.hut.fi/maria/src/">http://www.tcs.hut.fi/maria/src/</A>.
You will need C and C++ compilers such as <A
HREF="http://gcc.gnu.org/">GCC</A> for compiling the source code.</P>
<P>For the convenience of Windows users, we provide executable files
that were compiled with gcc-2.95.2 configured as a cross-compiler for
the <A HREF="http://www.mingw.org/">mingw</A> target platform.</P>
</BODY></HTML>
|
