We propose a way of performing model checking analysis for biological systems. The technics were developed for a CTL* logic built upon Ambient Calculus. We introduce labeled syntax trees for ambient processes and use them as possible worlds in a Kripke structure developed for a propositional branching temporal logic. The accessibility relation over labeled syntax trees is generated by the reduction over corresponding Ambient Calculus processes. Providing the algorithms for calculating the accessibility relation between states, we open the perspective of using model checking algorithms developed for temporal logics in analyzing any phenomena described in Ambient Calculus.
Titolo: | Model Checking Biological Systems Described Using Ambient Calculus |
Autori: | R., Mardare; Priami, Corrado; Quaglia, Paola; Vagin, Oleksandr |
Autori Unitn: | |
Titolo del volume contenente il saggio: | Computational Methods in Systems Biology: International Conference CMSB 2004, Paris, France, May 26-28, 2004, Revised Selected Papers |
Luogo di edizione: | Berlin |
Casa editrice: | Springer |
Anno di pubblicazione: | 2005 |
ISBN: | 9783540253754 |
Handle: | http://hdl.handle.net/11572/94796 |
Appare nelle tipologie: | 02.1 Saggio su volume miscellaneo o Capitolo di libro (Essay or Book Chapter) |