Abstract
We propose a novel scalable parallel algorithm for synthesis of interdependent parameters from CTL specifications for non-linear dynamical systems. The method employs a symbolic representation of sets of parameter valuations in terms of the first-order theory of the reals. To demonstrate its practicability, we apply the method to a class of piecewise multi-affine dynamical systems representing dynamics of biological systems with complex non-linear behaviour.
This work has been supported by the Czech Science Foundation grant GA15-11089S.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Arney, D., Pajic, M., Goldman, J.M., Lee, I., Mangharam, R., Sokolsky, O.: Toward patient safety in closed-loop medical device systems. In: ICCPS 2010, pp. 139–148. ACM (2010)
Baker, M., Carpenter, B., Shafi, A.: MPJ express: towards thread safe Java HPC. In: IEEE Cluster Computing 2006. IEEE Computer Society (2006)
Barnat, J., Brim, L., Krejčí, A., Streck, A., Šafránek, D., Vejnár, M., Vejpustek, T.: On parameter synthesis by parallel model checking. IEEE/ACM Trans. Comput. Biol. Bioinf. 9(3), 693–705 (2012)
Barnat, J., Brim, L., Šafránek, D.: High-performance analysis of biological systems dynamics with the divine model checker. Brief. Bioinf. 11(3), 301–312 (2010)
Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.5. Technical report, Department of Computer Science, The University of Iowa (2015)
Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics). Springer-Verlag New York Inc, Secaucus (2006)
Batt, G., Page, M., Cantone, I., Gössler, G., Monteiro, P., de Jong, H.: Efficient parameter search for qualitative models of regulatory networks using symbolic model checking. Bioinformatics 26(18), 603–610 (2010)
Batt, G., Yordanov, B., Weiss, R., Belta, C.: Robustness analysis and tuning of synthetic gene networks. Bioinformatics 23(18), 2415–2422 (2007)
Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., Grosu, R.: Abstraction-based parameter synthesis for multiaffine systems. In: Piterman, N., et al. (eds.) HVC 2015. LNCS, vol. 9434, pp. 19–35. Springer, Heidelberg (2015). doi:10.1007/978-3-319-26287-1_2
Brim, L., Dluhoš, P., Šafránek, D., Vejpustek, T.: STL*: extending signal temporal logic with signal-value freezing operator. Inf. Comput. 236, 52–67 (2014). Special Issue on Hybrid Systems and Biology
Brim, L., Češka, M., Demko, M., Pastva, S., Šafránek, D.: Parameter synthesis by parallel coloured CTL model checking. In: Roux, O., Bourdon, J. (eds.) CMSB 2015. LNCS, vol. 9308, pp. 251–263. Springer, Heidelberg (2015)
Brim, L., Demko, M., Pastva, S., Šafránek, D.: High-performance discrete bifurcation analysis for piecewise-affine dynamical systems. In: Abate, A., et al. (eds.) HSB 2015. LNCS, vol. 9271, pp. 58–74. Springer, Heidelberg (2015). doi:10.1007/978-3-319-26916-0_4
Brim, L., Yorav, K., Žídková, J.: Assumption-based distribution of CTL model checking. STTT 7(1), 61–73 (2005)
Chiang, H.D., Wang, T.: On the number and types of unstable equilibria in nonlinear dynamical systems with uniformly-bounded stability regions. IEEE Trans. Autom. Control 61(2), 485–490 (2016)
Collins, P., Habets, L.C., van Schuppen, J.H., Černá, I., Fabriková, J., Šafránek, D.: Abstraction of biochemical reaction systems on polytopes. In: IFAC World Congress. pp. 14869–14875. IFAC (2011)
Dang, T., Donze, A., Maler, O., Shalev, N.: Sensitive state-space exploration. In: IEEE Conference on Decision and Control, pp. 4049–4054 (2008)
Donzé, A., Fanchon, E., Gattepaille, L.M., Maler, O., Tracqui, P.: Robustness analysis and behavior discrimination in enzymatic reaction networks. PLoS ONE 6(9), e24246 (2011)
Donzé, A., Krogh, B., Rajhans, A.: Parameter synthesis for hybrid systems with an application to simulink models. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol. 5469, pp. 165–179. Springer, Heidelberg (2009)
Donzé, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S.: On temporal logic and signal processing. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 92–106. Springer, Heidelberg (2012)
Dreossi, T., Dang, T.: Parameter synthesis for polynomial biological models. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, HSCC 2014, pp. 233–242 (2014)
Dvorak, P., Chrast, L., Nikel, P.I., Fedr, R., Soucek, K., Sedlackova, M., Chaloupkova, R., Lorenzo, V., Prokop, Z., Damborsky, J.: Exacerbation of substrate toxicity by IPTG in Escherichia coli BL21(DE3) carrying a synthetic metabolic pathway. Microb. Cell Fact. 14(1), 1–15 (2015)
Elowitz, M.B., Leibler, S.: A synthetic oscillatory network of transcriptional regulators. Nature 403(6767), 335–338 (2000)
Gao, S., Kong, S., Clarke, E.M.: \({\sf dReal{:}}\) an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 208–214. Springer, Heidelberg (2013)
Gardner, T.S., Cantor, C.R., Collins, J.J.: Construction of a genetic toggle switch in Escherichia coli. Nature 403, 339–342 (1999)
Giacobbe, M., Guet, C.C., Gupta, A., Henzinger, T.A., Paixão, T., Petrov, T.: Model checking gene regulatory networks. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 469–483. Springer, Heidelberg (2015)
Grosu, R., Batt, G., Fenton, F.H., Glimm, J., Le Guernic, C., Smolka, S.A., Bartocci, E.: From cardiac cells to genetic regulatory networks. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 396–411. Springer, Heidelberg (2011)
Jha, S., Shyamasundar, R.K.: Adapting biochemical kripke structures for distributed model checking. In: Priami, C., Ingólfsdóttir, A., Mishra, B., Riis Nielson, H. (eds.) Transactions on Computational Systems Biology VII. LNCS (LNBI), vol. 4230, pp. 107–122. Springer, Heidelberg (2006)
Li, W., Zhong, L., He, Y., Meng, J., Yao, F., Guo, Y., Xu, C.: Multiple steady-states analysis and unstable operating point stabilization in homogeneous azeotropic distillation with intermediate entrainer. Ind. Eng. Chem. Res. 54(31), 7668–7686 (2015)
Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: POPL 2014, pp. 607–618. ACM (2014)
Madsen, C., Shmarov, F., Zuliani, P.: BioPSy: an SMT-based tool for guaranteed parameter set synthesis of biological models. In: Roux, O., Bourdon, J. (eds.) CMSB 2015. LNCS, vol. 9308, pp. 182–194. Springer, Heidelberg (2015)
Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004)
Milias-Argeitis, A., Engblom, S., Bauer, P., Khammash, M.: Stochastic focusing coupled with negative feedback enables robust regulation in biochemical reaction networks. J. R. Soc. Interface 12(113), 20150831 (2015)
de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Raman, V., Donzé, A., Sadigh, D., Murray, R.M., Seshia, S.A.: Reactive synthesis from signal temporal logic specifications. In: HSCC 2015, pp. 239–248. ACM (2015)
Rizk, A., Batt, G., Fages, F., Soliman, S.: A general computational method for robustness analysis with applications to synthetic gene networks. Bioinformatics 25(12), i169–i178 (2009)
Rosenfeld, N., Alon, U.: Response delays and the structure of transcription networks. J. Mol. Biol. 329(4), 645–654 (2003)
Swat, M., Kel, A., Herzel, H.: Bifurcation analysis of the regulatory modules of the mammalian G1/S transition. Bioinformatics 20(10), 1506–1511 (2004)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Beneš, N., Brim, L., Demko, M., Pastva, S., Šafránek, D. (2016). Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-affine Systems. In: Artho, C., Legay, A., Peled, D. (eds) Automated Technology for Verification and Analysis. ATVA 2016. Lecture Notes in Computer Science(), vol 9938. Springer, Cham. https://doi.org/10.1007/978-3-319-46520-3_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-46520-3_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-46519-7
Online ISBN: 978-3-319-46520-3
eBook Packages: Computer ScienceComputer Science (R0)