hierarchy.org 27.7 KB
Newer Older
1
2
3
4
5
6
7
# -*- coding: utf-8 -*-
#+TITLE: Exploring the temporal hierarchy of Manna & Pnueli
#+DESCRIPTION: Spot command-line tools for exploring the temporal hierarchy of Manna & Pnueli
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html

/A hierarchy of temporal properties/ was defined by Manna & Pnueli in
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
8
their [[ftp://www-cs.stanford.edu/cs/theory/amir/hierarchy.ps][PODC'90 paper]].
9
10
11
12
13
14
15
16
17

This hierarchy relates "properties" (i.e., omega-regular languages) to
structural properties of the automata that can recognize them.

* Description of the classes

The hierarchy is built from the classes pictured in the following
diagram, where each class includes everything below it. For instance,
the /recurrence/ class includes the /obligation/ class which also
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
18
19
includes the /safety/ and /guarantee/ classes, as well as the unnamed
intersection of /safety/ and /guarantee/ (=B= in the picture).
20

21
[[file:hierarchy.svg]]
22
23
24
25

Forget about the LTL properties and about the red letters displayed in
this picture for a moment.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
26
27
28
- The /reactivity/ class represents all possible omega-regular
  languages, i.e., all languages that can be recognized by a
  non-deterministic Büchi automaton.
29

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
30
31
- The /recurrence/ subclass contains all properties that can be
  recognized by a deterministic Büchi automaton.
32

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
33
- The dual class, /persistence/ properties, are those that can be
Maximilien Colange's avatar
Typos    
Maximilien Colange committed
34
  recognized by a weak Büchi automaton (i.e., in each SCC either all
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
35
  states are accepting, or all states are rejecting).
36

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
37
38
39
- The intersection of /recurrence/ and /persistence/ classes form the
  /obligation/ properties: any of those can be recognized by a weak
  and deterministic Büchi automaton.
40

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
41
42
43
- /Guarantee/ properties are a subclass of /obligation/ properties
  that can be recognized by terminal Büchi automata (i.e., upon
  reaching an accepting state, any suffix will be accepted).
44

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
45
- /Safety/ properties are the dual of /Guarantee/ properties: they can
Maximilien Colange's avatar
Typos    
Maximilien Colange committed
46
  be recognized by ω-automata that accept all their runs (i.e., the
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
47
  acceptance condition is "true").  Note that since these automata are
Maximilien Colange's avatar
Typos    
Maximilien Colange committed
48
  not necessary complete, it is still possible for some words not to
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
49
50
51
52
  be accepted.  If we interpret the ω-automata with "true" acceptance
  as finite automata with all states marked as final, we obtain
  monitors, i.e., finite automata that recognize all finite prefixes
  that can be extended into valid ω-words.
53

Maximilien Colange's avatar
Typos    
Maximilien Colange committed
54
- Finally, at the very bottom is an unnamed class that contains
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
55
56
57
  /Safety/ properties that are also /Guarantee/ properties: those are
  properties that can be represented by monitors in which the only
  cycles are self-loops labeled by true.
58
59
60

The "LTL normal forms" displayed in the above figure help to visualize
the type of LTL formulas contained in each of these class.  But note
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
61
that (1) this hierarchy applies to all omega-regular properties, not
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
just LTL-defined properties, and (2) the LTL expression displayed in
the figure are actually normal forms in the sense that if an
LTL-defined property belongs to the given class, then there exists an
equivalent LTL property under the stated form, were $p$, $q$, $p_i$
and $q_i$ are subexpressions that may use only Boolean operators, the
next operator ($\mathsf{X}$), and past-LTL operators (which are not
supported by Spot).  The combination of these allowed operators only
makes it possible to express constraints on finite prefixes.

/Obligations/ can be thought of as Boolean combinations of /safety/
and /guarentee/ properties, while /reactivity/ properties are Boolean
combinations of /recurrence/ and /persistence/ properties.  The
negation of a /safety/ property is a /guarantee/ property (and
vice-versa), and the same duality hold for /persistence/ and
/recurrence/ properties.

The red letters in each of these seven classes are keys used in
Spot to denote the classes.

* Deciding class membership

The =--format=%h= option can be used to display the "class key" of the
most precise class to which a formula belongs.

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -f 'a U b' --format=%h
#+END_SRC
#+RESULTS:
: G

If you find hard to remember the class name corresponding to the class
keys, you can request verbose output with =%[v]h=:

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -f 'a U b' --format='%[v]h'
#+END_SRC
#+RESULTS:
: guarantee

But actually any /guarantee/ property is also an /obligation/, a
/recurrence/, a /persistence/, and a /reactivity/ property.  You can
get the complete list of classes using =%[w]h= or =%[vw]h=:

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -f 'a U b' --format='%[w]h = %[vw]h'
#+END_SRC
#+RESULTS:
: GOPRT = guarantee obligation persistence recurrence reactivity

This =--format= option is also supported by =randltl=, =genltl=, and
=ltlgrind=.  So for instance if you want to classify the 55 LTL
patterns of [[http://patterns.projects.cs.ksu.edu/documentation/patterns/ltl.shtml][Dwyers et al. (FMSP'98)]] using this hierarchy, try:

#+BEGIN_SRC sh :results verbatim :exports both
genltl --dac-patterns --format='%[v]h' | sort | uniq -c
#+END_SRC

#+RESULTS:
:       1 guarantee
:       2 obligation
:       1 persistence
:       2 reactivity
:      12 recurrence
:      37 safety

Maximilien Colange's avatar
Typos    
Maximilien Colange committed
127
In this output, the most precise class is given for each formula, and
128
the count of formulas for each subclass is given.  We have to remember
Maximilien Colange's avatar
Typos    
Maximilien Colange committed
129
that the recurrence class also includes obligation, safety, and
130
131
132
133
134
135
136
137
138
guarantee properties.  In this list, there are no formulas that belong
to the intersection of the /guarantee/ and /safety/ classes (it would
have been listed as =guarantee safety=).

From this list, only 3 formulas are not recurrence properties (i.e.,
not recognized by deterministic Büchi automata): one of them is a
persistence formula, the other two cannot be classified better than in
the /reactivity/ class.  Let's pretend we are interested in those
three non-recurrence formulas, we can use =ltlfilt -v --recurrence= to
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
139
140
remove all recurrence properties from the =genltl --dac-pattern=
output:
141
142
143
144
145
146
147
148
149
150
151
152

#+BEGIN_SRC sh :results verbatim :exports both
genltl --dac-patterns |
  ltlfilt -v --recurrence --format='%[v]h, %f'
#+END_SRC

#+RESULTS:
: persistence, G!p0 | F(p0 & (!p1 W p2))
: reactivity, G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & X(!p2 U p4)))) U (p2 | G(p1 -> (p3 & XFp4)))))
: reactivity, G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & !p4 & X((!p2 & !p4) U p5)))) U (p2 | G(p1 -> (p3 & !p4 & X(!p4 U p5))))))

