Goal specification¶

In its simplest form, a goal is the local state of one automaton, for instance g=1. The goal is reached as soon as a state where g=1 is reached. Note that there is no assumption on the stability of this state, this is why we refer to the transient reachability analysis.

Besides the single local state, a goal can be * a (sub-)state, specified either as by a dict-like object or string representation of the (sub)-state * a sequence of (sub-)state: for instance a Goal("a=1","b=1") is reached if one can reach a state where a=1 and from which can be reached a state where b=1 * a disjunction of goals: Goal("a=1")|Goal("c=1") is reached if one can reach a state where either a=1 or c=1.

In general, a goal is instanciated using the class Goal.

[2]:

from pypint import Goal # avoid typing pypint
simple = Goal("g=1")    # simple goal
simple = Goal(g=1) # equivalent notation
substate = Goal({"a": 1, "b": 1})   # reach a state where both a=1 and b=1
seq = Goal({"a": 1, "b": 1}, {"c": 1}) # reach a state where a=1 and b=1 and from c=1 is reachable
seq = Goal("a=1,b=1", "c=1") # equivalent to above
alt = Goal("a=1", "b=1") | Goal("c=1") # either reach a state where a=1 and then a state where b=1,
                                       # or reach a state where c=1

Note that if the goal consists of a single argument (such as a simple local state), there is no need to explicitly instanciates this class: method(Goal("g=1")) is equivalent to method("g=1").

Static reachability analysis¶

Verifying reachability properties in automata networks is a PSPACE-complete problem, and is therefore hardly tractable for large systems. Pint implements a static analysis for the formal approximaton of reachability properties with a lower complexity. It consists in both over- and under-approximations, i.e., the verification of necessary or sufficient conditions. As evaluated in [Paulevé et al in MSCS 2012; Folschette et al in TCS 2015; Paulevé et al in LMBS 2014], such an analysis can be tractable on networks with several hundreds of nodes.

Let us load a medium-size model:

[3]:

mapk = pypint.load("http://ginsim.org/sites/default/files/MAPK_large_19june2013.zginml")
mapk.summary()

[3]:

{'max_local_states': 2,
 'nb_automata': 53,
 'nb_local_states': 106,
 'nb_states': 9007199254740992,
 'nb_transitions': 177}

The reachability() method takes as main argument the goal. It returns either True or False depending if the goal is reachable or not from the model initial state.

[4]:

mapk.having("initState_1").reachability("Proliferation=1")

[4]:

True

By default, if the static analysis is not conclusive (i.e., the necessary condition is satisified, but the sufficient condition is not), pint falls back to exact model checking with ITS. The model-checker can be modified with the fallback argument (see reachability() documentation).

[5]:

mapk.having("initState_10").reachability("Proliferation=1")

[5]:

True

[6]:

mapk.having("initState_10").reachability("Proliferation=1", fallback=None)

[6]:

pypint.types.Inconc

Finally, the static analysis can be bypassed by specifying the tool argument to the desired model-checker.

[ ]:

mapk.having("initState_1").reachability("Proliferation=1", tool="nusmv")

It is worth noting that prior to any model-checking verification, the model is first reduced using the goal-oriented model reduction to enhance the tractability of the analysis.

Identification of mutations to control goal reachability¶

One of the prime application of reachability analysis is the identification of perturbations which would control the goal reachability.

Pint offers an efficient static analysis which identify mutations for preventing a goal to occur. The analysis aims at being tractable on networks with hundreds of nodes.

The method oneshot_mutations_for_cut() takes as main argument the goal and returns a list of mutations which makes it impossible to reach.

In the following example, we compute the mutations which prevent both the activation of Apoptosis and CellCycleArrest. A mutation can be tested with the lock() method which blocks the specfied automata to the given local states. It is guaranteed that the reachability returns false. We test it here with the 7-th returned mutations, i.e., {'AKT2': 1, 'ERK': 1, 'p63': 1}.

[7]:

wt = pypint.load("models/invasion_pathways.an")
wt.initial_state["ECMicroenv"] = 1
goal = Goal("Apoptosis=1") | Goal("CellCycleArrest=1")
mutations = wt.oneshot_mutations_for_cut(goal, maxsize=3, exclude={"ECMicroenv"})
mutations

[7]:

