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 prepositional 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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Mardare, R., Priami, C., Quaglia, P., & Vagin, O. (2005). Model checking biological systems described using ambient calculus. In Lecture Notes in Bioinformatics (Subseries of Lecture Notes in Computer Science) (Vol. 3082, pp. 85–103). Springer Verlag. https://doi.org/10.1007/978-3-540-25974-9_8
Mendeley helps you to discover research relevant for your work.