Syntactic Markovian Bisimulation for Chemical Reaction Networks

被引:16
作者
Cardelli, Luca [1 ,2 ]
Tribastone, Mirco [3 ]
Tschaikowski, Max [3 ]
Vandin, Andrea [3 ]
机构
[1] Microsoft Res, Oxford, England
[2] Univ Oxford, Oxford, England
[3] IMT Sch Adv Studies Lucca, Lucca, Italy
来源
MODELS, ALGORITHMS, LOGICS AND TOOLS: ESSAYS DEDICATED TO KIM GULDSTRAND LARSEN ON THE OCCASION OF HIS 60TH BIRTHDAY | 2017年 / 10460卷
关键词
PROBABILISTIC MODEL CHECKING; PROCESS ALGEBRA; REDUCTION; SYSTEMS; CHAINS; LUMPABILITY; SIMULATION; FRAMEWORK; BIOLOGY; PEPA;
D O I
10.1007/978-3-319-63121-9_23
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
In chemical reaction networks (CRNs) with stochastic semantics based on continuous-time Markov chains (CTMCs), the typically large populations of species cause combinatorially large state spaces. This makes the analysis very difficult in practice and represents the major bottleneck for the applicability of minimization techniques based, for instance, on lumpability. In this paper we present syntactic Markovian bisimulation (SMB), a notion of bisimulation developed in the Larsen-Skou style of probabilistic bisimulation, defined over the structure of a CRN rather than over its underlying CTMC. SMB identifies a lumpable partition of the CTMC state space a priori, in the sense that it is an equivalence relation over species implying that two CTMC states are lumpable when they are invariant with respect to the total population of species within the same equivalence class. We develop an efficient partition-refinement algorithm which computes the largest SMB of a CRN in polynomial time in the number of species and reactions. We also provide an algorithm for obtaining a quotient network from an SMB that induces the lumped CTMC directly, thus avoiding the generation of the state space of the original CRN altogether. In practice, we show that SMB allows significant reductions in a number of models from the literature. Finally, we study SMB with respect to the deterministic semantics of CRNs based on ordinary differential equations (ODEs), where each equation gives the time-course evolution of the concentration of a species. SMB implies forward CRN bisimulation, a recently developed behavioral notion of equivalence for the ODE semantics, in an analogous sense: it yields a smaller ODE system that keeps track of the sums of the solutions for equivalent species.
引用
收藏
页码:466 / 483
页数:18
相关论文
共 48 条
  • [1] Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks
    Abate, Alessandro
    Brim, Lubos
    Ceska, Milan
    Kwiatkowska, Marta
    [J]. COMPUTER AIDED VERIFICATION, PT I, 2015, 9206 : 195 - 213
  • [2] [Anonymous], GEN EV COMP C GECCO
  • [3] Autant C., 1992, Application and Theory of Petri Nets 1992. 13th International Conference Proceedings, P45
  • [4] Deciding bisimilarity and similarity for probabilistic processes
    Baier, C
    Engelen, B
    Majster-Cederbaum, M
    [J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2000, 60 (01) : 187 - 231
  • [5] BioNetGen: software for rule-based modeling of signal transduction based on the interactions of molecular domains
    Blinov, ML
    Faeder, JR
    Goldstein, B
    Hlavacek, WS
    [J]. BIOINFORMATICS, 2004, 20 (17) : 3289 - 3291
  • [6] EXACT AND ORDINARY LUMPABILITY IN FINITE MARKOV-CHAINS
    BUCHHOLZ, P
    [J]. JOURNAL OF APPLIED PROBABILITY, 1994, 31 (01) : 59 - 75
  • [7] On process rate semantics
    Cardelli, Luca
    [J]. THEORETICAL COMPUTER SCIENCE, 2008, 391 (03) : 190 - 215
  • [8] ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations
    Cardelli, Luca
    Tribastone, Mirco
    Tschaikowski, Max
    Vandin, Andrea
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2017, PT II, 2017, 10206 : 310 - 328
  • [9] Comparing Chemical Reaction Networks: A Categorical and Algorithmic Perspective
    Cardelli, Luca
    Tribastone, Mirco
    Tschaikowski, Max
    Vandin, Andrea
    [J]. PROCEEDINGS OF THE 31ST ANNUAL ACM-IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2016), 2016, : 485 - 494
  • [10] Efficient Syntax-Driven Lumping of Differential Equations
    Cardelli, Luca
    Tribastone, Mirco
    Tschaikowski, Max
    Vandin, Andrea
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS (TACAS 2016), 2016, 9636 : 93 - 111