Models¶

Automaton¶

class ggsolver.logic.base.Automaton(**kwargs)[source]¶

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.

__init__(**kwargs)[source]¶

Supported keyword arguments:

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.
acc_cond – (tuple) A tuple of automaton acceptance type and an acceptance set. For example, DFA has an acceptance condition of (Automaton.ACC_REACH, 0).
is_deterministic – (bool) Whether the Automaton is deterministic.

acc_cond()[source]¶

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()[source]¶

Acceptance type of the automaton.

Returns: A value from Automaton.ACC_TYPES.

atoms()[source]¶

Returns a list/tuple of atomic propositions.

Returns: (list of str) A list of atomic proposition.

classmethod deserialize(obj_dict)¶

Constructs a graphical model from a serialized graph object. The node properties are deserialized as state properties, the edge properties are deserialized as transition properties, and the graph properties are deserialized as model properties. All the deserialized properties are represented as a function in the GraphicalModel class. See example #todo.

The format is described in GraphicalModel.serialize().

Returns: (Sub-class of GraphicalModel) An instance of the cls class. cls must be a sub-class of GraphicalModel.

final(state)[source]¶

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)[source]¶: Constructs an Automaton from another Automaton instance. The input automaton’s acceptance condition must match that of a current Automaton.

graphify(pointed=False, base_only=False)¶

Constructs the underlying graph of the graphical model.

Parameters: pointed – (bool) If pointed is True, the TSys.graphify_pointed() is called, which constructs a pointed graphical model containing only the states reachable from the initial state. Otherwise, TSys.graphify_unpointed() is called, which constructs the complete transition system.
Returns: (ggsolver.graph.Graph object) An equivalent graph representation of the graphical model.

init_state()¶: Returns the initial state of the graphical model.

initialize(state)¶: Sets the initial state of the graphical model.

Note

The function does NOT check if the given state is valid.

is_complete()[source]¶: Is the automaton complete? That is, is transition function well-defined at every state for any input symbol?

is_deterministic()¶: Returns True if the graphical model is deterministic. Else, returns False.

is_nondeterministic()¶: Returns True if the graphical model is non-deterministic. Else, returns False.

is_probabilistic()¶: Returns True if the graphical model is probabilistic. Else, returns False.

classmethod load(fpath, protocol='json')¶

Loads the graphical model from file.

Parameters

fpath – (str) Path to which the file should be saved. Must include an extension.
protocol – (str) The protocol to use to save the file. Options: {“json” [Default], “pickle”}.

Note

Pickle protocol is not tested.

num_acc_sets()[source]¶: Number of acceptance sets.

save(fpath, pointed=False, overwrite=False, protocol='json')¶

Saves the graphical model to file.

Parameters

fpath – (str) Path to which the file should be saved. Must include an extension.
pointed – (bool) If pointed is True, the TSys.graphify_pointed() is called, which constructs a pointed graphical model containing only the states reachable from the initial state. Otherwise, TSys.graphify_unpointed() is called, which constructs the complete transition system.
overwrite – (bool) Specifies whether to overwrite the file, if it exists. [Default: False]
protocol – (str) The protocol to use to save the file. Options: {“json” [Default], “pickle”}.

Note

Pickle protocol is not tested.

serialize()¶

Serializes the underlying graph of the graphical model into a dictionary with the following format. The state properties are saved as node properties, transition properties are stored are edge properties and model properties are stored as graph properties in the underlying graph:

{
    "graph": {
        "nodes": <number of nodes>,
        "edges": {
            uid: {vid: key},
            ...
        }
        "node_properties": {
            "property_name": {
                "default": <value>,
                "dict": {
                    "uid": <property value>,
                    ...
                }
            },
            ...
        },
        "edge_properties": {
            "property_name": {
                "default": <value>,
                "dict": [{"edge": [uid, vid, key], "pvalue": <property value>} ...]
            },
            ...
        },
        "graph_properties": {
            "property_name": <value>,
            ...
        }
    }
}

Returns: (dict) Serialized graphical model.

sigma()[source]¶: Returns the set of alphabet of automaton. It is the powerset of atoms().

states()¶

Defines the states component of the graphical model.

Returns: (list/tuple of JSONifiable object). List or tuple of states.

TSys¶

class ggsolver.models.TSys(is_deterministic=True, is_probabilistic=False, **kwargs)[source]¶

Represents a transition system [Principles of Model Checking, Def. 2.1].

\[TSys = (S, A, T, AP, L)\]

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

