High-level modeling and verification of cellular signaling

We use computational modeling and formal analysis techniques to study temporal behavior of a discrete logical model of the naïve T cell differentiation. The model is analyzed formally and automatically by performing temporal logic queries via statistical model checking. While the model can be verified and then further explored using Monte Carlo simulations, model checking allows for much more efficient analysis by testing a large set of system properties, with much smaller runtime than the one required by simulations. The results obtained using model checking provide details about relative timing of events in the system, which would otherwise be very cumbersome and time consuming to obtain through simulations only. We efficiently test a large number of properties, and confirm or reject hypotheses that were drawn from previous analysis of experimental and simulation data.