Speaker: |
Quoc-Nam Tran, Lamar Univ, Texas, USA |
Title: |
Algebraic& Statistic Computation for Model Checking in BioInformatics |
Date: |
04.06. 2012 13:30--14:30 |
Location: |
RISC Seminar room |
Abstract: |
Temporal model checking is an algorithmic and formal approach for
automatically verifying whether a finite-state concurrent system such
as a sequential circuit design functions correctly. Typically,
computation is carried over Boolean algebras using binary decision
diagrams (BDDs) or satisfiability (SAT) solvers. Researchers have been
using BDDs and bounded model checking (BMC) on Boolean gene regulatory
networks for bioinformatics. Previous works also showed that BDDs
blow-up more frequently on random networks than on sequential circuits.
A gene regulatory network is a collection of DNA segments in a cell
which interact with each other indirectly through their RNA and protein
expression products and with other substances in the cell, thereby
governing the rates at which genes in the network are transcribed into
mRNA. We present a computational method for direct computation of
Groebner bases (GB) in Boolean rings for temporal logic reasoning and
for checking the dynamic of Boolean gene regulatory networks in
particular. In contrast to other known algebraic approaches, the degree
of intermediate polynomials during the calculation of Groebner bases
using our method will never grow resulted in a significant improvement
in running time and memory space consumption.
Another focus of this talk is on probabilistic boolean networks because
recent experimental results have demonstrated that gene expression is a
stochastic process. We will show how algebraic and continuous
stochastic logic can be used for checking the dynamic of probabilistic
boolean networks in the context of Markov theory. |
VCAL file: |
|