The set of states \(S\) is represented by TSys.states function,
The set of actions \(A\) is represented by TSys.actions function,
The transition function \(T\) is represented by TSys.delta function,
The set of atomic propositions is represented by TSys.atoms function,
The labeling function \(L\) is represented by TSys.label function.

All of the above functions are marked abstract. The recommended way to use TSys class is by subclassing it and implementing its component functions.

A transition system can be either deterministic or non-deterministic or probabilistic. To define a deterministic transition system, provide a keyword argument is_deterministic=True to the constructor. To define a nondeterministic transition system, provide a keyword argument is_deterministic=False to the constructor. To define a probabilistic transition system, provide a keyword arguments is_deterministic=False, is_probabilistic=True to the constructor.

The design of TSys class closely follows its mathematical definition. Hence, the signatures of delta function for deterministic, nondeterministic, probabilistic transition systems are different.

deterministic: delta(state, act) -> single state
non-deterministic: delta(state, act) -> a list of states
probabilistic: delta(state, act) -> a distribution over states

An important feature of TSys class is the graphify() function. It constructs a Graph object that is equivalent to the transition system. The nodes of the Graph represent the states of TSys, the edges of the Graph are defined by the set of actions and the delta function. The atomic propositions, labeling function are stored as node, edge and graph properties. By default, every Graph returned a TSys.graphify() function have the following (node/edge/graph) properties:

state: (node property) A Map from every node to the state of transition system it represents.
actions: (graph property) List of valid actions.
input: (edge property) A map from every edge (uid, vid, key) to its associated action label.
prob: (edge property) The probability associated with the edge (uid, vid, key).
atoms: (graph property) List of valid atomic propositions.
label: (node property) A map every node to the list of atomic propositions true in the state represented by that node.
init_state: (graph property) Initial state of transition system.
is_deterministic: (graph property) Is the transition system deterministic?
is_probabilistic: (graph property) Is the transition system probabilistic?

Note: Some features of probabilistic transition system are not tested. If you are trying to implement a probabilistic transition system, reach out to Abhishek Kulkarni (a.kulkarni2@ufl.edu).

Next, we demonstrate how to use TSys class to define a deterministic, non-deterministic and probabilistic transition system.

__init__(is_deterministic=True, is_probabilistic=False, **kwargs)[source]¶

Constructs a transition system.

Parameters

is_deterministic – (bool). If True then the transition system is deterministic. Otherwise, it is either non-deterministic or probabilistic.
is_probabilistic – (bool). If is_deterministic is False, then if is_probabilistic is True then the transition system is probabilistic. Otherwise, it is non-deterministic.
input_domain – (optional, str). Name of the member function of TSys class that defines the inputs to the transition system. [Default: “actions”]
init_state – (optional, JSON-serializable object). The initial state of the transition system.

actions()[source]¶

Defines the actions component of the transition system.

Returns: (list/tuple of str). List or tuple of action labels.

atoms()[source]¶

Defines the atomic propositions component of the transition system.

Returns: (list/tuple of str). List or tuple of atomic proposition labels.

delta(state, act)[source]¶

Defines the transition function of the transition system.

Parameters

state – (object) A valid state.
act – (str) An action.

Returns

(object/list(object)/util.Distribution object). Depending on the type of transition system, the return type is different. - Deterministic: returns a single state. - Non-deterministic: returns a list/tuple of states. - Probabilistic: returns a distribution over all state.

classmethod deserialize(obj_dict)¶

Constructs a graphical model from a serialized graph object. The node properties are deserialized as state properties, the edge properties are deserialized as transition properties, and the graph properties are deserialized as model properties. All the deserialized properties are represented as a function in the GraphicalModel class. See example #todo.

The format is described in GraphicalModel.serialize().

Returns: (Sub-class of GraphicalModel) An instance of the cls class. cls must be a sub-class of GraphicalModel.

graphify(pointed=False, base_only=False)¶

Constructs the underlying graph of the graphical model.

Parameters: pointed – (bool) If pointed is True, the TSys.graphify_pointed() is called, which constructs a pointed graphical model containing only the states reachable from the initial state. Otherwise, TSys.graphify_unpointed() is called, which constructs the complete transition system.
Returns: (ggsolver.graph.Graph object) An equivalent graph representation of the graphical model.

init_state()¶: Returns the initial state of the graphical model.

initialize(state)¶: Sets the initial state of the graphical model.

Note

The function does NOT check if the given state is valid.

is_deterministic()¶: Returns True if the graphical model is deterministic. Else, returns False.

is_nondeterministic()¶: Returns True if the graphical model is non-deterministic. Else, returns False.

