Abstract
We propose a general framework for the analysis of hybrid automata representing biological systems which interacts with an environment. Our framework is based on unwinding conditions and it aims at establishing which external interactions substantially change the system behaviours. We exploit our proposal for the analysis of influenza disease treatable with both antivirals and interferons.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.H.: Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: On the robustness of temporal properties for stochastic models. In: Proc. of 2nd Int. Workshop on Hybrid Systems and Biology (HSB 2013). EPTCS, vol. 125, pp. 3–19 (2013)
Bossi, A., Piazza, C., Rossi, S.: Compositional information flow security for concurrent programs. Journal of Computer Security 15(3), 373–416 (2007)
Bossi, A., Focardi, R., Piazza, C., Rossi, S.: Bisimulation and unwinding for verifying possibilistic security properties. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 223–237. Springer, Heidelberg (2002)
Brim, L., Vejpustek, T., Safránek, D., Fabriková, J.: Robustness analysis for value-freezing signal temporal logic. In: Proc. of 2nd Int. Workshop on Hybrid Systems and Biology (HSB 2013). EPTCS, vol. 125, pp. 20–36 (2013)
Casagrande, A., Piazza, C., Policriti, A., Mishra, B.: Inclusion dynamics hybrid automata. Inform. and Comput. 206(12), 1394–1424 (2008)
Casagrande, A., Dreossi, T., Piazza, C.: Hybrid automata and ε-analysis on a neural oscillator. In: Proc. of First Int. Workshop on Hybrid Systems and Biology (HSB 2012). EPTCS, vol. 92, pp. 58–72 (2012)
Casagrande, A., Piazza, C.: Unwinding biological systems (April 2014), http://www.dmi.units.it/%7ecasagran/resources/unwinding.pdf (submitted)
Chiang, K., Fages, F., Jiang, J.-H., Soliman, S.: On the hybrid composition and simulation of heterogeneous biochemical models. In: Gupta, A., Henzinger, T.A. (eds.) CMSB 2013. LNCS, vol. 8130, pp. 192–205. Springer, Heidelberg (2013)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)
Dianzani, F., Viano, I., Santiano, M., Zucca, M., Gullino, P., Baron, S.: Tissue culture models of in vivo interferon production and action. In: Human Interferon, pp. 119–131. Springer (1978)
Donzé, A., Ferrère, T., Maler, O.: Efficient robust monitoring for STL. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 264–279. Springer, Heidelberg (2013)
Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92–106. Springer, Heidelberg (2010)
Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science 410(42), 4262–4291 (2009)
Focardi, R., Gorrieri, R.: A taxonomy of security properties for process algebras. Journal of Computer Security 3(1), 5–34 (1995)
Focardi, R., Rossi, S.: Information flow security in dynamic contexts. In: Proc. of 15th IEEE Computer Security Foundations Workshop (CSFW 2002), pp. 307–319. IEEE Computer Society (2002)
Ghosh, R., Tomlin, C.J.: Lateral Inhibition through Delta-Notch Signaling: A Piecewise Affine Hybrid Model. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 232–246. Springer, Heidelberg (2001)
Ghosh, R., Tiwari, A., Tomlin, C.: Automated symbolic reachability analysis; with application to delta-notch signaling automata. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 233–248. Springer, Heidelberg (2003)
Ghosh, R., Tomlin, C.: Symbolic reachable set computation of piecewise affine hybrid automata and its application to biological modelling: Delta-notch protein signalling. Systems Biology 1(1), 170–183 (2004)
Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11–20. IEEE Computer Society Press (1982)
Goujon, C., Moncorgé, O., Bauby, H., Doyle, T., Ward, C.C., Schaller, T., Hué, S., Barclay, W.S., Schulz, R., Malim, M.H.: Human mx2 is an interferon-induced post-entry inhibitor of hiv-1 infection. Nature 502(7472), 559–562 (2013)
Handel, A., Longini, Jr. I.M., Antia, R.: Neuraminidase inhibitor resistance in influenza: assessing the danger of its generation and spread. PLoS Comput. Biol. 3(12), e240 (2007)
Henzinger, T.A.: The Theory of Hybrid Automata. In: Proc. of IEEE Symposium on Logic in Computer Science (LICS 1996), pp. 278–292. IEEE Computer Society Press (1996)
Jacobs, L.D., Cookfair, D.L., Rudick, R.A., Herndon, R.M., Richert, J.R., Salazar, A.M., Fischer, J.S., Goodkin, D.E., Granger, C.V., Simon, J.H., et al.: Intramuscular interferon beta-1a for disease progression in relapsing multiple sclerosis. Annals of Neurology 39(3), 285–294 (1996)
Johnson, N.P.A.S., Mueller, J.: Updating the accounts: global mortality of the 1918-1920 “Spanish” influenza pandemic. Bull. Hist. Med. 76(1), 105–115 (2002)
Julkunen, I., Melén, K., Nyqvist, M., Pirhonen, J., Sareneva, T., Matikainen, S.: Inflammatory responses in influenza a virus infection. Vaccine 19, S32–S37 (2000)
Kitano, H.: Biological robustness. Nature Reviews Genetics 5(11), 826–837 (2004)
Kitano, H.: Towards a theory of biological robustness. Molecular Systems Biology 3(137) (2007)
Lafferriere, G., Pappas, G.J., Sastry, S.: O-minimal hybrid systems. Mathematics of Control, Signals, and Systems 13, 1–21 (2000)
Lynch, N.A., Segala, R., Vaandrager, F.W.: Hybrid i/o automata. Inf. Comput. 185(1), 105–157 (2003)
Maler, O., Manna, Z., Pnueli, A.: From timed to hybrid systems. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 447–484. Springer, Heidelberg (1992)
Milner, R.: A Calculus of Communicating Systems. Springer (1980)
World Health Organization: Influenza fact sheet no. 211 (March 2014), http://www.who.int/mediacentre/factsheets/fs211/en/
Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM Journal on Computing 16(6), 973–989 (1987)
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, October 31-November 2, pp. 46–57. IEEE Computer Society Press (1977)
Pnueli, A.: The temporal semantics of concurrent programs. In: Kahn, G. (ed.) Semantics of Concurrent Computation. LNCS, vol. 70, pp. 1–20. Springer, Heidelberg (1979)
Quesada, J.R., Reuben, J., Manning, J.T., Hersh, E.M., Gutterman, J.U.: Alpha interferon for induction of remission in hairy-cell leukemia. New England Journal of Medicine 310(1), 15–18 (1984)
Rizk, A., Batt, G., Fages, F., Soliman, S.: Continuous valuations of temporal logic specifications with applications to parameter optimization and robustness measures. TCS 412(26), 2827–2839 (2011)
Ryan, P.Y.A., Schneider, S.A.: Process algebra and non-interference. Journal of Computer Security 9(1/2), 75–103 (2001)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)
Saenz, R.A., Quinlivan, M., Elton, D., MacRae, S., Blunden, A.S., Mumford, J.A., Daly, J.M., Digard, P., Cullinane, A., Grenfell, B.T., et al.: Dynamics of influenza virus infection and pathology. Journal of Virology 84(8), 3974–3983 (2010)
Taubenberger, J.K., Morens, D.M.: 1918 Influenza: the mother of all pandemics. Emerging Infectious Diseases 12(1), 15–22 (2006), http://www.ncbi.nlm.nih.gov/pubmed/16494711 , PMID: 16494711
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)
Walther, E., Hohlfeld, R.: Multiple sclerosis side effects of interferon beta therapy and their management. Neurology 53(8), 1622–1622 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Casagrande, A., Piazza, C. (2014). External Interactions on Hybrid Models of Biological Systems. In: Fages, F., Piazza, C. (eds) Formal Methods in Macro-Biology. FMMB 2014. Lecture Notes in Computer Science(), vol 8738. Springer, Cham. https://doi.org/10.1007/978-3-319-10398-3_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-10398-3_6
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10397-6
Online ISBN: 978-3-319-10398-3
eBook Packages: Computer ScienceComputer Science (R0)