Validation of biological models with temporal logic and Timed Hybrid Petri Nets.

Autor: Troncale S, Comet JP, Bernot G
Jazyk: angličtina
Zdroj: Annual International Conference of the IEEE Engineering in Medicine and Biology Society. IEEE Engineering in Medicine and Biology Society. Annual International Conference [Annu Int Conf IEEE Eng Med Biol Soc] 2007; Vol. 2007, pp. 4603-8.
DOI: 10.1109/IEMBS.2007.4353365
Abstrakt: The Hybrid Functional Petri Nets (HFPN) formalism has shown its convenience for modelling biological systems. This class of models has been fruitfully applied in biology but the remarkable expressiveness of HFPN often leads to incomplete validations. In this paper, we propose a logical framework for Timed Hybrid Petri Nets (THPN), a sub-class of HFPN. We propose an extension of Event Clock Logic dedicated to THPN and a procedure to convert a THPN into a real-time automaton. A small biological model shows that our framework allows us to formally prove properties by a well suited model-checking procedure.
Databáze: MEDLINE