is_probabilistic()¶: Returns True if the graphical model is probabilistic. Else, returns False.

label(state)[source]¶

Defines the labeling function of the transition system.

Parameters: state – (object) A valid state.
Returns: (list/tuple of str). A list/tuple of atomic propositions that are true in the given state.

classmethod load(fpath, protocol='json')¶

Loads the graphical model from file.

Parameters

fpath – (str) Path to which the file should be saved. Must include an extension.
protocol – (str) The protocol to use to save the file. Options: {“json” [Default], “pickle”}.

Note

Pickle protocol is not tested.

save(fpath, pointed=False, overwrite=False, protocol='json')¶

Saves the graphical model to file.

Parameters

fpath – (str) Path to which the file should be saved. Must include an extension.
pointed – (bool) If pointed is True, the TSys.graphify_pointed() is called, which constructs a pointed graphical model containing only the states reachable from the initial state. Otherwise, TSys.graphify_unpointed() is called, which constructs the complete transition system.
overwrite – (bool) Specifies whether to overwrite the file, if it exists. [Default: False]
protocol – (str) The protocol to use to save the file. Options: {“json” [Default], “pickle”}.

Note

Pickle protocol is not tested.

serialize()¶

Serializes the underlying graph of the graphical model into a dictionary with the following format. The state properties are saved as node properties, transition properties are stored are edge properties and model properties are stored as graph properties in the underlying graph:

{
    "graph": {
        "nodes": <number of nodes>,
        "edges": {
            uid: {vid: key},
            ...
        }
        "node_properties": {
            "property_name": {
                "default": <value>,
                "dict": {
                    "uid": <property value>,
                    ...
                }
            },
            ...
        },
        "edge_properties": {
            "property_name": {
                "default": <value>,
                "dict": [{"edge": [uid, vid, key], "pvalue": <property value>} ...]
            },
            ...
        },
        "graph_properties": {
            "property_name": <value>,
            ...
        }
    }
}

Returns: (dict) Serialized graphical model.

states()¶

Defines the states component of the graphical model.

Returns: (list/tuple of JSONifiable object). List or tuple of states.

Game¶

class ggsolver.models.Game(is_turn_based=True, is_deterministic=True, is_probabilistic=False, **kwargs)[source]¶

Represents a game transition system, hereafter referred simply as a game. A Game can represent two mathematical structures commonly used in literature, namely

\[G = (S, A, T, AP, L, formula)\]

\[G = (S, A, T, F, WinCond)\]

In the Game class, each component is represented as a function. By defining the relevant functions, a Game class may represent either of the two mathematical structures.

The set of states \(S\) is represented by Game.states function,
The set of actions \(A\) is represented by Game.actions function,
The transition function \(T\) is represented by Game.delta function,
The set of atomic propositions \(AP\) is represented by Game.atoms function,
The labeling function \(L\) is represented by Game.label function.
When the winning condition is represented by a logic formula \(formula\), we define Game.formula function.
When the winning condition is represented by a final states \(F\), we define Game.final function. In this case, we must also specify the acceptance condition.
The winning condition \(WinCond\) is represented by Game.win_cond function.

All of the above functions are marked abstract. The recommended way to use Game class is by subclassing it and implementing the relevant component functions.

Categorization of a Game: A game is categorized by three types:

A game can be either deterministic or non-deterministic or probabilistic. To define a deterministic transition system, provide a keyword argument is_deterministic=True to the constructor. To define a nondeterministic transition system, provide a keyword argument is_deterministic=False to the constructor. To define a probabilistic transition system, provide a keyword arguments is_deterministic=False, is_probabilistic=True to the constructor.

The design of Game class closely follows its mathematical definition. Hence, the signatures of delta function for deterministic, nondeterministic, probabilistic games are different.
- deterministic: delta(state, act) -> single state
- non-deterministic: delta(state, act) -> a list of states
- probabilistic: delta(state, act) -> a distribution over states
A game can be turn-based or concurrent. To define a concurrent game, provide a keyword argument is_turn_based=False. The game is turn_based by default.
A game can be a 1/1.5/2/2.5-player game. A one-player game models a deterministic motion planning-type problem in a static environment. A 1.5-player game is an MDP. A two-player game models a deterministic interaction between two strategic players. And, a 2.5-player game models a stochastic interaction between two strategic players.

If a game is one or two player, then the Game.delta() is deterministic. If a game is 1.5 or 2.5 player, then the Game.delta() is either non-deterministic (when transition probabilities are unknown), and probabilistic (when transition probabilities are known).

