VERIFY  levchenko AGAINST
BEGIN  

// reachability of local (single-level) states 
// in Boolean semantics, any species is only in one state at each point of time

! EF( Raf * RafP );
! EF( MEK * MEKP * MEKPP );
! EF( ERK * ERKP * ERKPP );


// reachability of global (multi-level) states 

EF( ( RafP ) * ( MEKP + MEKPP ) );
EF( ( RafP ) * ( ERKP + ERKPP ) );
EF( ( MEKP + MEKPP ) * ( ERKP + ERKPP ) );
EF( ( RafP ) * ( MEKP + MEKPP ) * ( ERKP + ERKPP ) );


// there is no activation guarantee

! AF( RafP );
! AF( MEKPP );
! AF( ERKPP );


// cascades

!(( Raf * MEK * ERK ) -> E( ! ( RafP ) U MEKP ));
!(( Raf * MEK * ERK ) -> E( ! ( MEKP ) U MEKPP ));
!(( Raf * MEK * ERK ) -> E( ! ( MEKPP ) U ERKP ));
!(( Raf * MEK * ERK ) -> E( ! ( ERKP ) U ERKPP ));


// property (Q1)
// The signal sequence predicted by the partial order run of the i/o T-invariant 
// is the only possible one. In other words, starting at the initial state,
// it is necessary to pass through states RafP, MEKP, MEKPP and ERKP in order to
// reach ERKPP.

!(E ( ! RafP  U MEKP ) + E ( ! MEKP U MEKPP ) +
  E ( ! MEKPP U ERKP ) + E ( ! ERKP U ERKPP )   )

// to weak, not sensitive to bridging transitions, e.g. from ERK to ERKPP 

!(E ( ! RafP  U MEKP ) * E ( ! MEKP U MEKPP ) *
  E ( ! MEKPP U ERKP ) * E ( ! ERKP U ERKPP )   )


// property (Q2)
// Dephosphorylation takes place independently. 
// E.g., the duration of the phosphorylated state of ERK is independent of 
// the duration of the phosphorylated states of MEK and Raf.

EF ( Raf * ( ERKP + ERKPP ) ) * EF ( RafP * ( ERKP + ERKPP ) ) * 
EF ( MEK * ( ERKP + ERKPP ) ) * EF ( ( MEKP + MEKPP ) * ( ERKP + ERKPP ) );


// property (3)
// A cyclic behaviour w.r.t. the presence/absence of a specie is possible forever

AG( ( RafP -> EF( ! RafP ) ) * ( ! RafP -> EF( RafP ) ) );
AG( ( MEK -> EF( ! MEK ) ) * ( ! MEK -> EF( MEK ) ) );
AG( ( ERK -> EF( ! ERK ) ) * ( ! ERK -> EF( ERK ) ) );
AG( ( MEKPP -> EF( ! MEKPP ) ) * ( ! MEKPP -> EF( MEKPP ) ) );

END.