BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Sven DRAŽAN, Jana FABRIKOVÁ and David ŠAFRÁNEK. On Algorithmic Analysis of Transcriptional Regulation by LTL Model Checking. Theoretical Computer Science. vol. 2009, No 410, p. 3128-3148, 20 pp. ISSN 0304-3975. 2009.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name On Algorithmic Analysis of Transcriptional Regulation by LTL Model Checking
Name in Czech Algoritmická analýza transkripční regulace s využitím metody ověřování modelů
Authors BARNAT, Jiří (203 Czech Republic, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution), Ivana ČERNÁ (203 Czech Republic, belonging to the institution), Sven DRAŽAN (203 Czech Republic, belonging to the institution), Jana FABRIKOVÁ (203 Czech Republic, belonging to the institution) and David ŠAFRÁNEK (203 Czech Republic, guarantor, belonging to the institution).
Edition Theoretical Computer Science, 2009, 0304-3975.
Other information
Original language English
Type of outcome Article in a journal
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Czech Republic
Confidentiality degree is not subject to a state or trade secret
WWW URL
Impact factor Impact factor: 0.943
RIV identification code RIV/00216224:14330/09:00029225
Organization unit Faculty of Informatics
UT WoS 000268921500007
Keywords in English Genetic regulatory network; Piecewise-linear approximation; Model checking
Tags Genetic regulatory network, Model checking, Piecewise-linear approximation
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 2/2/2011 09:33.
Abstract
This paper is focused on the model checking approach for analysis of piecewise-linear deterministic models of genetic regulatory networks. Firstly, the qualitative simulation algorithm of de Jong et.al. that builds the heart of Genetic Network Analyzer (GNA) is revisited and its time complexity is studied in detail. Secondly, a novel algorithm that reduces the state space generation time is introduced. The new algorithm is developed as an abstraction of the original GNA algorithm. Finally, a fragment of linear time temporal logic for which the provided abstraction is conservative is identified. Efficiency of the new algorithm when implemented in the parallel model checking environment is demonstrated on a set of experiments performed on randomly modified biological models. In general, the achieved results bring a new insight into the field of qualitative simulation emerging in the context of systems biology.
Abstract (in Czech)
Článek přináší výsledek v oblasti algoritmické analýzy modelů dynamiky genetických regulačních sítí. Z teoretického hlediska je analyzována (exponenciální) složitost výpočtu de Jongova algoritmu pro kvalitativní analýzu genetických regulačních sítí prostřednictvím metody ověřování modelů. Na základě této analýzy je navržena abstrakce snižující třídu exponenciality časové složitosti výpočtu. V článku je rovněž identifikován fragment lineární temporální logiky, pro nějž je navrhovaná abstrakce systému konzervativní. V praktické části článku jsou prezentovány experimenty na nichž je porovnána původní verze algoritmu s verzí abstrahovanou.
Links
GA201/09/1389, research and development projectName: Verifikace a analýza velmi velkých počítačových systémů
Investor: Czech Science Foundation, Verification and Analysis of Large-Scale Computer Systems
MSM0021622419, plan (intention)Name: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
PrintDisplayed: 29/3/2024 01:17