Every state in a turn-based game is controlled by a player. To define which player controls which state, define a game component Game.turn() which takes in a state and returns a value between 0 and 3 to indicate which player controls the state.

An important feature of Game class is the graphify() function. It constructs a Graph object that is equivalent to the game. The nodes of the Graph represent the states of Game, the edges of the Graph are defined by the set of actions and the delta function. The atomic propositions, labeling function are stored as node, edge and graph properties. By default, every Graph returned a Game.graphify() function have the following (node/edge/graph) properties:

state: (node property) A Map from every node to the state of transition system it represents.
input_domain: (graph property) Name of function that defines input domain of game (=”actions”).
actions: (graph property) List of valid actions.
input: (edge property) A map from every edge (uid, vid, key) to its associated action label.
prob: (edge property) The probability associated with the edge (uid, vid, key).
atoms: (graph property) List of valid atomic propositions.
label: (node property) A map every node to the list of atomic propositions true in the state represented by that node.
init_state: (graph property) Initial state of transition system.
is_deterministic: (graph property) Is the transition system deterministic?
is_probabilistic: (graph property) Is the transition system probabilistic?
is_turn_based: (graph property) Is the transition system turn-based?
final: (node property) Returns an integer denoting the acceptance set the state belongs to.
win_cond: (graph property) The winning condition of the game.
formula: (graph property) A logic formula representing the winning condition of the game.
turn: (node property) A map from every node to an integer (0/1/2) that denotes which player controls the node.
p1_acts: (graph property) A subset of actions accessible to P1.
p2_acts: (graph property) A subset of actions accessible to P2.

Note: Some features of probabilistic transition system are not tested. If you are trying to implement a probabilistic transition system, reach out to Abhishek Kulkarni (a.kulkarni2@ufl.edu).

__init__(is_turn_based=True, is_deterministic=True, is_probabilistic=False, **kwargs)[source]¶

Constructs a transition system.

Parameters

is_deterministic – (bool). If True then the transition system is deterministic. Otherwise, it is either non-deterministic or probabilistic.
is_probabilistic – (bool). If is_deterministic is False, then if is_probabilistic is True then the transition system is probabilistic. Otherwise, it is non-deterministic.
input_domain – (optional, str). Name of the member function of TSys class that defines the inputs to the transition system. [Default: “actions”]
init_state – (optional, JSON-serializable object). The initial state of the transition system.

actions()¶

Defines the actions component of the transition system.

Returns: (list/tuple of str). List or tuple of action labels.

atoms()¶

Defines the atomic propositions component of the transition system.

Returns: (list/tuple of str). List or tuple of atomic proposition labels.

delta(state, act)¶

Defines the transition function of the transition system.

Parameters

state – (object) A valid state.
act – (str) An action.

Returns

(object/list(object)/util.Distribution object). Depending on the type of transition system, the return type is different. - Deterministic: returns a single state. - Non-deterministic: returns a list/tuple of states. - Probabilistic: returns a distribution over all state.

classmethod deserialize(obj_dict)¶

Constructs a graphical model from a serialized graph object. The node properties are deserialized as state properties, the edge properties are deserialized as transition properties, and the graph properties are deserialized as model properties. All the deserialized properties are represented as a function in the GraphicalModel class. See example #todo.

The format is described in GraphicalModel.serialize().

Returns: (Sub-class of GraphicalModel) An instance of the cls class. cls must be a sub-class of GraphicalModel.

final(state)[source]¶

Defines whether the given state is a final state. The structure of final state is based on the winning condition [See Automata, Logics and Infinite Games (Ch. 2)].

Parameters: state – (object) A valid state.
Returns: (int or a list of ints). The integer denotes the acceptance set the state belongs to.

formula()[source]¶: A logic formula representing the winning condition of the game.

graphify(pointed=False, base_only=False)¶

Constructs the underlying graph of the graphical model.

Parameters: pointed – (bool) If pointed is True, the TSys.graphify_pointed() is called, which constructs a pointed graphical model containing only the states reachable from the initial state. Otherwise, TSys.graphify_unpointed() is called, which constructs the complete transition system.
Returns: (ggsolver.graph.Graph object) An equivalent graph representation of the graphical model.

init_state()¶: Returns the initial state of the graphical model.

initialize(state)¶: Sets the initial state of the graphical model.

Note

The function does NOT check if the given state is valid.

is_deterministic()¶: Returns True if the graphical model is deterministic. Else, returns False.

is_nondeterministic()¶: Returns True if the graphical model is non-deterministic. Else, returns False.

