AFW

Module to manage AFW (Alternating Finite automaton on Words).

Formally a AFW (Alternating Finite automaton on Words) is a tuple \((Σ, S, s0, ρ, F )\), where:

  • Σ is a finite nonempty alphabet;

  • S is a finite nonempty set of states;

  • \(s0 ∈ S\) is the initial state (notice that, as in dfas, we have a unique initial state);

  • F ⊆ S is the set of accepting states;

  • \(ρ : S × Σ → B+(S)\) is a transition function. \(B+(X)\) be the set of positive Boolean formulas over a given set X ex. of \(ρ: ρ(s, a) = (s1 ∧ s2) ∨ (s3 ∧ s4)\)

In this module a AFW is defined as follows

AFW = dict() with the following keys-values:

  • alphabet => set()

  • states => set()

  • initial_state => ‘state_0’

  • accepting_states => set()

  • transitions => dict(), where

    key (state ∈ states, action ∈ alphabet)

    value [string representing a PYTHON boolean expression

    over states; where we also allow the formulas True and False]

List

formula_dual(input_formula)

Returns the dual of the input formula.

afw_complementation(afw)

Returns a AFW reading the complemented language read by input AFW.

afw_completion(afw)

Side effect on input! Complete the afw adding not present transitions and marking them as False.

afw_intersection(afw_1, afw_2)

Returns a AFW that reads the intersection of the languages read by input AFWs.

afw_nonemptiness_check(afw)

Checks if the input AFW reads any language other than the empty one, returning True/False.

afw_nonuniversality_check(afw)

Checks if the language read by the input AFW is different from Σ∗, returning True/False.

afw_to_nfa_conversion(afw)

Returns a NFA reading the same language of input AFW.

afw_union(afw_1, afw_2)

Returns a AFW that reads the union of the languages read by input AFWs.

nfa_to_afw_conversion(nfa)

Returns a AFW reading the same language of input NFA.

rename_afw_states(afw, suffix)

Side effect on input! Renames all the states of the AFW adding a suffix.

afw_word_acceptance(afw, word)

Checks if a word is accepted by input AFW, returning True/False.

Functions

PySimpleAutomata.AFW.afw_complementation(afw: dict) → dict[source]

Returns a AFW reading the complemented language read by input AFW.

Let \(A = (Σ, S, s^0 , ρ, F )\). Define \(Ā = (Σ, S, s^0 , \overline{ρ}, S − F )\), where \(\overline{ρ}(s, a) = \overline{ρ(s, a)}\) for all \(s ∈ S\) and \(a ∈ Σ\). That is, \(\overline{ρ}\) is the dualized transition function. It can be shown that \(L( Ā) = Σ^∗ − L(A)\).

The input afw need to be completed i.e. each non existing transition must be added pointing to False.

Parameters:

afw (dict) – input AFW.

Returns:

(dict) representing a AFW.

PySimpleAutomata.AFW.afw_completion(afw)[source]

Side effect on input! Complete the afw adding not present transitions and marking them as False.

Parameters:

afw (dict) – input AFW.

PySimpleAutomata.AFW.afw_intersection(afw_1: dict, afw_2: dict) → dict[source]

Returns a AFW that reads the intersection of the languages read by input AFWs.

Let \(A_1 = (Σ, S_1 , s^0_1, ρ_1 , F_1 )\) and \(A_2 = (Σ, S_2 , s^0_2, ρ_2 , F_2 )\) be alternating automata accepting the languages \(L( A_1)\) and \(L(A_2)\). Then, \(B_∩ = (Σ, S_1 ∪ S_2 ∪ {root}, root, ρ_∩ , F_1 ∪ F_2 )\) with \(ρ_∩ = ρ_1 ∪ ρ_2 ∪ [(root, a): ρ(s^0_1 , a) ∧ ρ(s^0_2 , a)]\) accepts \(L(A_1) ∩ L(A_2)\).

Parameters:

  • afw_1 (dict) – first input AFW;

  • afw_2 (dict) – second input AFW.

Returns:

(dict) representing a AFW.

PySimpleAutomata.AFW.afw_nonemptiness_check(afw: dict) → bool[source]

Checks if the input AFW reads any language other than the empty one, returning True/False.

The afw is translated into a nfa and then its nonemptiness is checked.

Parameters:

afw (dict) – input AFW.

Returns:

(bool), True if input afw is nonempty, False otherwise.

PySimpleAutomata.AFW.afw_nonuniversality_check(afw: dict) → bool[source]

Checks if the language read by the input AFW is different from Σ∗, returning True/False.

The afw is translated into a nfa and then its nonuniversality is checked.

Parameters:

