Logic

Automaton

class ggsolver.logic.Automaton(**kwargs)

Represents an Automaton.

\[\mathcal{A} = (Q, \Sigma := 2^{AP}, \delta, q_0, F)\]

In the Automaton class, each component is represented as a function.

• The set of states \(Q\) is represented by Automaton.states function,

• The set of atomic propositions \(AP\) is represented by Automaton.atoms function,

• The set of symbols \(\Sigma\) is represented by Automaton.sigma function,

• The transition function \(\delta\) is represented by Automaton.delta function,

• The initial state \(q_0\) is represented by Automaton.init_state function.

An automaton may have one of the following acceptance conditions:

• (Automaton.ACC_REACH, 0)

• (Automaton.ACC_SAFETY, 0)

• (Automaton.ACC_BUCHI, 0)

• (Automaton.ACC_COBUCHI, 0)

• (Automaton.ACC_PARITY, 0)

• (Automaton.ACC_PREF_LAST, None)

• (Automaton.ACC_ACC_PREF_MP, None)

ACC_BUCHI = 'Buchi'

ACC_COBUCHI = 'co-Buchi'

ACC_PARITY = 'Parity Min Even'

ACC_PREF_LAST = 'Preference Last'

ACC_PREF_MP = 'Preference MostPreferred'

ACC_REACH = 'Reach'

ACC_SAFETY = 'Safety'

ACC_TYPES = ['undefined', 'Reach', 'Safety', 'Buchi', 'co-Buchi', 'Parity Min Even', 'Preference Last', 'Preference MostPreferred']

Acceptance conditions supported by Automaton.

acc_cond()

Acceptance condition of the automaton.

Returns

(2-tuple) A value of type (acc_type, acc_set) where acc_type is from Automaton.ACC_TYPES and acc_set is either an integer or a list of integer.

acc_type()

Acceptance type of the automaton.

Returns

A value from Automaton.ACC_TYPES.

atoms()

Returns a list/tuple of atomic propositions.

Returns

(list of str) A list of atomic proposition.

final(state)

Returns the acceptance set associated with the given state.

Parameters

state – (an element of self.states()) A valid state.

Returns

(int) Acceptance set associated with the given state.

from_automaton(aut: Automaton)

Constructs an Automaton from another Automaton instance. The input automaton’s acceptance condition must match that of a current Automaton.

is_complete()

Is the automaton complete? That is, is transition function well-defined at every state for any input symbol?

num_acc_sets()

Number of acceptance sets.

sigma()

Returns the set of alphabet of automaton. It is the powerset of atoms().

SpotAutomaton

class ggsolver.logic.SpotAutomaton(formula=None, options=None, atoms=None)

SpotAutomaton constructs an Automaton from an LTL specification string using spot (https://spot.lrde.epita.fr/) with customizations for ggsolver.

Customizations: Since ggsolver contains several algorithms for reactive/controller synthesis, we prefer to construct deterministic automata. Given an LTL formula, SpotAutomaton automatically determines the best acceptance condition that would result in a deterministic automaton..

Programmer’s note: The graphified version of automaton does not use PL formulas as edge labels. This is intentionally done to be able to run our codes on robots that may not have logic libraries installed.

acc_cond()

Returns acceptance condition according to ggsolver definitions: See ACC_REACH, … variables in Automaton class. See SpotAutomaton.spot_acc_cond() for acceptance condition in spot’s nomenclature.

acc_name()

Name of acceptance condition as per spot’s nomenclature.

atoms()

Atomic propositions appearing in LTL formula.

delta(state, inp)

Transition function of automaton. For a deterministic automaton, returns a single state. Otherwise, returns a list/tuple of states.

Parameters

• state – (object) A valid state.

• inp – (list) List of atoms that are true (an element of sigma).

final(state)

Maps every state to its acceptance set.

formula()

The LTL Formula.

init_state()

Initial state of automaton.

is_complete()

Is the automaton complete?

is_deterministic()

Is the automaton deterministic?

is_inherently_weak()

Is it the case that accepting and rejecting cycles cannot be mixed in the same SCC?

is_semi_deterministic()

Is the automaton semi-deterministic? See https://spot.lrde.epita.fr/doxygen/namespacespot.html#a56b3f00b7b93deafb097cad595998783

is_state_based_acc()

Is the acceptance condition state-based?

is_stutter_invariant()

The property recognized by the automaton is stutter-invariant (see https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf)

is_terminal()

Automaton is weak, accepting SCCs are complete, accepting edges may not go to rejecting SCCs. An automaton is weak if the transitions of an SCC all belong to the same acceptance sets.

See https://spot.lrde.epita.fr/concepts.html

is_unambiguous()

There is at most one run accepting a word (but it might be recognized several time). See https://spot.lrde.epita.fr/concepts.html.

is_weak()

Are transitions of an SCC all belong to the same acceptance sets?

num_acc_sets()

Number of acceptance sets.

spot_acc_cond()

Acceptance condition in spot’s nomenclature.

states()

States of automaton.

PL

class ggsolver.logic.PL(f_str, atoms=None)

PL formula is internally represented as spot.formula instance.

allsat()

Generates the set of all satisfying assignments to atoms of the given propositional logic formula.

Note

Complexity: Exponential in the number of atoms.

atoms()

Gets the list of atoms associated with PL formula.

The list may contain atoms that do not appear in the formula, if the user has provided it. :return: (List[str]) List of atoms.

evaluate(true_atoms)

Evaluates a propositional logic formula given the set of true atoms.

Parameters

true_atoms – (Iterable[str]) A propositional logic formula.

Returns

(bool) True if formula is true, otherwise False.

simplify()

Simplifies a propositional logic formula.

We use the boolean_to_isop=True option for spot.simplify. See https://spot.lrde.epita.fr/doxygen/classspot_1_1tl__simplifier__options.html

Returns

(str) String representing simplified formula.

translate()

Translate a propositional logic formula to an automaton. :return: (SpotAutomaton) SpotAutomaton representing the automaton for PL formula.

ScLTL

class ggsolver.logic.ScLTL(f_str, atoms=None)

ScLTL formula is internally represented as spot.formula instance.

LTL

class ggsolver.logic.LTL(f_str, atoms=None)

LTL formula is internally represented as spot.formula instance.

evaluate(true_atoms)

Evaluates a propositional logic formula given the set of true atoms.

Parameters

true_atoms – (Iterable[str]) A propositional logic formula.

Returns

(bool) True if formula is true, otherwise False.

simplify()

Simplifies a propositional logic formula.

We use the boolean_to_isop=True option for spot.simplify. See https://spot.lrde.epita.fr/doxygen/classspot_1_1tl__simplifier__options.html

Returns

(str) String representing simplified formula.