Transient reachability analysis¶
Content
The main features of pint relate to the transient reachability analysis, for which efficient over- and under-approximation have been designed.
The reachability properties are specfied in term of a goal. We first detail the different possible specifications for such a goal, and then illustrate various analyses of its reachability.
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()
Downloading ‘http://ginsim.org/sites/default/files/MAPK_large_19june2013.zginml’ to ‘gen/pintz1udn39lMAPK_large_19june2013.zginml’
Source file is in zginml format, importing with logicalmodel
Invoking GINsim…
Simplifying model…
25 state(s) have been registered: initState_11, initState_14, initState_12, initState_25, initState_23, initState_17, initState_6, initState_16, initState_4, initState_21, initState_13, initState_2, initState_9, initState_19, initState_1, initState_7, initState_3, initState_15, initState_10, initState_22, initState_18, initState_8, initState_24, initState_5, initState_20
[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")
Approximations are inconclusive, fallback to exact model-checking with its
[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
Source file is in Automata Network (an) format
This computation is an under-approximation: returned mutations are all valid, but they may be non-minimal, and some solutions may be missed.
Limiting solutions to mutations of at most 3 automata. Use maxsize
argument to change.
[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)
This computation is an under-approximation: returned cut-sets are all valid, but they may be non-minimal, and some cut-sets may be missed.
Limiting results to cut-sets with at most 3 elements. Use maxsize
argument to change.
[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)
This computation is an under-approximation: returned cut-sets are all valid, but they may be non-minimal, and some cut-sets may be missed.
Limiting results to cut-sets with at most 3 elements. Use maxsize
argument to change.
[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")
This computation is an under-approximation: returned transitions are all bifurcation transitions, but some may have been missed. Use method="exact"
for complete identification.
[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)
Source file is in Automata Network (an) format
[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 (seeGoal.__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 frominitial_state
False
if goal is not reachable frominitial_state
Inconc
if the static analysis is not conclusive and fallback isNone
.
-
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()
andlock()
.- 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()
anddisable()
.- 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 bifurcationtransitions (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")
See also
Model
Complete API