afw (dict) – input AFW.

Returns:

(bool), True if input afw is nonuniversal, False otherwise.

PySimpleAutomata.AFW.afw_to_nfa_conversion(afw: dict) → dict[source]

Returns a NFA reading the same language of input AFW.

Let \(A = (Σ, S, s^0 , ρ, F )\) be an afw. Then we define the nfa \(A_N\) such that \(L(A_N) = L(A)\) as follows \(AN = (Σ, S_N , S^0_N , ρ_N , F_N )\) where:

  • \(S_N = 2^S\)

  • \(S^0_N= \{\{s^0 \}\}\)

  • \(F_N=2^F\)

  • \((Q,a,Q') ∈ ρ_N\) iff \(Q'\) satisfies \(⋀_{ s∈Q} ρ(s, a)\)

We take an empty conjunction in the definition of \(ρ_N\) to be equivalent to true; thus, \((∅, a, ∅) ∈ ρ_N\).

Parameters:

afw (dict) – input AFW.

Returns:

(dict) representing a NFA.

PySimpleAutomata.AFW.afw_union(afw_1: dict, afw_2: dict) → dict[source]

Returns a AFW that reads the union of the languages read by input AFWs.

Let \(A_1 = (Σ, S_1 , s^0_1, ρ_1 , F_1 )\) and \(A_2 = (Σ, S_2 , s^0_2, ρ_2 , F_2 )\) be alternating automata accepting the languages \(L( A_1)\) and \(L(A_2)\). Then, \(B_∪ = (Σ, S_1 ∪ S_2 ∪ {root}, ρ_∪ , root , F_1 ∪ F_2 )\) with \(ρ_∪ = ρ_1 ∪ ρ_2 ∪ [(root, a): ρ(s^0_1 , a) ∨ ρ(s^0_2 , a)]\) accepts \(L(A_1) ∪ L(A_2)\).

Pay attention to avoid having the AFWs with state names in common, in case use PySimpleAutomata.AFW.rename_afw_states function.

Parameters:

  • afw_1 (dict) – first input AFW;

  • afw_2 (dict) – second input AFW;.

Returns:

(dict) representing the united AFW.

PySimpleAutomata.AFW.afw_word_acceptance(afw: dict, word: list) → bool[source]

Checks if a word is accepted by input AFW, returning True/False.

The word w is accepted by a AFW if exists at least an accepting run on w. A run for AFWs is a tree and an alternating automaton can have multiple runs on a given input. A run is accepting if all the leaf nodes are accepting states.

Parameters:

  • afw (dict) – input AFW;

  • word (list) – list of symbols ∈ afw[‘alphabet’].

Returns:

(bool), True if the word is accepted, False otherwise.

PySimpleAutomata.AFW.formula_dual(input_formula: str) → str[source]

Returns the dual of the input formula.

The dual operation on formulas in \(B^+(X)\) is defined as: the dual \(\overline{θ}\) of a formula \(θ\) is obtained from θ by switching \(∧\) and \(∨\), and by switching \(true\) and \(false\).

Parameters:

input_formula (str) – original string.

Returns:

(str), dual of input formula.

PySimpleAutomata.AFW.nfa_to_afw_conversion(nfa: dict) → dict[source]

Returns a AFW reading the same language of input NFA.

Let \(A = (Σ,S,S^0, ρ,F)\) be an nfa. Then we define the afw AA such that \(L(AA) = L(A)\) as follows \(AA = (Σ, S ∪ {s_0}, s_0 , ρ_A , F )\) where \(s_0\) is a new state and \(ρ_A\) is defined as follows:

  • \(ρ_A(s, a)= ⋁_{(s,a,s')∈ρ}s'\), for all \(a ∈ Σ\) and \(s ∈ S\)

  • \(ρ_A(s^0, a)= ⋁_{s∈S^0,(s,a,s')∈ρ}s'\), for all \(a ∈ Σ\)

We take an empty disjunction in the definition of AA to be equivalent to false. Essentially, the transitions of A are viewed as disjunctions in AA . A special treatment is needed for the initial state, since we allow a set of initial states in nondeterministic automata, but only a single initial state in alternating automata.

Parameters:

nfa (dict) – input NFA.

Returns:

(dict) representing a AFW.

PySimpleAutomata.AFW.rename_afw_states(afw: dict, suffix: str)[source]

Side effect on input! Renames all the states of the AFW adding a suffix.

It is an utility function used during testing to avoid automata to have states with names in common.

Avoid suffix that can lead to special name like “as”, “and”,…

Parameters:

  • afw (dict) – input AFW.

  • suffix (str) – string to be added at beginning of each state name.