Similar filtering options exist for other classes.  Since these tests
Maximilien Colange's avatar
Typos    
Maximilien Colange committed
153
are automata-based, they work with PSL formulas as well. For instance,
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
here is how to generate 10 random recurrence PSL formulas that are
not LTL formulas, and that are not obligations:

#+BEGIN_SRC sh :results verbatim :exports both
randltl --psl -n -1 a b |
   ltlfilt -v --ltl |
   ltlfilt -v --obligation |
   ltlfilt --recurrence -n10
#+END_SRC
#+RESULTS:
#+begin_example
((Fb W 0) | (1 U !a)) W ({b[*]}[]-> 0)
GF({[*]}<>-> !a)
{[*]}[]-> X(b M F!Gb)
G!({a[*2]}<>-> (b & F(0 R a)))
FX({[*]} -> GFb)
G({b[*][:*1]} xor (Fb U Fa)) W b
(b R a) & (({1 | [*0]} -> (1 U a)) W 0)
G({[*]}[]-> Fa)
{[*]}[]-> F(1 U b)
0 R !({!a | a[*]}[]-> GXa)
#+end_example

Note that the order of the =ltlfilt= filters could be changed provided
the =-n10= stays at the end.  For instance we could first keep all
recurrence before removing obligations and then removing LTL formulas.
The order given above actually starts with the easier checks first and
keep the most complex tests at the end of the pipeline so they are
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
182
183
184
185
186
187
188
189
applied to fewer formulas.  Testing whether a formula is an LTL
formula is very cheap, testing if a formula is an obligation is harder
(it may involves a translation to automata and a poweset
construction), and testing whether a formula is a recurrence is the
most costly procedure (it involves a translation as well, plus
conversion to deterministic Rabin automata, and an attempt to convert
the automaton back to deterministic Büchi).  As a rule of thumb,
testing classes that are lower in the hierarchy is cheaper.
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

