Abstract
Temporal logics and model-checking techniques have proved successful to respectively express biological properties of complex biochemical systems, and automatically verify their satisfaction in both qualitative and quantitative models. In this paper, we propose a finite time horizon model-checking algorithm for the existential fragment of LTL with numerical constraints over the reals, with the ability to compute the range of values of the real variables occurring in a formula that makes it true in a model. We illustrate this approach for the analysis of biological data time series, provide a set of biologically relevant patterns of formulas, and evaluate them on models of the cell cycle control and MAPK signal transduction.

URL:
http://rewerse.net/publications/rewerse-publications.html#REWERSE-RP-2007-107

BibTeX:

@inproceedings{REWERSE-RP-2007-107,
	author = {Fran\c{c}ois Fages and Aur\'{e}lien Rizk},
	title = {On the Analysis of Numerical Data Time Series in Temporal Logic},
	booktitle = {Proceedings of Computational Methods in Systems Biology 2007, Edinburgh, UK (20th--21st September 2007)},
	year = {2007},
	volume = {4695},
	series = {LNCS},
	pages = {48--63},
	url = {http://rewerse.net/publications/rewerse-publications.html#REWERSE-RP-2007-107}
}