Automatic Verification of Biochemical Network Using Model Checking Method

Jinkyung Kim, Younghee Lee, il Moon

Research output: Contribution to journalArticle

Abstract

This study focuses on automatic searching and verifying methods for the reachability, transition logics and hierarchical structure in all possible paths of biological processes using model checking. The automatic search and verification for alternative paths within complex and large networks in biological process can provide a considerable amount of solutions, which is difficult to handle manually. Model checking is an automatic method for verifying if a circuit or a condition, expressed as a concurrent transition system, satisfies a set of properties expressed in a temporal logic, such as computational tree logic (CTL). This article represents that model checking is feasible in biochemical network verification and it shows certain advantages over simulation for querying and searching of special behavioral properties in biochemical processes.

Original languageEnglish
Pages (from-to)90-94
Number of pages5
JournalChinese Journal of Chemical Engineering
Volume16
Issue number1
DOIs
Publication statusPublished - 2008 Feb 1

Fingerprint

Model checking
Biological Phenomena
Biochemical Phenomena
Temporal logic
Networks (circuits)

All Science Journal Classification (ASJC) codes

  • Environmental Engineering
  • Biochemistry
  • Chemistry(all)
  • Chemical Engineering(all)

Cite this

@article{bce57aabaf78426b8393d45355c5ac84,
title = "Automatic Verification of Biochemical Network Using Model Checking Method",
abstract = "This study focuses on automatic searching and verifying methods for the reachability, transition logics and hierarchical structure in all possible paths of biological processes using model checking. The automatic search and verification for alternative paths within complex and large networks in biological process can provide a considerable amount of solutions, which is difficult to handle manually. Model checking is an automatic method for verifying if a circuit or a condition, expressed as a concurrent transition system, satisfies a set of properties expressed in a temporal logic, such as computational tree logic (CTL). This article represents that model checking is feasible in biochemical network verification and it shows certain advantages over simulation for querying and searching of special behavioral properties in biochemical processes.",
author = "Jinkyung Kim and Younghee Lee and il Moon",
year = "2008",
month = "2",
day = "1",
doi = "10.1016/S1004-9541(08)60043-9",
language = "English",
volume = "16",
pages = "90--94",
journal = "Chinese Journal of Chemical Engineering",
issn = "1004-9541",
publisher = "Chemical Industry Press",
number = "1",

}

Automatic Verification of Biochemical Network Using Model Checking Method. / Kim, Jinkyung; Lee, Younghee; Moon, il.

In: Chinese Journal of Chemical Engineering, Vol. 16, No. 1, 01.02.2008, p. 90-94.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Automatic Verification of Biochemical Network Using Model Checking Method

AU - Kim, Jinkyung

AU - Lee, Younghee

AU - Moon, il

PY - 2008/2/1

Y1 - 2008/2/1

N2 - This study focuses on automatic searching and verifying methods for the reachability, transition logics and hierarchical structure in all possible paths of biological processes using model checking. The automatic search and verification for alternative paths within complex and large networks in biological process can provide a considerable amount of solutions, which is difficult to handle manually. Model checking is an automatic method for verifying if a circuit or a condition, expressed as a concurrent transition system, satisfies a set of properties expressed in a temporal logic, such as computational tree logic (CTL). This article represents that model checking is feasible in biochemical network verification and it shows certain advantages over simulation for querying and searching of special behavioral properties in biochemical processes.

AB - This study focuses on automatic searching and verifying methods for the reachability, transition logics and hierarchical structure in all possible paths of biological processes using model checking. The automatic search and verification for alternative paths within complex and large networks in biological process can provide a considerable amount of solutions, which is difficult to handle manually. Model checking is an automatic method for verifying if a circuit or a condition, expressed as a concurrent transition system, satisfies a set of properties expressed in a temporal logic, such as computational tree logic (CTL). This article represents that model checking is feasible in biochemical network verification and it shows certain advantages over simulation for querying and searching of special behavioral properties in biochemical processes.

UR - http://www.scopus.com/inward/record.url?scp=40249091372&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=40249091372&partnerID=8YFLogxK

U2 - 10.1016/S1004-9541(08)60043-9

DO - 10.1016/S1004-9541(08)60043-9

M3 - Article

VL - 16

SP - 90

EP - 94

JO - Chinese Journal of Chemical Engineering

JF - Chinese Journal of Chemical Engineering

SN - 1004-9541

IS - 1

ER -