270 J. Zhou et al.
Table 1.Basic templatesNo. Template Description
1 p 1 ∧F≤t^1 G≤t^2 p 2
wherep 1 :( 1 ≤x≤u 1 )
p 2 :( 2 ≤x≤u 2 )Starting from the levelp 1 ,withint 1
steps, the value ofxreaches the level
p 2 and stays there for at leastt 2 steps.
Typically describes sustained
activations or deactivations.
Constraints can be used to specify
whetherxdecreases or increases from
the initial level
2 p 1 ∧F≤t^1 (p 2 ∧F≤t^2 p 3 )
wherep 1 :( 1 ≤x≤u 1 )
p 2 :( 2 ≤x≤u 2 )
p 3 :( 3 ≤x≤u 3 )Starting from an initial levelp 1 ,the
value ofxreaches the levelp 2 within
t 1 steps. Then, fromp 2 ,xreaches a
levelp 3 withint 2 steps. Formulates
evolution of species concentration
from an initial level to a new level and
then further to another new level or
back to the initial level
3 p 1 ∧F≤t^1 (p 2 ∧F≤t^2 G≤t^3 p 3 )
wherep 1 :( 1 ≤x≤u 1 )
p 2 :( 2 ≤x≤u 2 )
p 3 :( 3 ≤x≤u 3 )Similar to Template 2, the value ofx
starts from the levelp 1 , reaches the
levelp 2 withint 1 steps. Then within
the nextt 2 steps, reaches a levelp 3
and stays inp 3 for at leastt 3 steps.
Characterizes transient or sustained
activations, can be extended to
formulate bistability
4 p 1 ∧F≤t^1 (p 2 ∧F≤t^2 (p 3 ∧F≤t^1 (p 4 )))
wherep 1 :( 1 ≤x≤u 1 )
p 2 :( 2 ≤x≤u 2 )
p 3 :( 3 ≤x≤u 3 )
p 4 :( 4 ≤x≤u 4 )Starting from an initial levelp 1 ,the
value ofxreaches the levelp 2 where
(u 1 < 2 )withint 1 steps. Then, from
p 2 ,xreaches a levelp 3 ,(u 3 < 2 )
withint 2 steps. Further fromp 3 ,x
reaches a levelp 4 where (u 3 < 4 ).
Imposing constraints [u 1 < 2 ]∧[u 1 <
4 ]∧[u 3 < 2 ]∧[u 3 < 4 ] characterizes
oscillationsclassifies a set of random trajectories generated by a model as belonging to one
of the templates and then proceeds to synthesize a concrete property using the
template.
3.1 Data Preprocessing
The evolution of a variablexis mainly reflected by changes in its value over
time. We first transform the trajectories by evaluating the change inxat each
time point, and computing the normalizedΔx(t) data over time as indicated by