Temporal Logic Modeling of Dynamical Behaviors: First-Order Patterns and Solvers

This chapter describes how quantitative temporal logic formulas can be used to formalize imprecise dynamical behaviors of biological systems, and how such a formal specification of experimental observations can be used to calibrate models to real data, in a more versatile way than with curve fitting algorithms. It presents useful patterns of first-order temporal logic formulas to facilitate their use by the modelers, present efficient solvers dedicated to them, and illustrate their use to build a coupled model of the cell cycle and the circadian molecular clock with period and phase constraints. The chapter considers finite traces obtained either by biological experiments in the case of real data, or by numerical integration in the case of simulated data over a finite time horizon. To give meaning to LTL formulas, a finite trace is thus complemented in an infinite trace by adding a loop on the last state.