ABSTRACT
Ordinary differential equations (ODEs) are widespread in many natural sciences including chemistry, ecology, and systems biology, and in disciplines such as control theory and electrical engineering. Building on the celebrated molecules-as-processes paradigm, they have become increasingly popular in computer science, with high-level languages and formal methods such as Petri nets, process algebra, and rule-based systems that are interpreted as ODEs. We consider the problem of comparing and minimizing ODEs automatically. Influenced by traditional approaches in the theory of programming, we propose differential equivalence relations. We study them for a basic intermediate language, for which we have decidability results, that can be targeted by a class of high-level specifications. An ODE implicitly represents an uncountable state space, hence reasoning techniques cannot be borrowed from established domains such as probabilistic programs with finite-state Markov chain semantics. We provide novel symbolic procedures to check an equivalence and compute the largest one via partition refinement algorithms that use satisfiability modulo theories. We illustrate the generality of our framework by showing that differential equivalences include (i) well-known notions for the minimization of continuous-time Markov chains (lumpability), (ii)~bisimulations for chemical reaction networks recently proposed by Cardelli et al., and (iii) behavioral relations for process algebra with ODE semantics. With a prototype implementation we are able to detect equivalences in biochemical models from the literature that cannot be reduced using competing automatic techniques.
- MAPK cascade in yeast - dimerization of Ste5. Available at http: //vcell.org/bionetgen/samples.html.Google Scholar
- A. Antoulas. Approximation of Large-Scale Dynamical Systems. Advances in Design and Control. SIAM, 2005. Google ScholarDigital Library
- U. M. Ascher and L. R. Petzold. Computer Methods for Ordinary Differential Equations and Differential-Algebraic Equations. SIAM, 1988. Google ScholarDigital Library
- A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic, 1(1): 162–170, 2000. Google ScholarDigital Library
- C. Baier and J.-P. Katoen. Principles of model checking. MIT Press, 2008. ISBN 978-0-262-02649-9. Google ScholarDigital Library
- C. Baier, B. Engelen, and M. E. Majster-Cederbaum. Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci., 60(1):187–231, 2000. Google ScholarDigital Library
- C. Barrett, R. Sebastiani, S. A. Seshia, S. A. S. Cesare Tinelli Clark Barrett, Roberto Sebastiani, and C. Tinelli. Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications, chapter Satisfiability Modulo Theories. IOS Press, 2009.Google Scholar
- D. Barua and B. Goldstein. A mechanistic model of early FcεRI signaling: lipid rafts and the question of protection from dephosphorylation. PLoS One, 7(12), 2012.Google Scholar
- J. Berdine and N. Bjørner. Computing all implied equalities via SMTbased partition refinement. In Automated Reasoning, volume 8562 of LNCS, pages 168–183. Springer, 2014.Google Scholar
- M. Bernardo. A survey of Markovian behavioral equivalences. In Formal Methods for Performance Evaluation, volume 4486 of LNCS, pages 180–219. Springer, 2007. Google ScholarDigital Library
- M. L. Blinov, J. R. Faeder, B. Goldstein, and W. S. Hlavacek. BioNet-Gen: software for rule-based modeling of signal transduction based on the interactions of molecular domains. Bioinformatics, 20(17): 3289–3291, 2004. Google ScholarDigital Library
- P. Buchholz. Exact and ordinary lumpability in finite markov chains. Journal of Applied Probability, 31(1):59–75, 1994.Google ScholarCross Ref
- P. Buchholz. Exact performance equivalence: An equivalence relation for stochastic automata. Theoretical Computer Science, 215(1–2): 263–287, 1999. Google ScholarDigital Library
- L. Calzone, F. Fages, and S. Soliman. BIOCHAM: an environment for modeling biological systems and formalizing experimental knowledge. Bioinformatics, 22(14):1805–1807, 2006. Google ScholarDigital Library
- F. Camporesi and J. Feret. Formal reduction for rule-based models. Electronic Notes in Theoretical Computer Science, 276:29–59, 2011. Google ScholarDigital Library
- F. Camporesi, J. Feret, H. Koeppl, and T. Petrov. Combining model reductions. Electronic Notes in Theoretical Computer Science, 265: 73–96, 2010. Google ScholarDigital Library
- L. Cardelli. On process rate semantics. Theoretical Computer Science, 391(3):190–215, 2008. Google ScholarDigital Library
- L. Cardelli. Morphisms of reaction networks that couple structure to function. BMC Systems Biology, 8(1):84, 2014.Google ScholarCross Ref
- L. Cardelli and A. Csikász-Nagy. The cell cycle switch computes approximate majority. Sci. Rep., 2, 2012.Google Scholar
- L. Cardelli, M. Tribastone, M. Tschaikowski, and A. Vandin. Forward and backward bisimulations for chemical reaction networks. In CONCUR, pages 226–239, 2015.Google Scholar
- F. Ciocchetta and J. Hillston. Bio-PEPA: A framework for the modelling and analysis of biological systems. Theoretical Computer Science, 410 (33-34):3065–3084, 2009. Google ScholarDigital Library
- J. Colvin, M. I. Monine, J. R. Faeder, W. S. Hlavacek, D. D. V. Hoff, and R. G. Posner. Simulation of large-scale rule-based models. Bioinformatics, 25(7):910–917, 2009. Google ScholarDigital Library
- J. Colvin, M. I. Monine, R. N. Gutenkunst, W. S. Hlavacek, D. D. V. Hoff, and R. G. Posner. Rulemonkey: software for stochastic simulation of rule-based models. BMC Bioinformatics, 11:404, 2010.Google ScholarCross Ref
- H. Conzelmann, J. Saez-Rodriguez, T. Sauter, B. Kholodenko, and E. Gilles. A domain-oriented approach to the reduction of combinatorial complexity in signal transduction networks. BMC Bioinformatics, 7(1): 34, 2006.Google ScholarCross Ref
- H. Conzelmann, D. Fey, and E. Gilles. Exact model reduction of combinatorial reaction networks. BMC Systems Biology, 2(1):78, 2008.Google ScholarCross Ref
- V. Danos and C. Laneve. Formal molecular biology. Theoretical Computer Science, 325(1):69–110, 2004. Google ScholarDigital Library
- V. Danos, J. Desharnais, F. Laviolette, and P. Panangaden. Bisimulation and cocongruence for probabilistic systems. Information and Computation, 204(4):503–523, 2006. Google ScholarDigital Library
- V. Danos, J. Feret, W. Fontana, R. Harmer, and J. Krivine. Abstracting the differential semantics of rule-based models: Exact and automated model reduction. In LICS, pages 362–381, 2010. Google ScholarDigital Library
- R. David and H. Alla. Discrete, Continuous, and Hybrid Petri Nets. Springer, 2005.Google Scholar
- L. De Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, pages 337–340, 2008. Google ScholarDigital Library
- R. De Nicola, D. Latella, M. Loreti, and M. Massink. A uniform definition of stochastic process calculi. ACM Computing Surveys, 46 (1):5:1–5:35, 2013. Google ScholarDigital Library
- C. Dehnert, J.-P. Katoen, and D. Parker. SMT-based bisimulation minimisation of Markov models. In VMCAI, volume 7737 of LNCS, pages 28–47, 2013.Google Scholar
- S. Derisavi, H. Hermanns, and W. H. Sanders. Optimal state-space lumping in Markov chains. Inf. Process. Lett., 87(6):309–315, 2003. Google ScholarDigital Library
- J. R. Faeder, W. S. Hlavacek, I. Reischl, M. L. Blinov, H. Metzger, A. Redondo, C. Wofsy, and B. Goldstein. Investigation of early events in FcεRI-mediated signaling using a detailed mathematical model. The Journal of Immunology, 170(7):3769–3781, 2003.Google ScholarCross Ref
- J. Feret. Fragments-based model reduction: Some case studies. Electronic Notes in Theoretical Computer Science, 268:77–96, 2010. Google ScholarDigital Library
- J. Feret, V. Danos, J. Krivine, R. Harmer, and W. Fontana. Internal coarse-graining of molecular systems. Proceedings of the National Academy of Sciences, 106(16):6453–6458, 2009.Google ScholarCross Ref
- J. Feret, T. Henzinger, H. Koeppl, and T. Petrov. Lumpability abstractions of rule-based systems. Theoretical Computer Science, 431: 137–164, 2012. Google ScholarDigital Library
- J. Fisher and T. Henzinger. Executable cell biology. Nature Biotechnology, 25(11):1239–1249, 2007.Google ScholarCross Ref
- V. Galpin. Continuous approximation of PEPA models and Petri nets. International Journal of Computer Aided Engineering and Technology, 2:324–339, 2010.Google ScholarCross Ref
- S. Gao, S. Kong, and E. Clarke. Satisfiability modulo ODEs. In FMCAD, pages 105–112, 2013.Google Scholar
- S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan. Synthesis of loop-free programs. In PLDI, pages 62–73, 2011. Google ScholarDigital Library
- R. A. Hayden and J. T. Bradley. A fluid analysis framework for a Markovian process algebra. Theoretical Computer Science, 411(22- 24):2260–2297, 2010. Google ScholarDigital Library
- M. Heiner, D. Gilbert, and R. Donaldson. Petri nets for systems and synthetic biology. In Formal Methods for Computational Systems Biology, volume 5016 of LNCS, pages 215–264. Springer, 2008. Google ScholarDigital Library
- H. Hermanns and M. Rettelbach. Syntax, semantics, equivalences, and axioms for MTIPP. In Proceedings of Process Algebra and Probabilistic Methods, pages 71–87, Erlangen, 1994.Google Scholar
- H. Hermanns and M. Siegle. Bisimulation algorithms for stochastic process algebras and their BDD-based implementation. In ARTS, pages 244–264, 1999. Google ScholarDigital Library
- J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996. Google ScholarDigital Library
- J. Hillston. Fluid flow approximation of PEPA models. In QEST, pages 33–43, Sept. 2005. Google ScholarDigital Library
- D. T. Huynh and L. Tian. On some equivalence relations for probabilistic processes. Fundam. Inform., 17(3):211–234, 1992.Google ScholarCross Ref
- G. Iacobelli, M. Tribastone, and A. Vandin. Differential bisimulation for a Markovian process algebra. In MFCS, pages 293–306, 2015.Google ScholarCross Ref
- D. Jovanovic and L. M. de Moura. Solving non-linear arithmetic. In IJCAR, pages 339–354, 2012. Google ScholarDigital Library
- P. C. Kanellakis and S. A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput., 86(1): 43–68, 1990. Google ScholarDigital Library
- J. Kemeny and J. Snell. Finite Markov Chains. Springer New York, Heidelberg, Berlin, 1976.Google Scholar
- P. Kocieniewski, J. R. Faeder, and T. Lipniacki. The interplay of double phosphorylation and scaffolding in MAPK pathways. Journal of Theoretical Biology, 295:116–124, 2012.Google ScholarCross Ref
- A. S. Köksal, V. Kuncak, and P. Suter. Constraints as control. In POPL, pages 151–164, 2012. Google ScholarDigital Library
- M. Kwiatkowska, G. Norman, and D. Parker. Prism 4.0: Verification of probabilistic real-time systems. In CAV, pages 585–591, 2011. Google ScholarDigital Library
- M. Kwiatkowski and I. Stark. The continuous pi-calculus: A process algebra for biochemical modelling. In CMSB, pages 103–122, 2008. Google ScholarDigital Library
- K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Inf. Comput., 94(1):1–28, 1991. Google ScholarDigital Library
- Y. Li, A. Albarghouthi, Z. Kincaid, A. Gurfinkel, and M. Chechik. Symbolic optimization with SMT solvers. In POPL, pages 607–618, 2014. Google ScholarDigital Library
- S. Mover, A. Cimatti, A. Tiwari, and S. Tonetta. Time-aware relational abstractions for hybrid systems. In EMSOFT, pages 1–10, 2013. Google ScholarDigital Library
- M. Nagasaki, S. Onami, S. Miyano, and H. Kitano. Bio-calculus: Its concept and molecular interaction. Genome Informatics, 10:133–143, 1999.Google Scholar
- D. L. Nelson and M. M. Cox. Lehninger Principles of Biochemistry. Palgrave Macmillan, 6th edition, 2013.Google Scholar
- J. Norris. Markov Chains. Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, 1998.Google Scholar
- M. S. Okino and M. L. Mavrovouniotis. Simplification of mathematical models of chemical reaction systems. Chemical Reviews, 2(98):391– 408, 1998.Google ScholarCross Ref
- R. Paige and R. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973–989, 1987. Google ScholarDigital Library
- G. J. Pappas. Bisimilar linear systems. Automatica, 39(12):2035–2047, 2003. Google ScholarDigital Library
- M. Pedersen and G. Plotkin. A language for biochemical systems: Design and formal specification. In Transactions on Computational Systems Biology XII, volume 5945 of LNCS, pages 77–145. Springer, 2010. Google ScholarDigital Library
- A. D. Pierro, C. Hankin, and H. Wiklicky. Quantitative relations and approximate process equivalences. In CONCUR, pages 498–512, 2003.Google ScholarCross Ref
- A. Regev and E. Shapiro. Cellular abstractions: Cells as computation. Nature, 419(6905):343–343, 2002.Google ScholarCross Ref
- S. Sankaranarayanan and A. Tiwari. Relational abstractions for continuous and hybrid systems. In CAV, pages 686–702, 2011. Google ScholarDigital Library
- M. W. Sneddon, J. R. Faeder, and T. Emonet. Efficient modeling, simulation and coarse-graining of biological complexity with NFsim. Nature Methods, 8(2):177–183, 2011.Google ScholarCross Ref
- J. Sproston and S. Donatelli. Backward bisimulation in Markov chain model checking. IEEE Trans. Software Eng., 32(8):531–546, 2006. Google ScholarDigital Library
- W. J. Stewart. Probability, Markov Chains, Queues, and Simulation. Princeton University Press, 2009. Google ScholarDigital Library
- R. Suderman and E. J. Deeds. Machines vs. ensembles: Effective MAPK signaling through heterogeneous sets of protein complexes. PLoS Comput. Biol., 9(10):e1003278, 10 2013.Google ScholarCross Ref
- J. Toth, G. Li, H. Rabitz, and A. S. Tomlin. The effect of lumping and expanding on kinetic differential equations. SIAM Journal on Applied Mathematics, 57(6):1531–1556, 1997. Google ScholarDigital Library
- M. Tribastone. A fluid model for layered queueing networks. IEEE Trans. Software Eng., 39(6):744–756, 2013. Google ScholarDigital Library
- M. Tribastone, S. Gilmore, and J. Hillston. Scalable differential analysis of process algebra models. IEEE Trans. Software Eng., 38(1):205–219, 2012. Google ScholarDigital Library
- M. Tschaikowski and M. Tribastone. Exact fluid lumpability for Markovian process algebra. In CONCUR, pages 380–394, 2012. Google ScholarDigital Library
- A. Valmari and G. Franceschinis. Simple O(m log n) time Markov chain lumping. In TACAS, pages 38–52, 2010. Google ScholarDigital Library
- A. J. van der Schaft. Equivalence of dynamical systems by bisimulation. IEEE Transactions on Automatic Control, 49, 2004.Google Scholar
- E. O. Voit. Biochemical systems theory: A review. ISRN Biomathematics, 2013:53, 2013. URL http://dx.doi.org/10.1155/2013/ 897658%}897658.Google ScholarCross Ref
Index Terms
- Symbolic computation of differential equivalences
Recommendations
Symbolic computation of differential equivalences
POPL '16Ordinary differential equations (ODEs) are widespread in many natural sciences including chemistry, ecology, and systems biology, and in disciplines such as control theory and electrical engineering. Building on the celebrated molecules-as-processes ...
Symbolic computation of differential equivalences
AbstractOrdinary differential equations (ODEs) are widespread in many natural sciences including chemistry, ecology, and systems biology, and in disciplines such as control theory and electrical engineering. Building on the celebrated ...
Linearization techniques for singular initial-value problems of ordinary differential equations
Linearization methods for singular initial-value problems in second-order ordinary differential equations are presented. These methods result in linear constant-coefficients ordinary differential equations which can be integrated analytically, thus ...
Comments