[{'AKT1': 1},
 {'CDH1': 1, 'NICD': 0},
 {'CDH2': 1, 'NICD': 0},
 {'CTNNB1': 0, 'NICD': 0},
 {'DKK1': 1, 'NICD': 0},
 {'AKT2': 1, 'ERK': 1, 'ZEB2': 0},
 {'AKT2': 1, 'ERK': 1, 'p63': 1},
 {'AKT2': 1, 'ZEB2': 0, 'p21': 0},
 {'ERK': 1, 'SNAI1': 1, 'ZEB2': 0},
 {'ERK': 1, 'SNAI2': 1, 'ZEB2': 0},
 {'ERK': 1, 'SNAI2': 1, 'p63': 1},
 {'ERK': 1, 'ZEB1': 1, 'ZEB2': 0},
 {'ERK': 1, 'ZEB1': 1, 'p53': 1},
 {'ERK': 1, 'ZEB1': 1, 'p63': 1},
 {'ERK': 1, 'ZEB2': 0, 'p53': 0},
 {'ERK': 1, 'miR200': 0, 'p63': 1},
 {'NICD': 0, 'SNAI2': 1, 'TWIST1': 0},
 {'NICD': 0, 'TWIST1': 0, 'p53': 0},
 {'SNAI2': 1, 'ZEB2': 0, 'p21': 0},
 {'ZEB2': 0, 'p21': 0, 'p53': 0}]

[8]:

wt.lock(mutations[6]).reachability(goal)

[8]:

False

Cut sets of paths to goal¶

Cut sets are sets of local states of automata which cover all the paths (or traces) from the initial state to any state where the goal is present. Therefore, disabling the local states of a cut set removes (cuts) all the paths to the goal, making it impossible to reach.

The method is fully detailed in [Paulevé et al at CAV 2013]. It is tractable on very networks, up to several thousands of automata.

The call of the method cutsets() is similar to oneshot_mutations_for_cut(). It returns a list of cut sets of all the paths to the given goal:

[9]:

wt.cutsets("Apoptosis=1",maxsize=3)

[9]:

[{'p53': 1}, {'CTNNB1': 1, 'NICD': 1}]

A cut set can be applied using the disable() method which removes all the transitions which involve the given local states. The reachability of the goal is guaranteed to be impossible:

[10]:

wt.disable(p53=1).reachability("Apoptosis=1")

[10]:

False

Remark that the semantics of a cut set is different than the one of a mutation: a mutation specifies the state in which an automaton should be enforced (gain/loss of function), whereas a cut set specifies which states should be avoided. Therefore, the cut set {'CTNNB1': 1, 'NICD': 1} can be implemented as a mutation by enforcing CTNNB1 and NICD to 0. However, to be correct, this latter reasonning assumes that the initial state is not changed by the mutation, i.e. CTNNB1 and NICD should be 0 in the initial state. The mutation then prevent any value change which will prevent the goal reachability.

By default, the returned cut sets do not involve initial local state, so one can implement them as mutations safely. A more complete set of cut sets can be returned by explicitely allowing initial local states:

[11]:

wt.cutsets("Apoptosis=1",maxsize=3,exclude_initial_state=False)

[11]:

[{'AKT1': 0},
 {'AKT2': 0},
 {'DNAdamage': 0},
 {'ERK': 0},
 {'SNAI2': 0},
 {'ZEB2': 0},
 {'miR200': 0},
 {'miR34': 0},
 {'p53': 0},
 {'p53': 1},
 {'p63': 0},
 {'p73': 0},
 {'CDH1': 0, 'CTNNB1': 0},
 {'CDH1': 0, 'ECMicroenv': 1},
 {'CDH1': 0, 'NICD': 1},
 {'CDH2': 0, 'CTNNB1': 0},
 {'CDH2': 0, 'ECMicroenv': 1},
 {'CDH2': 0, 'NICD': 1},
 {'CTNNB1': [0, 1]},
 {'CTNNB1': 0, 'DKK1': 0},
 {'CTNNB1': 1, 'ECMicroenv': 1},
 {'CTNNB1': 1, 'NICD': 1},
 {'DKK1': 0, 'ECMicroenv': 1},
 {'DKK1': 0, 'NICD': 1}]

This last example also shows that a cut set can contain several, if not all, local states of a same automaton: {'CTNNB1': [0, 1]} means that all the paths to the Apoptosis activation use, at some point, either the inactive or active form of CTNNB1. Hence disabling all the transitions triggered by CTNNB1 will break all the possible ways to Apoptosis.

Identification of bifurcation transitions¶

Given an initial state and a goal, a bifurcation transitions is a transition after which the goal is no longer reachable. Bifurcation transitions are local transitions of the automata network that are triggered in the transient dynamics. See [Fitime et al at WCB 2016] for more information.

Bifurcation transitions are helpful to understand differentiation processes, as they give the decisive modification which removed the capability to reach the goal.

