alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

org: some doc about the hierarchy

Browse source 
* doc/org/hierarchy.org, doc/org/hierarchy.tex: New files.
* doc/Makefile.am, doc/org/tools.org, NEWS: Add them.
This commit is contained in:
Alexandre Duret-Lutz 2017-01-11 22:57:49 +01:00
parent cf9ad8ebd1
commit 8754cea2ca
5 changed files with 874 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -44,11 +44,11 @@ New in spot 2.2.2.dev (Not yet released)
belonging to these two classes of the temporal hierarchy. Unlike
--syntactic-recurrence and --syntactic-persistence, the new checks
are automata-based and will also match pathological formulas.
See https://www.lrde.epita.fr/hierarchy.html
* The --format option of ltlfilt/genltl/randltl/ltlgrind learned to
print the class of a formula in the temporal hierarchy of Manna &
Pnueli using %h. Try to classify the Dwyer & al. patterns with:
genltl --dac --format='%[vw]h' | sort | uniq -c
Pnueli using %h. See https://www.lrde.epita.fr/hierarchy.html
Library:

10
doc/Makefile.am
View file

@ -1,5 +1,5 @@
## -*- coding: utf-8 -*-
## Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016 Laboratoire de
## Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016, 2017 Laboratoire de
## Recherche et Développement de l'Epita (LRDE).
## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -83,6 +83,9 @@ ORG_FILES = \
org/dstar2tgba.org \
org/genltl.org \
org/hoa.org \
org/hierarchy.org \
org/hierarchy.tex \
$(srcdir)/org/hierarchy.png \
org/index.org \
org/install.org \
org/ioltl.org \
@ -127,6 +130,11 @@ $(srcdir)/org/arch.png: org/arch.tex
pdflatex -shell-escape arch.tex && \
rm -f arch.pdf arch.aux arch.log
$(srcdir)/org/hierarchy.png: org/hierarchy.tex
cd $(srcdir)/org && \
pdflatex -shell-escape hierarchy.tex && \
rm -f hierarchy.pdf hierarchy.aux hierarchy.log
$(srcdir)/org-stamp: $(ORG_FILES) $(configure_ac)
$(MAKE) org && touch $@

818
doc/org/hierarchy.org Normal file
View file

@ -0,0 +1,818 @@
# -*- 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.

44
doc/org/hierarchy.tex Normal file
View file

@ -0,0 +1,44 @@
\documentclass[convert={size=360}]{standalone}
\usepackage{tikz}
\usetikzlibrary{shadows}
\def\F{\mathsf{F}} % in future
\def\G{\mathsf{G}} % globally
\begin{document}
\def\mycyan{cyan!30}
\def\mypink{magenta!30}
\begin{tikzpicture}[scale=.9]
\draw[drop shadow,fill=white] (0,0) rectangle (6,7);
\path[fill=\mycyan,fill opacity=.4] (0,6.5) -- (6,3) -- (6,0) -- (0,0);
\path[fill=\mycyan,fill opacity=.5] (0,3) -- (4.5,0) -- (0,0);
\path[fill=\mypink,fill opacity=.3] (6,6.5) -- (0,3) -- (0,0) -- (6,0);
\path[fill=\mypink,fill opacity=.4] (6,3) -- (1.5,0) -- (6,0);
\draw (0,0) rectangle (6,7);
\node[align=center] (rea) at (3,6) {Reactivity\\ $\bigwedge\G\F p_i\lor \F\G q_i$};
\node[align=center] (rec) at (1.1,4.5) {Recurrence\\ $\G\F p$};
\node[align=center] (per) at (4.9,4.5) {Persistence\\ $\F\G p$};
\node[align=center] (obl) at (3,2.85) {Obligation\\ $\bigwedge\G p_i\lor \F q_i$};
\node[align=center] (saf) at (1,1) {Safety\\ $\G p$};
\node[align=center] (gua) at (5,1) {Guarantee\\ $\F p$};
\node[above left,rotate=90,color=cyan!75] (det) at (0,6.5) {Deterministic B\"uch\rlap{i}};
\node[above right,rotate=90,color=cyan](weak) at (0,0) {Monitor};
\node[below left,rotate=90,color=magenta!75](weak) at (6,6.5) {Weak B\"uch\rlap{i}};
\node[below right,rotate=90,color=magenta](weak) at (6,0) {Terminal B\"uchi};
\node[above=-1mm,red] at (rea.north) {\tt T};
\node[above,red] at (rec.north) {\tt R};
\node[above,red] at (per.north) {\tt P};
\node[above,red] at (obl.north) {\tt O};
\node[above,red] at (saf.north) {\tt S};
\node[above,red] at (gua.north) {\tt G};
\node[above,red] at (3,0.3) {\tt B};
\end{tikzpicture}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:

1
doc/org/tools.org
View file

@ -79,6 +79,7 @@ convenience, you can browse their HTML versions:
- [[file:csv.org][Reading and writing CSV files]]
- [[file:satmin.org][SAT-based minimization of Deterministic ω-Automata]]
- [[file:hierarchy.org][Exploring the temporal hierarchy of Manna & Pnueli]]
* Citing