# 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]

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. (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. (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. (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. (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. (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;. (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’]. (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. (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. (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.