An LTL Model Checking Approach for Biological Parameter Inference

被引：0

作者：

Gallet, Emmanuelle ^{[1
]}

Manceny, Matthieu ^{[2
]}

Le Gall, Pascale ^{[1
]}

Ballarini, Paolo ^{[1
]}

机构：

[1] Ecole Cent Paris, Lab MAS, F-92195 Chatenay Malabry, France

[2] ISEP, Lab LISITE, F-75006 Paris, France

来源：

FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2014 | 2014年 / 8829卷

关键词：

LTL Model Checking; Parameter Identification; Symbolic Execution; Genetic Regulatory Network; Thomas Discrete Modeling; REGULATORY NETWORKS;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

The identification of biological parameters governing dynamics of Genetic Regulatory Networks (GRN) poses a problem of combinatorial explosion, since the possibilities of parameter instantiation are numerous even for small networks. In this paper, we propose to adapt LTL model checking algorithms to infer biological parameters from biological properties given as LTL formulas. In order to reduce the combinatorial explosion, we represent all the dynamics with one parametric model, so that all GRN dynamics simply result from all eligible parameter instantiations. LTL model checking algorithms are adapted by postponing the parameter instantiation as far as possible. Our approach is implemented within the SPuTNIk tool.

引用

页码：155 / 170

页数：16

共 50 条

[21] Simple bounded LTL model checking
Latvala, T
Biere, AN
Heljanko, K
Junttila, T
FORMAL METHODS IN COMPUTER-AIDED DESIGN, 2004, 3312 : 186 - 200
[22] Bounded model checking for past LTL
Benedetti, M
Cimatti, A
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2003, 2619 : 18 - 33
[23] Measuring Progress of Probabilistic LTL Model Checking
Cormie-Bowins, Elise
van Breugel, Franck
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (85): : 33 - 47
[24] LTL model checking for modular Petri nets
Latvala, T
Mäkelä, M
APPLICATIONS AND THEORY OF PETRI NETS 2004, PROCEEDINGS, 2004, 3099 : 298 - 311
[25] Tuning SAT solvers for LTL Model Checking
Kheireddine, Anissa
Renault, Etienne
Baarir, Souheib
2022 29TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, APSEC, 2022, : 259 - 268
[26] LTL model checking of self modifying code
Touili, Tayssir
Ye, Xin
FORMAL METHODS IN SYSTEM DESIGN, 2022, 60 (02) : 195 - 227
[27] Model checking LTL using constraint programming
Esparza, J
Melzer, S
APPLICATION AND THEORY OF PETRI NETS 1997, 1997, 1248 : 1 - 20
[28] Program complexity of dynamic LTL model checking
Kähler, D
Wilke, T
COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2003, 2803 : 271 - 284
[29] Yet another look at LTL model checking
Schneider, K
CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, 1999, 1703 : 321 - 325
[30] LTL model checking for communicating concurrent programs
Adrien Pommellet
Tayssir Touili
Innovations in Systems and Software Engineering, 2020, 16 : 161 - 179

← 1 2 3 4 5 →