Package owl.translations.rabinizer
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 nontrivial product construction.
 The master tracks the evolution of the formula as
implied by the finite prefix read so far by simple unfolding. For example, the formula
phi = "a U b  X a"
would induce a master automaton with states(phi)
, @{code a U b},false
, andtrue
. This is sufficient for formulas without a "G" operator in them (or any similar temporal operator requiring infinite horizon), since a state likeG a
will never unfold tott
but still might hold for a word.  The monitors are designed to
provide this information. For each
G<psi>
in the given formula, a monitor is constructed which tracks the validity ofF G<psi>
. This, of course is not the same as the original subformula. 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 nonfalse 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 subformulas 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.
 See Also:
RabinizerBuilder
,MonitorBuilder

Class Summary Class Description MonitorState RabinizerBuilder Central class handling the Rabinizer construction.RabinizerConfiguration RabinizerState