Computational Methods in Systems Biology

PINT: A Static Analyzer for Transient Dynamics of Qualitative Networks 313

Table 1. Benchmark† of goal reachability verification with two exact methods
(NuSMVandITS-reach)andPint, before (normal font) and after (bold font) goal-
oriented model reduction;|T|is the number of local transitions in automata networks;
|state|is the number of reachable global states, when computable. KO indicates an
out-of-memory/time computation. In all casesPintis conclusive.

Verification of goal reachability

Model (|nodes|) |T| |states| NuSMV(EFg) ITS-reach Pint

TCell-d (101) [ 1 ] 381 ≈ 2. 4 · 108 2s 40Mb 0.5 s 26 Mb 0.02 s

profile 1 0 1

TCell-d (101) 381 KO KO 960 s 1.6 Gb 4.5 s

profile 2 221 75,947,684 470 s 270 Mb 15 s 160 Mb

RBE2F (370) [ 22 ] 742 KO KO KO 0.2 s

56 2,350,494 3s 37Mb 4s 13Mb

MAPK (309) [ 24 ] 1251 KO KO KO 48 s

429 KO KO KO

Scripts and models available athttp://loicpauleve.name/pint-benchmarks.tbz2

Table 2.Performance†of cut sets and mutations under-approximations withPint
depending on the maximal cardinality of returned sets.

Goal TCell-d (101) Egf-r (104) [ 23 ] MAPK (309) PID (10,229) [ 20 ]

FOXP3=1 AP1=1 ERK-PP=1 SNAIL=1

3-cut sets 0.06 s 35 0.02 s 34 0.06 s 24 1.2 s 7

4-cut sets 0.10 s 101 0.02 s 34 0.1 s 48 5s 37

6-cut sets 0.60 s 495 0.03 s 34 1s 60 10 m 907

3-mutations 0.30 s 15 0.30 s 20 5s 222 50 m 7

4-mutations 0.30 s 15 0.30 s 22 10 s 1896 50 m 67

6-mutations 0.30 s 15 0.30 s 22 KO 50 m 367

Scripts and models available athttp://loicpauleve.name/pint-benchmarks.tbz2

Table 3.Performance† (Scripts and models available athttp://loicpauleve.name/
pint-benchmarks.tbz2) of exact and approximatedidentification of bifurcation transi-
tionswithNuSMVandPint, respectively;|tb|is the number of identified bifurcation
transitions.

|T| |states| goal NuSMV Pint

|tb| time |tb| time

EGF/TNF (28) [ 17 ] 53 3968 NFkB = 0 5 0.2 s 2 0.1 s

MAPK (53) [ 11 ] 173 KO Proliferation = 1 KO 13 40 s

TCell-d (101) 381 KO FOXP3 = 1 KO 4 58 s

Scripts and models available athttp://loicpauleve.name/pint-benchmarks.tbz2