Misc Functions on Generators

EmptyLanguage

Set generator to mark empty language.

Detailed description:

Returns a generator G with the specified alphabet Sigma, no states and no transitions; i.e., we have Lm(G) = L(G) = 0.

Parameter Conditions:

The empty language generator is deterministic.

IsEmptyLanguage

Test Generator G for empty marked language Lm(G).

Parameter Conditions:

The argument may be non-deterministic.

Automaton

Convert generator to formal automaton.

Detailed description:

Converts the given generator G to a formal automaton that generates the same marked language Lm(G) while accepting any input string, i.e. L(G) = Sigma*. This is achieved by introducing a dump state to represent Sigma*-Closure(Lm(G)).

Example:

G GRes

Parameter Conditions:

The provided generator is assumed to be deterministic. The resulting generator is guaranteed to be deterministic.

IsPrefixClosed

Tests a language for being prefix-closed.

Detailed description:

A language L is prefix-closed if for each string s ∈ L all prefixes r ≤ s are also element of L:

s ∈ L and r ≤ s    ⇒    r ∈ L.

The function IsPrefixClosed tests whether the language Lm(G) marked by the specified generator G is prefix-closed. It does so by testing whether any state that is accessible and co-accessible also is marked. For deterministic generators, this condition is sufficient and necessary. In general, it is only sufficient.

Example:

G

The language Lm(G) marked by the above generator is not prefix-closed, since the states 1, 2 and 4 are accessible and co-accessible but not marked. For example, the string ac ∉ Lm(G) is a prefix of acbb ∈ Lm(G).

PrefixClosure

Compute prefix closure for given language.

Detailed description:

For any language L there exists a smallest prefix-closed superset, the so-called prefix-closure of L:

Closure(L) := {r ∈ Sigma*| ∃ s ∈ L : r ≤ s}.

This function computes a realisation of the prefix-closure of Lm(GArg) by first erasing all states that are not co-accessible and then marking the remaining states.

Example:

G GRes

IsOmegaClosed

Tests a language for being omega-closed.

Detailed description:

A omega-language L ⊆ Sigma^w is omega-closed if any strictly increasing sequence of prefixes from L converges to an omega-string in L, i.e. if

L = B(Prefix(L)),

where Prefix(L) ⊆ Sigma* denotes the set of all finite prefixes from L and B(.) is the adherence operator.

The function IsOmegaClosed tests for the specified generator G whether Bm(G) is omega-closed. The implementation first computes the omega-trim state set. If within this set there exists an SCC with no marked states the function returns false. Else it returns true.

Example:

G

The language Bm(G) realized by the above generator is not omega-closed. The states 6 and 7 constitute an SCC when restricting G to the omega-trim state set {1,2,4,6,7}. Thus, the limit of the sequence a d (a b)^i is in B(Prefix(L)) but not in B(L). The function IsOmegaClosed returns false.

Parameter Conditions:

The argument must be deterministic.

OmegaClosure

Compute omega closure for given language.

Detailed description:

For any omega-language L ⊆ Sigma^w there exists a smallest omega-closed superset, the so-called omega-closure or topological closure of L:

Closure(L) = B(Prefix(L)) ⊆ Sigma^w,

where Prefix(H) ⊆ Sigma* denotes the set of all finite prefixes from H and B(.) is the limit operator ; see also IsOmegaClosed.

The function OmegaClosure computes a realisation of the the omega-closure for the specified omega language Bm(GArg). It first invokes OmegaTrim and then markes all states. Thus, Closure(Bm(GArg)) = B(GRes) = Bm(GRes) and Prefix(Bm(GArg)) = L(GRes) = Lm(GRes).

Example:

G GRes