8754cea2ca
* doc/org/hierarchy.org, doc/org/hierarchy.tex: New files. * doc/Makefile.am, doc/org/tools.org, NEWS: Add them.
818 lines
27 KiB
Org Mode
818 lines
27 KiB
Org Mode
# -*- 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
|
|
a [[ftp://www-cs.stanford.edu/cs/theory/amir/hierarchy.ps][PODC'90 paper]].
|
|
|
|
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
|
|
includes the /safety/ and /guarantee/ classes.
|
|
|
|
[[file:hierarchy.png]]
|
|
|
|
Forget about the LTL properties and about the red letters displayed in
|
|
this picture for a moment.
|
|
|
|
The /reactivity/ class represents all possible omega-regular
|
|
languages, i.e., all languages that can be recognized by a
|
|
non-deterministic Büchi automaton.
|
|
|
|
The /recurrence/ subclass contains all properties that can be
|
|
recognized by a deterministic Büchi automaton.
|
|
|
|
The dual class, /persistence/ properties, are those that can
|
|
be reresented by a weak Büchi automaton (i.e., in each SCC either
|
|
all states are accepting, or all states are rejecting).
|
|
|
|
The intersection of /recurrence/ and /persistence/ classes form the
|
|
/obligation/ properties: those can be recognized by a weak and
|
|
deterministic Büchi automaton.
|
|
|
|
/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).
|
|
|
|
/Safety/ properties are the dual of /Guarantee/ properties: they can
|
|
be recognized by a monitor (i.e., an ω-automaton that accepts all its
|
|
runs).
|
|
|
|
Finally, at the very bottom is an unnamed class that is contains
|
|
/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.
|
|
|
|
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
|
|
that (1) this hierarchy applies to any omega-regular properties, not
|
|
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
|
|
|
|
In this output, the most precise class is given for each formula, an
|
|
the count of formulas for each subclass is given. We have to remember
|
|
that the recurrence class also include obligation, safety, and
|
|
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
|
|
select them from the =genltl --dac-pattern= output:
|
|
|
|
#+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
|
|
are automata-based, they work with PSL formulas as weil. For instance,
|
|
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
|
|
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).
|
|
|
|
|
|
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.
|
|
|
|
Here is how to generate 10 random LTL formula that describe safety
|
|
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
|
|
be suggest equivalent formulas that are in the syntactic-safety
|
|
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.
|
|
|
|
When running =ltl2tgba -D= on an formula that represents and
|
|
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
|
|
produced for those classes. Dax et al.'s determinization of obligations
|
|
properties combined with Löding's minimization renders obsolete
|
|
older algorithms (and tools) that produced minimial deterministic
|
|
automata but only for the subclasses of /safety/ or /guarantee/.
|
|
|
|
If =ltl2tgba= is run without =-D=, 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.
|
|
|
|
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
|
|
|
|
#+BEGIN_SRC dot :file hier-oblig-1.png :cmdline -Tpng :var txt=hier-oblig-1 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-oblig-1.png]]
|
|
|
|
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
|
|
|
|
#+BEGIN_SRC dot :file hier-oblig-1b.png :cmdline -Tpng :var txt=hier-oblig-1b :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-oblig-1b.png]]
|
|
|
|
|
|
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
|
|
|
|
#+BEGIN_SRC dot :file hier-oblig-2.png :cmdline -Tpng :var txt=hier-oblig-2 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-oblig-2.png]]
|
|
|
|
|
|
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
|
|
ltldo 'ltl2dstar --automata=streett' -f 'a <-> GXa' -d.a
|
|
#+END_SRC
|
|
#+BEGIN_SRC dot :file hier-oblig-3.png :cmdline -Tpng :var txt=hier-oblig-3 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-oblig-3.png]]
|
|
|
|
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
|
|
#+BEGIN_SRC dot :file hier-oblig-4.png :cmdline -Tpng :var txt=hier-oblig-4 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
[[file:hier-oblig-4.png]]
|
|
|
|
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
|
|
#+BEGIN_SRC dot :file hier-guarantee-1.png :cmdline -Tpng :var txt=hier-guarantee-1 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-guarantee-1.png]]
|
|
|
|
#+NAME: hier-guarantee-2
|
|
#+BEGIN_SRC sh :results verbatim :exports code
|
|
ltl2tgba -D 'a U Xb' -d
|
|
#+END_SRC
|
|
#+BEGIN_SRC dot :file hier-guarantee-2.png :cmdline -Tpng :var txt=hier-guarantee-2 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-guarantee-2.png]]
|
|
|
|
|
|
|
|
|
|
** Safety
|
|
|
|
/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.
|
|
|
|
For most safety formula, the acceptance output by =ltl2tgba= will
|
|
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
|
|
#+BEGIN_SRC dot :file hier-safety-1.png :cmdline -Tpng :var txt=hier-safety-1 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-safety-1.png]]
|
|
|
|
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
|
|
that is guaranteed to be minimal, and will all its runs accepting.
|
|
|
|
#+NAME: hier-safety-2
|
|
#+BEGIN_SRC sh :results verbatim :exports code
|
|
ltl2tgba -D '(a W Gb) M b' -d
|
|
#+END_SRC
|
|
#+BEGIN_SRC dot :file hier-safety-2.png :cmdline -Tpng :var txt=hier-safety-2 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-safety-2.png]]
|
|
|
|
|
|
But 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 automata, but using the universal
|
|
acceptance (i.e. =t=).
|
|
|
|
#+NAME: hier-safety-1m
|
|
#+BEGIN_SRC sh :results verbatim :exports code
|
|
ltl2tgba -M '(a W Gb) M b' | autfilt --highlight-nondet -d
|
|
#+END_SRC
|
|
#+BEGIN_SRC dot :file hier-safety-1m.png :cmdline -Tpng :var txt=hier-safety-1m :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-safety-1m.png]]
|
|
|
|
#+NAME: hier-safety-2m
|
|
#+BEGIN_SRC sh :results verbatim :exports code
|
|
ltl2tgba -M -D '(a W Gb) M b' -d
|
|
#+END_SRC
|
|
#+BEGIN_SRC dot :file hier-safety-2m.png :cmdline -Tpng :var txt=hier-safety-2m :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-safety-2m.png]]
|
|
|
|
|
|
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,
|
|
even with =-D=.
|
|
|
|
All properties that are not in the /persistence/ class (this
|
|
includes the /recurrence/ properties that are not /obligations/)
|
|
can benefit from transition-based acceptance: using transition-based
|
|
acceptance will often produce shorter automata.
|
|
|
|
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
|
|
#+BEGIN_SRC dot :file hier-recurrence-1.png :cmdline -Tpng :var txt=hier-recurrence-1 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-recurrence-1.png]]
|
|
|
|
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
|
|
#+BEGIN_SRC dot :file hier-recurrence-2.png :cmdline -Tpng :var txt=hier-recurrence-2 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-recurrence-2.png]]
|
|
|
|
|
|
Here is an example of formula for which =ltl2tgba= does not produce a
|
|
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
|
|
#+BEGIN_SRC dot :file hier-recurrence-3.png :cmdline -Tpng :var txt=hier-recurrence-3 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-recurrence-3.png]]
|
|
|
|
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:
|
|
|
|
1. determinize the non-deterministic automaton to obtain a
|
|
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
|
|
ltl2tgba -G -D 'G(Gb | Fa)' -d.a
|
|
#+END_SRC
|
|
#+BEGIN_SRC dot :file hier-recurrence-4.png :cmdline -Tpng :var txt=hier-recurrence-4 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
[[file:hier-recurrence-4.png]]
|
|
|
|
2. transform the parity acceptance into Rabin acceptance: this is
|
|
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)' |
|
|
autfilt --generalized-rabin -d.a
|
|
#+END_SRC
|
|
#+BEGIN_SRC dot :file hier-recurrence-5.png :cmdline -Tpng :var txt=hier-recurrence-5 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-recurrence-5.png]]
|
|
|
|
(The only change here is in the acceptance condition.)
|
|
|
|
3. For the next step, we actually need state-based acceptance, so
|
|
let us also add =-S= to the previous command:
|
|
|
|
#+NAME: hier-recurrence-6
|
|
#+BEGIN_SRC sh :results verbatim :exports code
|
|
ltl2tgba -G -D 'G(Gb | Fa)' |
|
|
autfilt -S --generalized-rabin -d.a
|
|
#+END_SRC
|
|
#+BEGIN_SRC dot :file hier-recurrence-6.png :cmdline -Tpng :var txt=hier-recurrence-6 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-recurrence-6.png]]
|
|
|
|
4. Finally, convert the resulting automaton to TGBA, using =autfilt
|
|
--tgba=. Spot can convert automata with any acceptance condition
|
|
to TGBA, but when the input is a deterministic state-based 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).
|
|
|
|
#+NAME: hier-recurrence-7
|
|
#+BEGIN_SRC sh :results verbatim :exports code
|
|
ltl2tgba -G -D 'G(Gb | Fa)' |
|
|
autfilt -S --generalized-rabin |
|
|
autfilt --tgba -D -d.a
|
|
#+END_SRC
|
|
#+BEGIN_SRC dot :file hier-recurrence-7.png :cmdline -Tpng :var txt=hier-recurrence-7 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-recurrence-7.png]]
|
|
|
|
Here we are lucky that the deterministic Büchi automaton is even
|
|
smaller than the original non-deterministic version.
|
|
|
|
It is likely that =ltl2tgba= will implement all this processing chain
|
|
in the future, but hopefully it will be improved first (e.g., having
|
|
to go through state-based acceptance is unfortunate).
|
|
|
|
** 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
|
|
ltl2tgba -D FGa -d.a
|
|
#+END_SRC
|
|
#+BEGIN_SRC dot :file hier-persistence-1.png :cmdline -Tpng :var txt=hier-persistence-1 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-persistence-1.png]]
|
|
|
|
|
|
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 |
|
|
autfilt --complement -d.a
|
|
#+END_SRC
|
|
#+BEGIN_SRC dot :file hier-persistence-2.png :cmdline -Tpng :var txt=hier-persistence-2 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-persistence-2.png]]
|
|
|
|
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
|
|
#+BEGIN_SRC dot :file hier-persistence-3.png :cmdline -Tpng :var txt=hier-persistence-3 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-persistence-3.png]]
|
|
|
|
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 |
|
|
autfilt --highlight-nondet=5 -d.a
|
|
#+END_SRC
|
|
#+BEGIN_SRC dot :file hier-persistence-4.png :cmdline -Tpng :var txt=hier-persistence-4 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-persistence-4.png]]
|
|
|
|
So let's use the same tricks as in the previous section, determinizing
|
|
this automaton into a state-based Rabin automaton, and then back to
|
|
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 |
|
|
autfilt -S --generalized-rabin |
|
|
autfilt --tgba -D -d.a
|
|
#+END_SRC
|
|
#+BEGIN_SRC dot :file hier-persistence-5.png :cmdline -Tpng :var txt=hier-persistence-5 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-persistence-5.png]]
|
|
|
|
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 |
|
|
autfilt -S --generalized-rabin |
|
|
autfilt --tgba -D |
|
|
autfilt --complement -d.ab
|
|
#+END_SRC
|
|
#+BEGIN_SRC dot :file hier-persistence-6.png :cmdline -Tpng :var txt=hier-persistence-6 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:hier-persistence-6.png]]
|
|
|
|
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 |
|
|
autfilt -S --generalized-rabin |
|
|
autfilt --tgba -D |
|
|
autfilt --complement -B -d
|
|
#+END_SRC
|
|
|
|
#+BEGIN_SRC dot :file hier-persistence-7.png :cmdline -Tpng :var txt=hier-persistence-7 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
[[file:hier-persistence-7.png]]
|
|
|
|
That is indeed, a weak automaton.
|