Package owl.automaton.algorithm.simulations

Class ColorRefinement<S>

java.lang.Object

owl.automaton.algorithm.simulations.ColorRefinement<S>

Type Parameters:

S - Type of state for the underlying automaton.

public class ColorRefinement<S>
extends Object

Computes direct simulation relation of an automaton based on the color refinement algorithm. See the constructor of for more info.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	ColorRefinement.Neighborhood	Represents the neighborhood of a state.
static class	ColorRefinement.NeighborType	Represents a neighbor type consisting of color and associated valuation.

Method Summary

Modifier and Type	Method	Description
static <S> Set<Pair<S,S>>	of(Automaton<S,? extends BuchiAcceptance> automaton)	Computes the color refinement (i.e.

Methods inherited from class java.lang.Object

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

Method Detail

of

public static <S> Set<Pair<S,S>> of(Automaton<S,? extends BuchiAcceptance> automaton)

Computes the color refinement (i.e. direct simulation relation) for a given automaton. Based on the algorithm "StrongFairSimulationReduction" presented in "Optimizing Buchi Automata" by Etessami and Holzmann in 2000.

Type Parameters:

S - The type of state in the automaton.

Parameters:

automaton - The automaton to compute the refinement for.

Returns:

A set of direct-similar pairs of states.