The method bifurcations() takes as first argument the goal for which the bifurcation transitions will be identified. It returns a list of LocalTransition objects.

The method may be tractable on networks with several hundreds of nodes.

[12]:

wt.bifurcations("Apoptosis=1")

[12]:

["AKT2" 0 -> 1 when "TWIST1"=1 and "GF"=0 and "CDH2"=0 and "p53"=0 and "miR203"=0 and "miR34"=0 and "TGFbeta"=0 and "NICD"=1,
 "AKT2" 0 -> 1 when "TWIST1"=1 and "GF"=0 and "miR34"=0 and "TGFbeta"=1 and "p53"=0 and "miR203"=0,
 "SNAI2" 0 -> 1 when "TWIST1"=0 and "NICD"=1 and "miR200"=0 and "p53"=0 and "CTNNB1"=0 and "miR203"=0,
 "SNAI2" 0 -> 1 when "p53"=0 and "miR200"=0 and "TWIST1"=1 and "miR203"=0,
 "SNAI2" 0 -> 1 when "p53"=0 and "miR203"=0 and "miR200"=0 and "TWIST1"=0 and "CTNNB1"=1,
 "AKT2" 0 -> 1 when "CDH2"=1 and "TWIST1"=1 and "GF"=0 and "miR34"=0 and "TGFbeta"=0 and "p53"=0 and "miR203"=0,
 "AKT2" 0 -> 1 when "p53"=0 and "miR203"=0 and "miR34"=0 and "TWIST1"=1 and "GF"=1]

For each of the returned local transitions, there exists a state reachable from the initial state which (1) can reach the goal; and (2) after applying the bifurcation transition, the goal is no longer reachable.

This method also allows a method="exact" keyword for the complete identification of bifurcation transitions using model-checking. It is however not tractable on large networks.

Goal-oriented model reduction¶

Pint can statically detect part of transitions that do not take part in minimal paths to the goal reachability. A path is minimal if and only it contains no cycle and all the transitions are causally related.

These transitions can then be removed from the model while preserving all the minimal paths to the goal and potentially reducing the reachable state graph significantly.

The following command loads a model of 53 automata and 173 local transitions. The reduction for reachability of active Apoptosis from the state where DNA_damage is on leads to an automata network with only 69 local transitions. In this case, the model-checking with NuSMV is tractable only with the reduced model.

[13]:

mapk53 = pypint.load("models/mapk53.an")
len(mapk53.automata), len(mapk53.local_transitions)

[13]:

(53, 173)

[14]:

red = mapk53.having(DNA_damage=1).reduce_for_goal(Apoptosis=1)
red.save_as("gen/mapk53-apoptosis.smv")  # export for later NuSMV model checking
len(red.local_transitions)

[14]:

69

By default, reduce_for_goal() also removes unused automata and local states. To prevent this behaviour, add the parameter squeeze=False.

Note that the method reachability() automatically performs the model reduction before calling the fallback model-checker. Therefore, this method is mainly used prior to an export for an external analysis, for instance with NuSMV or with mole.

Related functions and classes¶

class Goal(*args, **kwargs)

Object which represents reachability goal used in most of Pint commands.

In its simplest form, a goal is the local state of an automaton. A goal can also be a sequence of sub-states.

It can be instanciated either with arguments or keywords (but not both). If instanciated with arguments, each argument specifies a sub-state, and the goal is the sequence of these sub-states. A sub-state can be specified either by a string (in pint format), or by a dict-like object. If instanciated with keywords, the goal is a single sub-state where the keys correspond to the automata and the values their local states.

Finally, alternative goals can be constructed using the operator | on the instanciated individual goals (see Goal.__or__()).

Examples:

>>> Goal(a=1)          # simple goal
>>> Goal((a,1))        # equivalent to above
>>> Goal("a=1")        # equivalent to above
>>> Goal(a=1,b=1)      # single sub-state goal
>>> Goal("a=1,b=1")    # equivalent to above
>>> Goal("a=1", "b=1") # sequence of simple goals
>>> Goal({"a": 1, "b": 1}, {"a": 0})    # sequence of sub-state goals
>>> Goal(a=1) | Goal(b=1)  # alternative goals

Model.reachability(goal=None, fallback=’its’, tool=’sa’, sa_args=[], reduce_for_goal=True, timeout=None, **kwgoal)

Check if goal is reachable from the initial state. At first, Pint tries static analysis for the verification. If non-conclusive, it can fallback to exact model-checking.

Parameters

• goal (str or list(str) or Goal) – goal specification (e.g., "a=1")

• kwgoal – keywords for goal specification (instead of goal argument)

