Algorithmic algebraic model checking II: Decidability of semi-algebraic model checking and its applications to systems biology

V. Mysore, C. Piazza, B. Mishra

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

Abstract

Motivated by applications to systems biology, and the emergence of semi-algebraic hybrid systems as a natural framework for modeling biochemical networks, we continue exploring the decidability problem for model-checking with TCTL (Timed Computation Tree Logic) over this broad class of semi-algebraic hybrid systems. Previously, we had introduced these models, demonstrated the close connection to the goals of systems biology. However, we had only developed the techniques for bounded reachability, arguing for the adequacy of such an approach in a majority of the biological applications. Here, we present a semi-decidable symbolic algebraic dense-time TCTL model checking algorithm, which satisfies two desirable properties: it can be derived automatically from the symbolic description, and it extends to and generalises other versions of temporal logics. The main mathematical device at the core of this approach is Tarski-Collins' real quantifier elimination employed at each fixpoint iteration, whose high complexity is the crux of its unfortunate limitation. Along with these results, we prove the undecidability of this problem in the more powerful "real" Turing machine formalism of Blum, Shub and Smale. We then demonstrate a preliminary version of our model-checker Tolque on the Delta-Notch example.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages217-233
Number of pages17
DOIs
StatePublished - 2005
EventThird International Symposium on Automated Technology for Verification and Analysis, ATVA 2005 - Taipei, Taiwan, Province of China
Duration: Oct 4 2005Oct 7 2005

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3707 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

OtherThird International Symposium on Automated Technology for Verification and Analysis, ATVA 2005
CountryTaiwan, Province of China
CityTaipei
Period10/4/0510/7/05

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Algorithmic algebraic model checking II: Decidability of semi-algebraic model checking and its applications to systems biology'. Together they form a unique fingerprint.

Cite this