@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 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, 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.
  • The monitors are designed to provide this information. For each 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.

See Also:
RabinizerBuilder, MonitorBuilder