is_probabilistic()¶: Returns True if the graphical model is probabilistic. Else, returns False.

is_turn_based()[source]¶: Is the game turn based?

label(state)¶

Defines the labeling function of the transition system.

Parameters: state – (object) A valid state.
Returns: (list/tuple of str). A list/tuple of atomic propositions that are true in the given state.

classmethod load(fpath, protocol='json')¶

Loads the graphical model from file.

Parameters

fpath – (str) Path to which the file should be saved. Must include an extension.
protocol – (str) The protocol to use to save the file. Options: {“json” [Default], “pickle”}.

Note

Pickle protocol is not tested.

p1_acts()[source]¶: A subset of actions accessible to P1.

p2_acts()[source]¶: A subset of actions accessible to P2.

save(fpath, pointed=False, overwrite=False, protocol='json')¶

Saves the graphical model to file.

Parameters

fpath – (str) Path to which the file should be saved. Must include an extension.
pointed – (bool) If pointed is True, the TSys.graphify_pointed() is called, which constructs a pointed graphical model containing only the states reachable from the initial state. Otherwise, TSys.graphify_unpointed() is called, which constructs the complete transition system.
overwrite – (bool) Specifies whether to overwrite the file, if it exists. [Default: False]
protocol – (str) The protocol to use to save the file. Options: {“json” [Default], “pickle”}.

Note

Pickle protocol is not tested.

serialize()¶

Serializes the underlying graph of the graphical model into a dictionary with the following format. The state properties are saved as node properties, transition properties are stored are edge properties and model properties are stored as graph properties in the underlying graph:

{
    "graph": {
        "nodes": <number of nodes>,
        "edges": {
            uid: {vid: key},
            ...
        }
        "node_properties": {
            "property_name": {
                "default": <value>,
                "dict": {
                    "uid": <property value>,
                    ...
                }
            },
            ...
        },
        "edge_properties": {
            "property_name": {
                "default": <value>,
                "dict": [{"edge": [uid, vid, key], "pvalue": <property value>} ...]
            },
            ...
        },
        "graph_properties": {
            "property_name": <value>,
            ...
        }
    }
}

Returns: (dict) Serialized graphical model.

states()¶

Defines the states component of the graphical model.

Returns: (list/tuple of JSONifiable object). List or tuple of states.

turn(state)[source]¶

Defines the player who controls the given state.

Parameters: state – (object) A valid state.
Returns: (int). In turn-based game, turn can be 1 for player 1 or 2 for player 2. In concurrent games, the turn must be 0.

Note

For concurrent games, the turn function can be left unimplemented.

win_cond()[source]¶: Winning condition of the game.

Solver¶

class ggsolver.models.Solver(graph, **kwargs)[source]¶

Represents a game solver that computes the winning regions and strategies for the players under a fixed solution concept.

Parameters: graph – (Graph or SubGraph instance) Graph or subgraph representing the game on a graph.

graph()[source]¶: Returns the input game graph.

is_solved()[source]¶: Returns if the game is solved or not.

reset()[source]¶: Resets the solver.

solution()[source]¶

Returns the solved game graph. The graph contains two special properties:

node_winner (node property): Maps each node to the id of player (1/2) who wins from that node.
edge_winner (edge property): Maps each edge to the id of player (1/2) who wins using that edge.

solve()[source]¶: Abstract method.

state2node(state)[source]¶: Helper function to get the node id associated with given state.

win_acts(state)[source]¶: Retuns the list of winning actions from the given state.

win_region(player)[source]¶: Returns the winning region for the player.

winner(state)[source]¶: Returns the player who wins from the given state.

DeterministicStrategy¶

class ggsolver.models.DeterministicStrategy(graph, player, losing_behavior=None, **kwargs)[source]¶

Represents a deterministic strategy. That is, the strategy at a given state always selects the same winning action.

Allows customization of losing behavior by specifying a function that maps a losing node to an action. By default, losing state is mapped to None.

__call__(state)[source]¶: Returns the action selected by strategy at given state.

NonDeterministicStrategy¶

class ggsolver.models.NonDeterministicStrategy(graph, player, losing_behavior=None, **kwargs)[source]¶

Represents a non-deterministic strategy. Uniformly samples an action from winning actions at that state.

Allows customization of losing behavior by specifying a function that maps a losing node to an action. By default, losing state is mapped to None.

__call__(state)[source]¶: Returns the action selected by strategy at given state.

Models¶

Automaton¶

TSys¶

Game¶

Solver¶

DeterministicStrategy¶

NonDeterministicStrategy¶

Page contents

Previous page

Next page

This Page