Abstract
Many biological systems can be modeled as multiaffine hybrid systems. Due to the nonlinearity of multiaffine systems, it is difficult to verify their properties of interest directly. A common strategy to tackle this problem is to construct and analyze a discrete overapproximation of the original system. However, the conservativeness of a discrete abstraction significantly determines the level of confidence we can have in the properties of the original system. In this paper, in order to reduce the conservativeness of a discrete abstraction, we propose a new method based on a sufficient and necessary decision condition for computing discrete transitions between states in the abstract system. We assume the state space partition of a multiaffine system to be based on a set of multivariate polynomials. Hence, a rectangular partition defined in terms of polynomials of the form \((x_i-c)\) is just a simple case of multivariate polynomial partition, and the new decision condition applies naturally. We analyze and demonstrate the improvement of our method over the existing methods using some examples.
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
References
Alur, R., Dang, T., Ivančić, F.: Progress on reachability analysis of hybrid systems using predicate abstraction. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 4–19. Springer, Heidelberg (2003)
Asarin, E., Dang, T., Girard, A.: Reachability analysis of nonlinear systems using conservative approximation. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 20–35. Springer, Heidelberg (2003)
Bak, S., Bogomolov, S., Henzinger, T.A., Johnson, T.T., Prakash, P.: Scalable static hybridization methods for analysis of nonlinear systems. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, Vienna, Austria, pp. 155–164, 12–14 April 2016
Bartocci, E., Corradini, F., Di Berardini, M.R., Entcheva, E., Smolka, S.A., Grosu, R.: Modeling and simulation of cardiac tissue using hybrid I/O automata. Theor. Comput. Sci. 410(33), 3149–3165 (2009)
Bartocci, E., Corradini, F., Entcheva, E., Grosu, R., Smolka, S.A.: Cellexcite: an efficient simulation environment for excitable cells. BMC Bioinform. 9, S–2 (2008)
Bartocci, E., Lió, P.: Computational modeling, formal analysis and tools for systems biology. PLOS Comput. Biol. 12(1), e1004591 (2016)
Bartocci, E., Liò, P., Merelli, E., Paoletti, N.: Multiple verification in complex biological systems: the bone remodelling case study. Trans. Comput. Syst. Biol. 14, 53–76 (2012)
Batt, G., Belta, C., Weiss, R.: Temporal logic analysis of gene networks under parameter uncertainty. Trans. Autom. Control 53(Special Issue), 215–229 (2008)
Batt, G., De Jong, H., Page, M., Geiselmann, J.: Symbolic reachability analysis of genetic regulatory networks using discrete abstractions. Automatica 44(4), 982–989 (2008)
Belta, C., Habets, L.C.: Controlling a class of nonlinear systems on rectangles. Trans. Autom. Control 51(11), 1749–1759 (2006)
Bogomolov, S., Donzé, A., Frehse, G., Grosu, R., Johnson, T.T., Ladan, H., Podelski, A., Wehrle, M.: Guided search for hybrid systems based on coarse-grained space abstractions. Int. J. Softw. Tools Technol. Transf. 18(4), 449–467 (2016). doi:10.1007/s10009-015-0393-y
Bogomolov, S., Frehse, G., Greitschus, M., Grosu, R., Pasareanu, C., Podelski, A., Strump, T.: Assume-guarantee abstraction refinement meets hybrid systems. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 116–131. Springer, Heidelberg (2014)
Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., Grosu, R.: Abstraction-based parameter synthesis for multiaffine systems. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 19–35. Springer, Heidelberg (2015). doi:10.1007/978-3-319-26287-1_2
Cox, D.A., Little, J., O’Shea, D.: Ideals, Varieties and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra. Springer, New York (2007)
Dang, T., Le Guernic, C., Maler, O.: Computing reachable states for nonlinear biological models. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 126–141. Springer, Heidelberg (2009)
Dreossi, T., Dang, T.: Parameter synthesis for polynomial biological models. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, pp. 233–242. ACM (2014)
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)
Habets, L., Collins, P.J., van Schuppen, J.H.: Reachability and control synthesis for piecewise-affine hybrid systems on simplices. IEEE Trans. Autom. Control 51(6), 938–948 (2006)
Habets, L., Van Schuppen, J.H.: A control problem for affine dynamical systems on a full-dimensional polytope. Automatica 40(1), 21–35 (2004)
Habets, L.C.G.J.M., Van Schuppen, J.: A control problem for affine dynamical systems on a full-dimensional simplex. Rep. Probab. Netw. Algorithms 17, 1–19 (2000)
Jiang, Y., Zhang, H., Li, Z., Deng, Y., Song, X., Gu, M., Sun, J.: Design and optimization of multiclocked embedded systems using formal techniques. IEEE Trans. Ind. Electron. 62(2), 1270–1278 (2015)
Jiang, Y., Zhang, H., Zhang, H., Liu, H., Song, X., Gu, M., Sun, J.: Design of mixed synchronous/asynchronous systems with multiple clocks. IEEE Trans. Parallel Distrib. Syst. 26(8), 2220–2232 (2015)
Kloetzer, M., Belta, C.: Reachability analysis of multi-affine systems. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 348–362. Springer, Heidelberg (2006)
Kong, H., Bogomolov, S., Schilling, C., Jiang, Y., Henzinger, T.A., Invariant clusters for hybrid systems. arXiv preprint arXiv: 1605.01450 (2016)
Kong, H., He, F., Song, X., Hung, W.N.N., Gu, M.: Exponential-condition-based barrier certificate generation for safety verification of hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 242–257. Springer, Heidelberg (2013)
Kong, H., Song, X., Han, D., Gu, M., Sun, J.: A new barrier certificate for safety verification of hybrid systems. Comput. J. 57(7), 1033–1045 (2014)
Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: International Conference on Embedded Software, pp. 97–106. ACM (2011)
Sogokon, A., Ghorbal, K., Jackson, P.B., Platzer, A.: A method for invariant generation for polynomial continuous systems. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 268–288. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49122-5_13
Tiwari, A.: Abstractions for hybrid systems. Formal Methods Syst. Des. 32(1), 57–83 (2008)
Tiwari, A., Khanna, G.: Series of abstractions for hybrid automata. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 465–478. Springer, Heidelberg (2002)
Acknowledgments
This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).
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
Kong, H. et al. (2016). Discrete Abstraction of Multiaffine Systems. In: Cinquemani, E., Donzé, A. (eds) Hybrid Systems Biology. HSB 2016. Lecture Notes in Computer Science(), vol 9957. Springer, Cham. https://doi.org/10.1007/978-3-319-47151-8_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-47151-8_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47150-1
Online ISBN: 978-3-319-47151-8
eBook Packages: Computer ScienceComputer Science (R0)