Skip to main navigation Skip to search Skip to main content

Model checking biological systems described using ambient calculus

  • Radu Mardare
  • , Corrado Priami
  • , Paola Quaglia
  • , Oleksandr Vagin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.
Original languageEnglish
Title of host publicationComputational Methods in Systems Biology. CMSB 2004
EditorsV. Danos, V. Schachter
Pages85-103
Number of pages19
Volume3082
ISBN (Electronic)978-3-540-25974-9
DOIs
Publication statusPublished - 2005

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
ISSN (Print)0302-9743

Keywords

  • model checking analysis
  • biological systems
  • ambient calculus
  • labeled syntax trees
  • Kripke structure
  • propositional branching temporal logic
  • accessibility relation between states
  • temporal logics

Fingerprint

Dive into the research topics of 'Model checking biological systems described using ambient calculus'. Together they form a unique fingerprint.

Cite this