@EverythingIsNonnullByDefault

Package owl.translations.rabinizer

A translation from LTL to tDGRA.

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.

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.

See Also:
RabinizerBuilder, MonitorBuilder
Skip navigation links