• fallback (str) – fallback to exact model-checking if static analysis is not conclusive. Supported model-checkers are: "its", "nusmv", and "mole".

• tool (str) – tool for the model-checking: * "sa": static analysis with potential fallback method if not conclusive * "its", "nusmv", "mole": directly use the specified model-checker.

• sa_args (list(str)) – additional arguments for static analysis

• reduce_for_goal (bool) – before invoking a model-checker, perform the goal-oriented reduction of the automata network

• timeout (int) – command timeout in seconds

Returns

• True if goal is reachable from initial_state

• False if goal is not reachable from initial_state

• Inconc if the static analysis is not conclusive and fallback is None.

Model.oneshot_mutations_for_cut(goal=None, maxsize=5, exclude=[], exclude_goal_automata=True, timeout=None, **kwgoal)

Computes sets of local states for which the locking in the initial state ensures that goal is impossible to reach.

Elements of the returned lists can be notably used as argument for methods Model.having() and lock().

Parameters

• goal (str or list(str) or Goal) – goal specification (e.g., "a=1")

• kwgoal – keywords for goal specification (instead of goal argument)

• maxsize (int) – maximal cardinality of returned sets.

• exclude (set(str)) – set/list of automata to exclude from the solutions

• exclude_goal_automata (bool) – exclude automata involved in the goal specification

• timeout (int) – command timeout in seconds

Return type

list(dict[str,int])

Model.lock(substate={}, **kwstate)

Returns the AN where the specified automata are lock to the given local state. The initial state is modified accordingly.

Parameters

• substate (list(tuple(str,int)) or dict[str,int]) – local states to lock.

• kwstate – complementary specification of local states.

Returns

a new FileModel instance for the modified AN.

Model.cutsets(goal=None, maxsize=5, exclude=[], exclude_initial_state=False, exclude_goal_automata=True, timeout=None, **kwgoal)

Computes sets of local states which are used in all the paths from the initial state to goal: if all the local states in a cut-set are disabled (all related local transitions are removed), then it is impossible to reach goal from the initial state.

Elements of the returned lists can be notably used as argument for methods Model.having() and disable().

Parameters

• goal (str or list(str) or Goal) – goal specification (e.g., "a=1")

• kwgoal – keywords for goal specification (instead of goal argument)

• maxsize (int) – maximal cardinality of a cut-set.

• exclude (set(str)) – set/list of automata to exclude from the solutions

• exclude_initial_state (bool) – if True, cut-sets can not be composed of initial local states.

• exclude_goal_automata (bool) – exclude automata involved in the goal specification

• timeout (int) – command timeout in seconds

Return type

list(dict[str,int or int list])

See also

method oneshot_mutations_for_cut()

Model.disable(local_states=[], **kwstate)

Returns the AN where all local transitions involving specified local states have been removed.

Parameters

• local_states (list(tuple(str,int)) or dict[str,int]) – local states to disable.

• kwstate – complementary specification of local states.

Returns

a new FileModel instance for the modified AN.

Model.bifurcations(goal=None, method=’ua’, timeout=None, **kwgoal)

Identify local transitions after which, in some state, goal is no longer reachable.

Parameters

• goal (str or list(str) or Goal) – goal specification (e.g., "a=1")

• kwgoal – keywords for goal specification (instead of goal argument)

• method (str) –

  • "exact", "nusmv", or "its" for complete identification of bifurcation

    transitions (PSPACE); "exact" is an alias for "nusmv".

  • "ua+mole" for under-approximation relying on exact the reachable states set prior computation (NP+PSPACE)

  • "ua" for under-approximation of bifurcation transitions (NP)

• timeout (int) – command timeout in seconds

Return type

LocalTransition list

Model.reduce_for_goal(goal=None, squeeze=True, squeeze_preserve=None, **kwgoal)

Compute the goal-oriented reduction of the automata network. The reduction removes local transitions that are guaranteed to never contribute to any minimal path from the initial state to the goal (a path is minimal if there exists no paths using a strict subset of transitions leading to the goal).

The reduced models preserves existential reachability properties, as well as cut sets.

The complexity of the method is polynomial in the number of local transitions and automata, and exponential in the size of the largest automata minus 1.

Parameters

• goal (str or list(str) or Goal) – goal specification (e.g., "a=1")

• kwgoal – keywords for goal specification (instead of goal argument)

• squeeze (bool) – if True (default), unused automata and local states are removed. Warning: this can lead to local state renaming.

• list squeeze_preserve (str) – do not squeeze the given automata

Returns

a new FileModel instance for the reduced automata network.

Example:

>>> redm = m.reduce_for_goal("g=1")