Rabinizer is a construction to translate LTL formulas to deterministic (generalized) Rabin
automata, additionally providing semantic information for all states, compared to
LTL->NBA->DRA
approaches using Safra trees, which lose any reasonable state space information in
the determinization process. It is the conceptual father to most other LTL translations in
owl.
The basic idea of Rabinizer is as follows. The resulting automaton consists of two different building blocks, the "master automaton" and the "monitors", which then are connected by a non-trivial product construction.
phi
= "a U b | X a"
would induce a master automaton with states (phi)
, @{code a U b},
false
, and true
. This is sufficient for formulas without a "G" operator in them (or any
similar temporal operator requiring infinite horizon), since a state like G a
will never
unfold to tt
but still might hold for a word.G<psi>
in the given formula, a monitor is constructed
which tracks the validity of F G<psi>
. This, of course is not the same as the original
sub-formula. The product construction takes care of connecting the provided information as
needed. The central idea of the product construction is the following. The state
of the master automaton gives us a "safety" condition - it tracks what was definitely satisfied
and definitely violated by the finite prefix. If we now "stabilize" to certain non-false states
in the master, we now use the monitors to decide the infinite time behaviour. Consider the
following setting. We remain in state G<psi>
in the master, hence we know that no finite
prefix violates G<psi>
. If the monitor for <psi>
accepts, we also know that
F G<psi>
holds. Together, we can deduce that the word satisfies G<psi>
.
This concept is encoded into the acceptance condition. We use a big disjunction of conditions
which allows the automaton to "guess" which G sub-formulas will accept. This is called the
"active set" |G|. Consider, for example, the formula G a XOR G b
. There, |G|
= {G a}
and |G| = {G b}
would accept, but not {G a, G b}
. The first part of each
condition therefore is a check if the chosen set entails the current master state, the
second part checks if all monitors satisfy this "promise".
Unfortunately, the actual construction is more complicated as soon as nested G formulae are involved. Explaining these technicalities is beyond the scope of this documentation and the interested reader is referred to actual paper defining the construction.
RabinizerBuilder
,
MonitorBuilder
Class | Description |
---|---|
RabinizerBuilder |
Central class handling the Rabinizer construction.
|
RabinizerCliParser | |
RabinizerConfiguration | |
RabinizerDegeneralizeMain | |
RabinizerMain | |
RabinizerState |