Automata

Note

All the following automata inherit from ggsolver.logic.base.Automaton. Refer to the class documentation for a description of inherited functions.

DFA: Deterministic Finite Automaton

class ggsolver.logic.automata.DFA(states=None, atoms=None, trans_dict=None, init_state=None, final=None)

Represents a Deterministic Finite-state base.Automaton.

• Acceptance Type: base.Automaton.ACC_REACH

• Acceptance condition: (Reach, 0)

  • Accepts: Finite words.

  • Interpretation: \(\mathsf{Last}(\rho) \in F\) where \(F = \{q \in Q \mid \mathsf{AccSet}(q) = 0\}\)

• Number of Acceptance Sets: 1

• final(state) function returns either -1 to indicate that the state is not accepting or 0 to indicate that the state is accepting with acceptance set 0.

__init__(states=None, atoms=None, trans_dict=None, init_state=None, final=None)

Constructs a DFA.

Parameters

• states – (Iterable) An iterable over states in the automaton.

• atoms – (Iterable[str]) An iterable over atomic propositions in the automaton.

• trans_dict – (dict) A dictionary defining the (deterministic) transition function of automaton. Format of dictionary: {state: {logic.PLFormula: state}}

• init_state – (object) The initial state, a member of states iterable.

• final – (Iterable[states]) The set of final states, a subset of states iterable.

Monitor: Deterministic Safety Automaton

class ggsolver.logic.automata.Monitor(states=None, atoms=None, trans_dict=None, init_state=None, final=None)

Represents a Safety automaton.

• Acceptance Type: base.Automaton.ACC_SAFETY

• Acceptance condition: (Safety, 0)

  • Accepts: Infinite words.

  • Interpretation: \(\mathsf{Occ}(\rho) \subseteq F\) where \(F = \{q \in Q \mid \mathsf{AccSet}(q) = 0\}\)

• Number of Acceptance Sets: 1

• final(state) function returns either -1 to indicate that the state is not accepting or 0 to indicate that the state is accepting with acceptance set 0.

__init__(states=None, atoms=None, trans_dict=None, init_state=None, final=None)

Constructs a Monitor.

Parameters

• states – (Iterable) An iterable over states in the automaton.

• atoms – (Iterable[str]) An iterable over atomic propositions in the automaton.

• trans_dict – (dict) A dictionary defining the (deterministic) transition function of automaton. Format of dictionary: {state: {logic.PLFormula: state}}

• init_state – (object) The initial state, a member of states iterable.

• final – (Iterable[states]) The set of final states, a subset of states iterable.

DBA: Deterministic Buchi Automaton

class ggsolver.logic.automata.DBA(states=None, atoms=None, trans_dict=None, init_state=None, final=None)

Represents a Deterministic Buchi automaton.

• Acceptance Type: base.Automaton.ACC_BUCHI

• Acceptance condition: (Buchi, 0)

  • Accepts: Infinite words.

  • Interpretation: \(\mathsf{Inf}(\rho) \cap F \neq \emptyset\) where \(F = \{q \in Q \mid \mathsf{AccSet}(q) = 0\}\)

• Number of Acceptance Sets: 1

• final(state) function returns either -1 to indicate that the state is not accepting or 0 to indicate that the state is accepting with acceptance set 0.

__init__(states=None, atoms=None, trans_dict=None, init_state=None, final=None)

Constructs a DBA.

Parameters

• states – (Iterable) An iterable over states in the automaton.

• atoms – (Iterable[str]) An iterable over atomic propositions in the automaton.

• trans_dict – (dict) A dictionary defining the (deterministic) transition function of automaton. Format of dictionary: {state: {logic.PLFormula: state}}

• init_state – (object) The initial state, a member of states iterable.

• final – (Iterable[states]) The set of final states, a subset of states iterable.

DCBA: Deterministic co-Buchi Automaton

class ggsolver.logic.automata.DCBA(states=None, atoms=None, trans_dict=None, init_state=None, final=None)

Represents a Deterministic co-Buchi automaton.

• Acceptance Type: base.Automaton.ACC_COBUCHI

• Acceptance condition: (co-Buchi, 0)

  • Accepts: Infinite words.

  • Interpretation: \(\mathsf{Inf}(\rho) \subseteq F\) where \(F = \{q \in Q \mid \mathsf{AccSet}(q) = 0\}\)

• Number of Acceptance Sets: 1

• final(state) function returns either -1 to indicate that the state is not accepting or 0 to indicate that the state is accepting with acceptance set 0.

__init__(states=None, atoms=None, trans_dict=None, init_state=None, final=None)

Constructs a DCBA.

Parameters

• states – (Iterable) An iterable over states in the automaton.

• atoms – (Iterable[str]) An iterable over atomic propositions in the automaton.

• trans_dict – (dict) A dictionary defining the (deterministic) transition function of automaton. Format of dictionary: {state: {logic.PLFormula: state}}

• init_state – (object) The initial state, a member of states iterable.

• final – (Iterable[states]) The set of final states, a subset of states iterable.

DPA: Deterministic Parity Automaton

class ggsolver.logic.automata.DPA(states=None, atoms=None, trans_dict=None, init_state=None, final=None)

Represents a Deterministic Buchi automaton.

• Acceptance Type: base.Automaton.ACC_PARITY

• Acceptance condition: (Parity Min Even , 0)

  • Accepts: Infinite words.

  • Interpretation: \(\min_{q \in \mathsf{Inf}(\rho)} \chi(q)\) is even, where \(\chi: Q \rightarrow \mathbb{N}\) is a coloring function that associates every state in DPA with a color (an integer).

• Number of Acceptance Sets: k, where k is a positive integer.

• final(state) a value between 0 and k-1 to indicate that the color of a state.

Note

The DPA definition is not stable. DO NOT USE IT!

__init__(states=None, atoms=None, trans_dict=None, init_state=None, final=None)

Constructs a DPA.

Parameters

• states – (Iterable) An iterable over states in the automaton.

• atoms – (Iterable[str]) An iterable over atomic propositions in the automaton.

• trans_dict – (dict) A dictionary defining the (deterministic) transition function of automaton. Format of dictionary: {state: {logic.PLFormula: state}}

• init_state – (object) The initial state, a member of states iterable.

• final – (dict[state: int]) A state to color mapping.