Class FiniteTransitionSystem

Kripke structure with labeled states and edges.

Who controls the state

To define who "moves the token" between vertices in the graph, set the attribute:

>>> g = FiniteTransitionSystem()
>>> g.owner = 'sys'

This means that when there are more than one transition enabled, then the system picks the next state.

The other option is:

>>> g.owner = 'env'

so the environment picks the next state.

State labeling

The state labels are sets of atomic propositions, similar to a KripkeStructure.

In principle some of the propositions that label states could be controlled by either of the players, but this would lead to less straightforward semantics.

You can achieve the same effect by using actions of the opponent.

It is a matter of future experimentation whether this capability will be introduced, by partitioning the props into env_props and sys_props (similar to env_vars, sys_vars in GRSpec).

Edge labeling

Edge labels are called "actions".

The edge labeling is syntactic sugar for labels that are shifted to the target states of those edges. So edge labeling is not an essential difference from Kripke structures.

Not to be confused with the term: "Labeled Transition System" found in the literature.

Also, it differs from the definition in Baier-Katoen in that actions are not mere reading aid, but are interpreted as propositions as explained above.

Besides, edge labeling usually allows for graphs with fewer vertices than the corresponding Kripke structure.

Open vs Closed

The essential difference from Kripke structures is the partition of atomic propositions into input/output sets.

If the set of inputs is empty, then the system is closed. Otherwise it is an open system. Open systems have an environment, closed don't.

Alternatively, FTS can be thought of as a shorthand for defining a vertex-labeled game graph, or equivalently a game structure.

System and environment actions

The only significant difference is in transition labeling. For closed systems, each transition is labeled with a system action. So each transition label comprises of a single sublabel, the system action.

For open systems, each transition is labeled with 2 sublabels:

• The first sublabel is a system action,
• the second an environment action.

Mutual exclusion of actions

Constraints on actions can be defined similarly to FTS actions by setting the fields:

• ofts.env_actions_must
• ofts.sys_actions_must

The default constraint is 'xor'.

sys.sys_actions_must: select constraint on actions. Options:

• 'mutex': at most 1 action True each time
• 'xor': exactly 1 action True each time
• 'none': no constraint on action values

The xor constraint can prevent the environment from blocking the system by setting all its actions to False.

The action are taken when traversing an edge. Each edge is annotated by a single action. If an edge (s1, s2) can be taken on two transitions, then 2 copies of that same edge are stored. Each copy is annotated using a different action, the actions must belong to the same action set. That action set is defined as a set instance. This description is a (closed) FTS.

The system and environment actions are associated with an edge of a reactive system. To store these, mutliple labels are used and their sets are encapsulated within the same FTS.

Example

In the following None represents the empty set, subset of AP. First create an empty transition system and add some states to it:

>>> from tulip import transys as trs
>>> ts = trs.FiniteTransitionSystem()
>>> ts.states.add('s0')
>>> ts.states.add_from(['s1', 's3', 'end', 5] )

Set an initial state, which must already be in states:

>>> ts.states.initial.add('s0')

There can be more than one possible initial states:

>>> ts.states.initial.add_from(['s0', 's3'] )

To label the states, we need at least one atomic proposition, here 'p':

>>> ts.atomic_propositions |= ['p', None]
>>> ts.states.add('s0', ap={'p'})
>>> ts.states.add_from([('s1', {'ap':{'p'} }),
                        ('s3', {'ap':{} } )])

If a state has already been added, its label of atomic propositions can be defined directly:

>>> ts.states['s0']['ap'] = {'p'}

Having added states, we can also add some labeled transitions:

>>> ts.actions |= ['think', 'write']
>>> ts.transitions.add('s0', 's1', actions='think')
>>> ts.transitions.add('s1', 5, actions='write')

Note that an unlabeled transition:

>>> ts.transitions.add('s0', 's3')

is considered as different from a labeled one and to avoid unintended duplication, after adding an unlabeled transition, any attempt to add a labeled transition between the same states will raise an exception, unless the unlabeled transition is removed before adding the labeled transition.

The user can still invoke NetworkX functions to set custom node and edge labels, in addition to the above ones. For example:

>>> ts.states.add('s0')
>>> ts.node['s0']['my_cost'] = 5

The difference is that atomic proposition and action labels are checked to make sure they are elements of the system's AP and Action sets.

It is not advisable to use MultiDiGraph.add_node and MultiDiGraph.add_edge directly, because that can result in an inconsistent system, since it skips all checks performed by transys.

Note

The attributes atomic_propositions and aps are equal. When you want to produce readable code, use atomic_propositions. Otherwise, aps offers shorthand access to the APs.

Reference

For closed systems this corresponds to Def. 2.1, p.20 [BK08]:

• states (instance of States) = S
• states.initial = S_0 \subseteq S
• atomic_propositions = AP
• actions = Act
• transitions (instance of Transitions):

       the transition relation ->
         = edge set + edge labeling function
         (labels \in actions)
  

  Unlabeled edges are defined using:

  • sys.transitions.add
  • sys.transitions.add_from
  • sys.transitions.add_adj

  and accessed using:

  • sys.transitions.find
• the state labeling function:

         L: S-> 2^AP
  

  can be defined using:

  • sys.states.add
  • sys.states.add_from

  and accessed using methods:

  • sys.states(data=True)
  • sys.states.find

See Also

KripkeStructure, tuple2fts, line_labeled_with, cycle_labeled_with

Return the graph name.

Returns
-------
name : string
    The name of the graph.

Examples
--------
>>> G = nx.Graph(name='foo')
>>> str(G)
'foo'