Since option =-o= (for specifying output file) also honors =%=-escape
sequences, we can use it with =%h= to split a list of formulas in 7
possible files.  Here is a generation of 200 random LTL formulas
binned into aptly named files:

#+BEGIN_SRC sh :results verbatim :exports both
randltl -n 200 a b -o random-%h.ltl
wc -l random-?.ltl
#+END_SRC

#+RESULTS:
:   40 random-B.ltl
:   49 random-G.ltl
:   12 random-O.ltl
:   21 random-P.ltl
:   18 random-R.ltl
:   51 random-S.ltl
:    9 random-T.ltl
:  200 total

#+BEGIN_SRC sh :results silent :exports results
rm -f random-?.ltl
#+END_SRC
#+RESULTS:

* Deciding classes membership syntactically

LTL formulas can also be classified into related classes which we
shall call /syntactic-safety/, /syntactic-guarantee/, etc.  See [[https://spot.lrde.epita.fr/tl.pdf][tl.pdf]]
for the grammar of each syntactic class.  Any LTL-definable property
of class C can be defined by an LTL formulas in class syntactic-C, but
an LTL formula can describe a property of class C even if that formula
is not in class syntactic-C (we just know that some equivalent formula
is in class syntactic-C).

=ltlfilt= has options like =--syntactic-guarantee=,
=--syntactic-persistence=, etc. to match formulas from this classes.

Maximilien Colange's avatar
Typos    
Maximilien Colange committed
229
Here is how to generate 10 random LTL formulas that describe safety
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
properties but that are not in the syntactic-safety class:

#+BEGIN_SRC sh :results verbatim :exports both
randltl -n-1 a b |
  ltlfilt -v --syntactic-safety |
  ltlfilt --safety -n10
#+END_SRC

#+RESULTS:
#+begin_example
F!(!b <-> FGb)
!Fb xor G((b xor (Xa M b)) U b)
a W F(a -> b)
((0 R Xa) R a) -> Fa
X(Xb & (!Ga R Ga))
(1 U b) | F(Fb W (a <-> FXa))
(a M 1) | (!a W a)
(G!a W ((b M 1) -> Fa)) -> !a
!a -> ((a xor !GFa) W 0)
b M Gb
#+end_example

Since all those formulas describe safety properties, an exercise would
Maximilien Colange's avatar
Typos    
Maximilien Colange committed
253
be to suggest equivalent formulas that are in the syntactic-safety
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
fragment.  For instance =b M Gb= can be rewritten as just =Gb=, which
belongs to this fragment.  In this particular case, =ltlfilt
--simplify= recognizes this:

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt --simplify -f 'b M Gb'
#+END_SRC
#+RESULTS:
: Gb

However in the general case Spot is not able to provide the equivalent
formula from the appropriate syntactic class.

* What to do with each class?

** Obligation

Spot implements algorithms from Löding ([[http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.6718][/Efficient minimization of
deterministic weak ω-automata/, IPL 2001]]) and Dax et al. ([[http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.2081][/Mechanizing
the powerset constructions for restricted classes of ω-automata/,
ATVA'07]]) in order to detect obligation properties, and produce minimal
weak deterministic automata for them.

Maximilien Colange's avatar
Typos    
Maximilien Colange committed
277
When running =ltl2tgba -D= on a formula that represents an
278
279
280
281
obligation property, you are guaranteed to obtain a minimal (in the
number of states) deterministic weak Büchi automaton that recognizes
it.  Note that since the /obligation/ class includes the /safety/ and
/guarantee/ classes, minimal deterministic automata will also be
Maximilien Colange's avatar
Typos    
Maximilien Colange committed
282
produced for those classes.  Dax et al.'s determinization of obligation
283
properties combined with Löding's minimization renders obsolete
Maximilien Colange's avatar
Typos    
Maximilien Colange committed
284
older algorithms (and tools) that produced minimal deterministic
285
286
automata but only for the subclasses of /safety/ or /guarantee/.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
287
288
289
290
If =ltl2tgba= is run without =-D= (but still with the default =--high=
optimization level), the minimal weak deterministic automaton will
only be output if it is smaller than the non-deterministic automaton
the translator could produce before determinization and minimization.
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309

For instance =Fa R b= is an obligation:

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -f 'Fa R b' --format='%[v]h'
#+END_SRC

#+RESULTS:
: obligation

If we translate it without =-D= we get a 3-state non-deterministic
automaton (here we use =autfilt --highlight-nondet= to show where the
non-determinism occurs):

#+NAME: hier-oblig-1
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba 'Fa R b' | autfilt --highlight-nondet -d
#+END_SRC

310
#+BEGIN_SRC dot :file hier-oblig-1.svg :var txt=hier-oblig-1 :exports results
311
312
313
314
$txt
#+END_SRC

#+RESULTS:
315
[[file:hier-oblig-1.svg]]
316
317
318
319
320
321
322
323
324
325
326

Note that the above automaton uses transition-based acceptance, but
since it is an obligation, using transition-based acceptance will not
improve anything, so we might as well require a Büchi automaton with
=-B= or just state-based acceptance with =-S=:

#+NAME: hier-oblig-1b
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba -B 'Fa R b' | autfilt --highlight-nondet -d
#+END_SRC

327
#+BEGIN_SRC dot :file hier-oblig-1b.svg :var txt=hier-oblig-1b :exports results
328
329
330
331
$txt
#+END_SRC

#+RESULTS:
332
[[file:hier-oblig-1b.svg]]
333
334
335
336
337
338
339
340
341
342


With =ltl2tgba -D= we get a (minimal) deterministic weak Büchi
automaton instead.

#+NAME: hier-oblig-2
#+BEGIN_SRC sh :results verbatim :exports code
  ltl2tgba -D 'Fa R b' -d
#+END_SRC

343
#+BEGIN_SRC dot :file hier-oblig-2.svg :var txt=hier-oblig-2 :exports results
344
345
346
347
$txt
#+END_SRC

#+RESULTS:
348
[[file:hier-oblig-2.svg]]
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364


When we called =ltl2tgba=, without the option =-D=, the two automata
(non-deterministic and deterministic) were constructed, but the
deterministic one was discarded because it was bigger.  Using =-D=
forces the deterministic automaton to be used regardless of its size.

The detection and minimization of obligation properties is also used
by =autfilt= when simplifying deterministic automata (they need to be
deterministic so that =autfilt= can easily compute their complement).

For instance, let us use =ltl2dstar= to construct a Streett automaton
for the obligation property =a <-> GXa=:

#+NAME: hier-oblig-3
#+BEGIN_SRC sh :results verbatim :exports code
365
ltldo 'ltl2dstar --automata=streett' -f 'a <-> GXa' -d
366
#+END_SRC
367
#+BEGIN_SRC dot :file hier-oblig-3.svg :var txt=hier-oblig-3 :exports results
368
369
370
371
$txt
#+END_SRC

#+RESULTS:
372
[[file:hier-oblig-3.svg]]
373
374
375
376
377
378
379

We can now minimize this automaton with:

#+NAME: hier-oblig-4
#+BEGIN_SRC sh :results verbatim :exports code
ltldo 'ltl2dstar --automata=streett' -f 'a <-> GXa' | autfilt -D -C -d
#+END_SRC
380
#+BEGIN_SRC dot :file hier-oblig-4.svg :var txt=hier-oblig-4 :exports results
381
382
383
$txt
#+END_SRC
#+RESULTS:
384
[[file:hier-oblig-4.svg]]
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413

Here we have used option =-C= to keep the automaton complete, so that
the comparison with =ltl2dstar= is fair, since =ltl2dstar= always
output complete automata.

** Guarantee

/Guarantee/ properties can be translated into terminal automata.
There is nothing particular in Spot about /guarantee/ properties, they
are all handled like /obligations/.

Again, using =-D= will always produce (minimal) deterministic Büchi
automata, even if they are larger than the non-deterministic version.
The output should be a terminal automaton in either case,

An example is =a U Xb=:

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -f 'a U Xb' --format='%[v]h'
#+END_SRC

#+RESULTS:
: guarantee


#+NAME: hier-guarantee-1
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba 'a U Xb' | autfilt --highlight-nondet -d
#+END_SRC
414
#+BEGIN_SRC dot :file hier-guarantee-1.svg :var txt=hier-guarantee-1 :exports results
415
416
417
418
$txt
#+END_SRC

#+RESULTS:
419
[[file:hier-guarantee-1.svg]]
420
421
422
423
424

#+NAME: hier-guarantee-2
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba -D 'a U Xb' -d
#+END_SRC
425
#+BEGIN_SRC dot :file hier-guarantee-2.svg :var txt=hier-guarantee-2 :exports results
426
427
428
429
$txt
#+END_SRC

#+RESULTS:
430
[[file:hier-guarantee-2.svg]]
431
432

** Safety
433
434
435
   :PROPERTIES:
   :CUSTOM_ID: safety
   :END:
436
437
438
439
440
441
442

/Safety/ properties also form a subclass of /obligation/ properties,
and again there is no code specific to them in the translation.
However, the /safety/ class corresponds to what can be represented
faithfully by monitors, i.e., automata that accept all their infinite
runs.

Maximilien Colange's avatar
Typos    
Maximilien Colange committed
443
For most safety formulas, the acceptance output by =ltl2tgba= will
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
already be =t= (meaning that all runs are accepting).  However since
the translator does not do anything particular about safety formulas,
it is possible to find some pathological formulas for which the
translator outputs a non-deterministic Büchi automaton where not all
run are accepting.

Here is an example:

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -f '(a W Gb) M b' --format='%[v]h'
#+END_SRC

#+RESULTS:
: safety


#+NAME: hier-safety-1
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba '(a W Gb) M b' | autfilt --highlight-nondet -d
#+END_SRC
464
#+BEGIN_SRC dot :file hier-safety-1.svg :var txt=hier-safety-1 :exports results
465
466
467
468
$txt
#+END_SRC

#+RESULTS:
469
[[file:hier-safety-1.svg]]
470
471
472
473
474

Actually, marking all states of this automaton as accepting would not
be wrong, the translator simply does not know it.

Using =-D= will fix that: it then produces a deterministic automaton
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
475
that is guaranteed to be minimal, and where all runs are accepting.
476
477
478
479
480

#+NAME: hier-safety-2
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba -D '(a W Gb) M b' -d
#+END_SRC
481
#+BEGIN_SRC dot :file hier-safety-2.svg :var txt=hier-safety-2 :exports results
482
483
484
485
$txt
#+END_SRC

#+RESULTS:
486
[[file:hier-safety-2.svg]]
487
488


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
489
490
491
492
If you are working with safety formula, and know you want to work with
monitors, you can use the =-M= option of =ltl2tgba=.  In this case
this will output the same automaton, but using the universal
acceptance (i.e. =t=).  You can interpret this output as a monitor
Maximilien Colange's avatar
Typos    
Maximilien Colange committed
493
(i.e., a finite automaton that accepts all prefixes that can be
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
494
extended into valid ω-words).
495
496
497
498
499

#+NAME: hier-safety-1m
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba -M '(a W Gb) M b' | autfilt --highlight-nondet -d
#+END_SRC
500
#+BEGIN_SRC dot :file hier-safety-1m.svg :var txt=hier-safety-1m :exports results
501
502
503
504
  $txt
#+END_SRC

#+RESULTS:
505
[[file:hier-safety-1m.svg]]
506
507
508
509
510

#+NAME: hier-safety-2m
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba -M -D '(a W Gb) M b' -d
#+END_SRC
511
#+BEGIN_SRC dot :file hier-safety-2m.svg :var txt=hier-safety-2m :exports results
512
513
514
515
$txt
#+END_SRC

#+RESULTS:
516
[[file:hier-safety-2m.svg]]
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531


Note that the =-M= option can be used with formulas that are not
safety properties.  In this case, the output monitor will recognize a
language larger than that of the property.

** Recurrence

/Recurrence/ properties can be represented by deterministic Büchi
automata.

For the subclass of /obligation/ properties, using =-D= is a sure way
to obain a deterministic automaton (and even a minimal one), but for
the /recurrence/ properties that are not /obligations/ the translator
does not make any special effort to produce deterministic automata,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
532
even with =-D= (this might change in the future).
533

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
534
535
536
537
All properties that are not in the /persistence/ class (this includes
the /recurrence/ properties that are not /obligations/) can benefit
from transition-based acceptance.  In other words using
transition-based acceptance will often produce shorter automata.
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552

The typical example is =GFa=, which can be translated into a 1-state
transition-based Büchi automaton:

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -f 'GFa' --format='%[v]h'
#+END_SRC

#+RESULTS:
: recurrence

#+NAME: hier-recurrence-1
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba 'GFa' -d
#+END_SRC
553
#+BEGIN_SRC dot :file hier-recurrence-1.svg :var txt=hier-recurrence-1 :exports results
554
555
556
557
$txt
#+END_SRC

#+RESULTS:
558
[[file:hier-recurrence-1.svg]]
559
560
561
562
563
564
565

Using state-based acceptance, at least two states are required.  For instance:

#+NAME: hier-recurrence-2
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba -S 'GFa' -d
#+END_SRC
566
#+BEGIN_SRC dot :file hier-recurrence-2.svg :var txt=hier-recurrence-2 :exports results
567
568
569
570
$txt
#+END_SRC

#+RESULTS:
571
[[file:hier-recurrence-2.svg]]
572
573


Maximilien Colange's avatar
Typos    
Maximilien Colange committed
574
Here is an example of a formula for which =ltl2tgba= does not produce a
575
576
577
578
579
580
581
582
583
584
585
586
587
deterministic automaton, even with =-D=.

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -f 'G(Gb | Fa)' --format='%[v]h'
#+END_SRC

#+RESULTS:
: recurrence

#+NAME: hier-recurrence-3
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba -D 'G(Gb | Fa)' | autfilt --highlight-nondet -d
#+END_SRC
588
#+BEGIN_SRC dot :file hier-recurrence-3.svg :var txt=hier-recurrence-3 :exports results
589
590
591
592
$txt
#+END_SRC

#+RESULTS:
593
[[file:hier-recurrence-3.svg]]
594
595
596
597

One way to obtain a deterministic Büchi automaton (it has to exist, since this is
a /recurrence/ property), is to chain a few algorithms implemented in Spot:

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
598
 1. Determinize the non-deterministic automaton to obtain a
599
600
601
602
603
604
    deterministic automaton with parity acceptance: this is done by
    using =ltl2tgba -G -D=, with option =-G= indicating that any
    acceptance condition may be used.

    #+NAME: hier-recurrence-4
    #+BEGIN_SRC sh :results verbatim :exports code
605
    ltl2tgba -G -D 'G(Gb | Fa)' -d
606
    #+END_SRC
607
    #+BEGIN_SRC dot :file hier-recurrence-4.svg :var txt=hier-recurrence-4 :exports results
608
609
610
    $txt
    #+END_SRC
    #+RESULTS:
611
    [[file:hier-recurrence-4.svg]]
612

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
613
 2. Transform the parity acceptance into Rabin acceptance: this is
614
615
616
617
618
619
620
    done with =autfilt --generalized-rabin=.  Because of the type of
    parity acceptance used, the result will actually be Rabin and not
    generalized Rabin.

    #+NAME: hier-recurrence-5
    #+BEGIN_SRC sh :results verbatim :exports code
    ltl2tgba -G -D 'G(Gb | Fa)' |
621
      autfilt --generalized-rabin -d
622
    #+END_SRC
623
    #+BEGIN_SRC dot :file hier-recurrence-5.svg :var txt=hier-recurrence-5 :exports results
624
625
626
627
    $txt
    #+END_SRC

    #+RESULTS:
628
    [[file:hier-recurrence-5.svg]]
629
630
631

    (The only change here is in the acceptance condition.)

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
632
 3. In step 4 we are going to convert the automaton to state-based
Maximilien Colange's avatar
Typos    
Maximilien Colange committed
633
634
    Büchi, and this sometimes works better if the input Rabin automaton
    also uses state-based acceptance.  So let us add =-S= to the
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
635
    previous command:
636
637
638
639

    #+NAME: hier-recurrence-6
    #+BEGIN_SRC sh :results verbatim :exports code
    ltl2tgba -G -D 'G(Gb | Fa)' |
640
      autfilt -S --generalized-rabin -d
641
    #+END_SRC
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
642

643
    #+BEGIN_SRC dot :file hier-recurrence-6.svg :var txt=hier-recurrence-6 :exports results
644
645
646
647
    $txt
    #+END_SRC

    #+RESULTS:
648
    [[file:hier-recurrence-6.svg]]
649

650
 4. Finally, convert the resulting automaton to BA, using =autfilt
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
651
652
653
654
655
656
657
658
    -B=.  Spot can convert automata with any acceptance condition to
    BA, but when the input is a deterministic Rabin automaton, it uses
    a dedicated algorithm that preserves determinism whenever possible
    (and we know it is possible, because we are working on a
    recurrence formula).  Adding =-D= here to suggest that we are
    trying to obtain a deterministic automaton does not hurt, as it
    will enable simplifications as a side-effect (without =-D= we
    simply get a larger deterministic automaton).
659
660
661
662
663

    #+NAME: hier-recurrence-7
    #+BEGIN_SRC sh :results verbatim :exports code
    ltl2tgba -G -D 'G(Gb | Fa)' |
      autfilt -S --generalized-rabin |
664
      autfilt -B -D -d
665
    #+END_SRC
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
666

667
    #+BEGIN_SRC dot :file hier-recurrence-7.svg :var txt=hier-recurrence-7 :exports results
668
669
670
671
    $txt
    #+END_SRC

    #+RESULTS:
672
    [[file:hier-recurrence-7.svg]]
673
674

Here we are lucky that the deterministic Büchi automaton is even
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
675
676
677
678
679
680
681
682
smaller than the original non-deterministic version.  As said earlier,
passing =-S= to the first =autfilt= was optional, but in this case it
helps producing a smaller automaton.  Here is what we get without it:

#+NAME: hier-recurrence-8
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba -G -D 'G(Gb | Fa)' |
  autfilt --generalized-rabin |
683
  autfilt -B -D -d
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
684
685
#+END_SRC

686
#+BEGIN_SRC dot :file hier-recurrence-8.svg :var txt=hier-recurrence-8 :exports results
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
687
688
689
690
$txt
#+END_SRC

#+RESULTS:
691
[[file:hier-recurrence-8.svg]]
692
693

It is likely that =ltl2tgba= will implement all this processing chain
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
694
in the future.
695
696
697
698
699
700
701
702
703

** Persistence

Since /persistence/ properties are outside of the /recurrence/ class,
they cannot be represented by deterministic Büchi automata.  The typical
persistence formula is =FGa=, and using =-D= on this is hopeless.

#+NAME: hier-persistence-1
#+BEGIN_SRC sh :results verbatim :exports code
704
ltl2tgba -D FGa -d
705
#+END_SRC
706
#+BEGIN_SRC dot :file hier-persistence-1.svg :var txt=hier-persistence-1 :exports results
707
708
709
710
$txt
#+END_SRC

#+RESULTS:
711
[[file:hier-persistence-1.svg]]
712
713
714
715
716
717
718
719
720
721
722
723


However since the *negation* of =FGa= is a /recurrence/, this negation
can be represented by a deterministic Büchi automaton, which means
that =FGa= could be represented by a deterministic co-Büchi automaton.
=ltl2tgba= does not generate co-Büchi acceptance, but we can do the
complementation ourselves:

#+NAME: hier-persistence-2
#+BEGIN_SRC sh :results verbatim :exports code
ltlfilt --negate -f FGa |
  ltl2tgba -D |
724
  autfilt --complement -d
725
#+END_SRC
726
#+BEGIN_SRC dot :file hier-persistence-2.svg :var txt=hier-persistence-2 :exports results
727
728
729
730
$txt
#+END_SRC

#+RESULTS:
731
[[file:hier-persistence-2.svg]]
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767

Note that in this example, we know that =GFa= is trivial enough that
=ltl2tgba -D GFa= will generate a deterministic automaton.  In the
general case we might have to determinize the automaton as we did in
the previous section (we will do it again below).

/Persistence/ properties can be represented by weak Büchi automata.  The
translator is aware of that, so when it detects that the input formula
is a syntactic-persistence, it simplifies its translation slightly to
ensure that the output will use at most one acceptance set.  (It is
possible to define a persistence properties using an LTL formula that
is not a syntactic-persistance, this optimization is simply not
applied.)

If the input is a weak property that is not syntactically weak, the
output will not necessarily be weak.  One costly way to obtain a weak
automaton for a formula $\varphi$ would be to first compute a
deterministic Büchi automaton of the recurrence $\lnot\varphi$ then
complement the acceptance of the resulting automaton, yielding a
deterministic co-Büchi automaton, and then transform that into a Büchi
automaton.

Let's do that on the persistence formula =F(G!a | G(b U a))=

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -f 'F(G!a | G(b U a))' --format='%[v]h'
#+END_SRC
#+RESULTS:
: persistence

Unfortunately the default output of the translation is not weak:

#+NAME: hier-persistence-3
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba 'F(G!a | G(b U a))' -d
#+END_SRC
768
#+BEGIN_SRC dot :file hier-persistence-3.svg :var txt=hier-persistence-3 :exports results
769
770
771
772
$txt
#+END_SRC

#+RESULTS:
773
[[file:hier-persistence-3.svg]]
774
775
776
777
778
779
780
781
782

Furthermore it appears that =ltl2tgba= does generate a deterministic
Büchi automaton for the complement, instead we get a non-deterministic
generalized Büchi automaton:

#+NAME: hier-persistence-4
#+BEGIN_SRC sh :results verbatim :exports code
ltlfilt --negate -f 'F(G!a | G(b U a))' |
  ltl2tgba -D |
783
  autfilt --highlight-nondet=5 -d
784
#+END_SRC
785
#+BEGIN_SRC dot :file hier-persistence-4.svg :var txt=hier-persistence-4 :exports results
786
787
788
789
$txt
#+END_SRC

#+RESULTS:
790
[[file:hier-persistence-4.svg]]
791

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
792
793
So let us use the same tricks as in the previous section,
determinizing this automaton into a Rabin automaton, and then back to
794
795
796
797
798
799
deterministic Büchi:

#+NAME: hier-persistence-5
#+BEGIN_SRC sh :results verbatim :exports code
ltlfilt --negate -f 'F(G!a | G(b U a))' |
  ltl2tgba -G -D |
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
800
  autfilt --generalized-rabin |
801
  autfilt --tgba -D -d
802
#+END_SRC
803
#+BEGIN_SRC dot :file hier-persistence-5.svg :var txt=hier-persistence-5 :exports results
804
805
806
807
$txt
#+END_SRC

#+RESULTS:
808
[[file:hier-persistence-5.svg]]
809
810
811
812
813
814
815
816

This is a deterministic Büchi automaton for the negation of our formula.
Now we can complement it to obtain a deterministic co-Büchi automaton for =F(G!a | G(b U a))=:

#+NAME: hier-persistence-6
#+BEGIN_SRC sh :results verbatim :exports code
ltlfilt --negate -f 'F(G!a | G(b U a))' |
  ltl2tgba -G -D |
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
817
  autfilt --generalized-rabin |
818
  autfilt --tgba -D |
819
  autfilt --complement -d
820
#+END_SRC
821

822
#+BEGIN_SRC dot :file hier-persistence-6.svg :var txt=hier-persistence-6 :exports results
823
824
825
826
$txt
#+END_SRC

#+RESULTS:
827
[[file:hier-persistence-6.svg]]
828
829
830
831
832
833
834

And finally we convert the result back to Büchi:

#+NAME: hier-persistence-7
#+BEGIN_SRC sh :results verbatim :exports code
ltlfilt --negate -f 'F(G!a | G(b U a))' |
  ltl2tgba -G -D |
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
835
  autfilt --generalized-rabin |
836
837
838
839
  autfilt --tgba -D |
  autfilt --complement -B -d
#+END_SRC

840
#+BEGIN_SRC dot :file hier-persistence-7.svg :var txt=hier-persistence-7 :exports results
841
842
843
$txt
#+END_SRC
#+RESULTS:
844
[[file:hier-persistence-7.svg]]
845
846

That is indeed, a weak automaton.