Package owl.translations.ltl2dela

Class NormalformDELAConstruction

java.lang.Object

owl.translations.ltl2dela.NormalformDELAConstruction

All Implemented Interfaces:

Function<LabelledFormula,Automaton<NormalformDELAConstruction.State,?>>

public final class NormalformDELAConstruction
extends Object
implements Function<LabelledFormula,Automaton<NormalformDELAConstruction.State,?>>

A translation from LTL to deterministic Emerson-Lei automata using the \Delta_2-normalisation procedure. Future Work / TODO: - Use lookahead to find more accepting and rejecting sinks. For this use an exhaustive SCC analysis that is bounded by the lookahead. - Round-Robin Chains that are independent from GF- / FG-subformulas. The heuristic depends on the fact that suspension collapse a SCC to a single state. - Store round-robin chains for beta generation. - Use non-trivial beta generation (using LTL Axioms.)

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	NormalformDELAConstruction.Construction
static class	NormalformDELAConstruction.State

Constructor Summary

Constructors

Constructor	Description
NormalformDELAConstruction(OptionalInt lookahead)

Method Summary

Modifier and Type	Method	Description
Automaton<NormalformDELAConstruction.State,?>	apply(LabelledFormula formula)
NormalformDELAConstruction.Construction	applyConstruction(LabelledFormula formula)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface java.util.function.Function

andThen, compose

Constructor Detail

NormalformDELAConstruction

public NormalformDELAConstruction(OptionalInt lookahead)

Method Detail

apply

public Automaton<NormalformDELAConstruction.State,?> apply(LabelledFormula formula)

Specified by:

apply in interface Function<LabelledFormula,Automaton<NormalformDELAConstruction.State,?>>

applyConstruction

public NormalformDELAConstruction.Construction applyConstruction(LabelledFormula formula)