=Paper=
{{Paper
|id=Vol-2756/paper6
|storemode=property
|title=Compositional Modeling of Biological Systems in CospanSpan(Graph)
|pdfUrl=https://ceur-ws.org/Vol-2756/paper_6.pdf
|volume=Vol-2756
|authors=Alessandro Gianola,Stefano Kasangian,Desiree Manicardi,Nicoletta Sabadini,Simone Tini
|dblpUrl=https://dblp.org/rec/conf/ictcs/GianolaKMST20
}}
==Compositional Modeling of Biological Systems in CospanSpan(Graph)==
Compositional Modeling of Biological Systems in CospanSpan(Graph)? Alessandro Gianola1,2 , Stefano Kasangian3 , Desiree Manicardi4 , Nicoletta Sabadini4 , and Simone Tini4 1 Free University of Bozen-Bolzano, Italy gianola@inf.unibz.it 2 University of California San Diego (UCSD), USA 3 Università degli Studi di Milano, Italy 4 Università degli Studi dell’Insubria, Italy Abstract. In this paper we investigate the expressiveness of the com- positional formalism of CospanSpan(Graph) in order to model biological systems: first, we provide a compositional and timed description of the combined, complex system of the Heart and a Dual Chamber Pacemaker. Then, we consider as a case study the well-known gene regulation system in the Lac Operon in Escherichia coli. Keywords: Automata · Compositionality · Categories · Open networks · Biological Systems 1 Introduction The CospanSpan(Graph) model, introduced in [14,13], has been shown to model a variety of phenomena from asynchronous circuits to hierarchy, mobility and coordination [11]. The elements of the model are cospans and spans of graphs which here we shall call simply Automata with interfaces. Automata, since the seminal work of McCulloch and Pitts, have become the standard model for the specification and verification of sequential discrete dynamical systems. In recent years we have been assisting to a paradigmatic shift from sequential systems to networks of parallel, interacting components. Various models of automata with product (of states) have been proposed to represent interactions (Zielonka [21], Petri [17]). These models are rather natural, but unfortunately are not com- positional, that is they lack a proper algebra. On the contrary, compositional- ity, i.e. the property of providing an algebraic calculus, is an essential feature of CospanSpan(Graph). In this approach, we provide explicitly operations that combine automata with interfaces and their connectors. Here, the operations can be interpreted in a very natural way as operations on automata with states and transitions, as well as interfaces and conditions. An expression in this algebra represents a hierarchical, reconfigurable network of interacting components. Automata Theory and Biology are very close disciplines, with a long tradition of reciprocal influences [3,15]. Many formalisms for modeling biological systems ? Copyright c 2020 for this paper by its authors. Use permitted under Creative Com- mons License Attribution 4.0 International (CC BY 4.0). 2 A. Gianola et al. have been proposed, mostly based on process algebras (e.g., [6,4]). In this paper we focus on the possibility an algebraic approach using CospanSpan(Graph) for the compositional description of biological systems. This is crucial for perform- ing verifications tasks as well. Specifically, in [9] we gave a rather simple but compositional description of the heart. Here, we provide a complete description of a Dual Chamber Pacemaker following [12,1], but, for the first time, in a com- positional way. So, a complete specification of the Heart-Pacemaker system can be provided. Finally, we consider as an additional case study the well-known gene regulation system in the Lac Operon of the Escherichia coli bacterium and we give a compositional description of it and its functioning. 2 CospanSpan(Graph): an algebraic formalism for automata networks A full description of the algebra of CospanSpan(Graph) and its applications to reconfigurable networks of automata has been provided in a series of papers [14,13,19,11]. The algebra has a categorical flavor, since Span(C) and Cospan(C) were described in a general category C by Benabou in [2]. Here we recall that when C is the category of Graphs, the operations of the algebra correspond in a natural way to operations on automata with interfaces (and their connectors) that extend Kleene’s algebras. Informally, a basic component is an automaton with states and transitions, i.e. a finite graph, plus: (i) a finite set of interfaces (i.e., communication ports); (ii) a selected subset of states, in analogy to ini- tial and final states in classical automata; (iii) every transition has an effect, maybe , on all the interfaces. Hence, it is an open system, not input/output. Suitable operations could be defined on automata with interfaces [14,13]. The main operations are: (i) the tensor product, i.e. two automata in parallel without communication; (ii) the parallel with communication in which two automata can be joined on common interfaces and, for each pair of states, only the transitions that have the same effects on the common interfaces are possible; (iii) a sequen- tial composition of automata through gluing selected states from both automata. Sequential and parallel feedback [11] can be derived from the full algebra. In [14] an informal geometric description was introduced for these operations. For example, the parallel composition of two automata is pictured as: 3 Pacemaker in CospanSpan(Graph) In this section, through the use of timed Cospan-Span(Graph) [5], we provide the model of a pacemaker that communicates with the heart system described in [9]. A pacemaker is a system that promptly supplies electrical impulses to the heart in order to maintain an appropriate heart rate and also ventricular-atrial Modeling of Biological Systems in CospanSpan(Graph) 3 synchrony. Different cardiac problems can occur, hence modern pacemakers are used in different ways: each of them has a different labeling. In particular, we model a Dual Chamber Pacemaker DDD − formalized in [12] using UPPAAL − that stimulates both the atrium and the ventricle. In [12], the Pacemaker DDD is made up of five components: (i) LRI Lower Rate Interval (ii) AVI Atrio-Ventricular Interval (iii) URI Upper Rate Inter- val (iv) PVARP Post Ventricular Atrial Refractory Period and PVAB Post Ventricular Atrial Blanking (v) VRP Ventricular Refractory Period. The next picture shows the pacemaker architecture and the communications with the heart system from [9]. Unlike [12], we add two components for broad- casting transmission: S1 and S2 - respectively for AP and VS - which transmits the signal to different other components simultaneously. The pacemaker shown here was modeled considering the heart in brachycar- dia or with a regular beat − with 80 beats per minute. The constants TAVI, TLRI, TPVARP, TVRP, TURI and TPVAB − described in [12] − which con- trol the duration of the operations, have the following values: (i) TAVI: 150 ms; (ii) TLRI: 1000 ms; (iii) TPVARP: 100 ms; (iv) TVRP: 150 ms; (v) TURI: 400 ms; (vi) TPVAB: 50ms. We adopt the convention Component={labels}, where labels are the proper labels of the interfaces and Component corresponds to the automaton to connect. We describe the AVI component (Figure 1), which maintains the appropri- ate interval between atrial and ventricular activation so it defines the longest interval between an atrial event and a ventricular event. If AVI does not de- tect any ventricular event (VS) after an atrial event (AS, AP), within TAVI, then AVI delivers a ventricular stimulation (VP). AVI has five interfaces: LRI = {ap, }, PVARP = {as, }, S2 = {vs, }, URI = {, 1 , 2 } and S1 = {vp, }. The transitions are: 4 A. Gianola et al. ap, , /, : -1 → 0 , as, /, : -1 → 0 , , /1 , : 0 → 1 , , /2 , : 0 → 1 , , /2 , : 1 → 2 , , /1 , : 1 → 2 ... ... , , /2 , : 149 → 150 , , /1 , : 149 → 150 , , vs/, : 150→ -1 , , /1 , : 150 → 151 , , vs/, : 151 → -1 , , /2 , : 151 → -1 , , /1 , : 151 → 151 , , /, : -1 → -1 Fig. 1. AVI The other components are described in detail in [10]. 4 Lac Operon In this section we formalize in CospanSpan(Graph) the Lactose Operon in the Escherichia coli bacterium, using for the first time a compositional framework. The lactose operon in Escherichia coli is composed of a sequence of genes that are responsible for producing three enzymes for lactose degradation, namely the lactose permease, which is incorporated in the membrane of the bacterium and actively transports the sugar into the cell, the beta galactosidase, which splits lactose into glucose and galactose, and the transacetylase, whose role is marginal. The Lac Operon functionality depends on the integration of two different control mechanisms, one mediated by lactose and the other by glucose. The model, from Modeling of Biological Systems in CospanSpan(Graph) 5 Fig. 2. Lac Operon model [7,16,18], that we consider is depicted in graphical form in Figure 2. The DNA sequence of the Lac Operon (depicted in Figure 2) regulates the production of the enzymes, through the genes LacZ, LacY, LacA. The regulation process is as follows: gene LacI encodes the lac repressor R, which, in the absence of lactose, binds to gene O (the operator). Transcription of structural genes into mRNA is performed by the RNA polymerase enzyme, which usually binds to gene P2 (the promoter) and scans the operon from left to right by transcribing the three structural genes LacZ, LacY and LacA into a single mRNA fragment. When the lac repressor R is bound to gene O (that is, the complex R-O is present) it becomes an obstacle for the RNA polymerase, and transcription of the struc- tural genes is not performed. On the other hand, when lactose is present inside the bacterium, it binds to the repressor thus inhibiting the binding of R to O. This inhibition allows the transcription of genes LacZ, LacY, LacA by the RNA polymerase. A second mechanism is relevant: when glucose is not present, the complex cAMP-CAP, which is present and acting on P1, can increase signifi- cantly the expression of lac genes. A complete description of the Lac Operon will be provided in a future paper, and it is interesting because the role of the Cospan structure is significant in the modeling. 5 Conclusions In this paper we investigated the compositional feature of CospanSpan(Graph) in modelling biological systems. A compositional description of these systems is promising because it can provide effective verification techniques, using tools that have been developed for Span(Graph) [20]. Further developments could be, for example, a different type of pacemaker and the integration of time and probability [8] in the description of the Heart-Pacemaker System. 6 A. Gianola et al. References 1. R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 1994. 2. J. Bènabou. Introduction to Bicategories. Reports of the Midwest Category Semi- nar, 47:1–77, 1967. 3. D. Besozzi, G. Mauri, G. Păun, and C. Zandron. Gemmating P systems: collapsing hierarchies. Theor. Comput. Sci., 296(2):253–267, 2003. 4. L. Cardelli, E. Caron, P. Gardner, O. Kahramanogullari, and A. Phillips. A process model of actin polymerisation. Electron. Notes Theor. Comput. Sci., 229(1):127– 144, 2009. 5. A. Cherubini, N. Sabadini, and R. F. C. Walters. Timing in the Cospan-Span model. Electr. Notes Theor. Comput. Sci., 104:81–97, 2004. 6. F. Ciocchetta and J. Hillston. Process algebras in systems biology. In Proc. of SFM, volume 5016 of LNCS, pages 265–312. Springer, 2008. 7. L. Corolli, C. Maj, F. Marini, D. Besozzi, and G. Mauri. An excursion in reaction systems: From computer science to biology. Theoretical Computer Science, 2012. 8. L. de Francesco Albasini, N. Sabadini, and R. F. C. Walters. The compositional construction of markov processes. Applied Categorical Structures, 19(1):425–437, 2011. 9. A. Gianola, S. Kasangian, D. Manicardi, N. Sabadini, F. Schiavio, and S. Tini. CospanSpan(graph): a compositional description of the heart system. Fundamenta Informaticae, 171 (1-4):221–237, 2020. 10. A. Gianola, S. Kasangian, D. Manicardi, N. Sabadini, and S. Tini. Compositional Modeling of Biological Systems in CospanSpan(Graph) (Extended Version). Tech- nical report, https://gianola.people.unibz.it, 2020. 11. A. Gianola, S. Kasangian, and N. Sabadini. Cospan/Span(Graph): an algebra for open, reconfigurable automata networks. In Proc. of CALCO, pages 2:1–2:17, 2017. 12. Z. Jiang, M. Pajic, S. Moarref, R. Alur, and R. Mangharam. Modeling and ver- ification of a dual chamber implantable pacemaker. In Proc. of TACAS, pages 188–203, 2012. 13. P. Katis, N. Sabadini, and R. Walters. A formalization of the IWIM model. In Proc. of Coordination Languages and Models, volume 1906 of LNCS, pages 267– 283. Springer, 2000. 14. P. Katis, N. Sabadini, and R. F. C. Walters. Span(Graph): A categorial algebra of transition systems. In Proc. of AMAST, pages 307–321, 1997. 15. C. Martı́n-Vide, G.Mauri, G. Paun, G. Rozenberg, and A. Salomaa, editors. Mem- brane Computing, International Workshop, WMC 2003, Tarragona, Spain, July 17-22, 2003, Revised Papers, volume 2933 of Lecture Notes in Computer Science. Springer, 2004. 16. G. Pardini, R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, and S. Tini. Composi- tional semantics and behavioural equivalences for reaction systems with restriction. Theoretical Computer Science, 2014. 17. C. A. Petri and W. Reisig. Petri net. Scholarpedia, 3(4):6477, 2008. 18. F. J. Romero-Campero and M. J. Pérez-Jiménez. Modelling gene expression control using P systems: The lac operon, a case study. Biosyst., 2008. 19. N. Sabadini, F. Schiavio, and R. Walters. On the geometry and algebra of networks with state. Theor. Comput. Sci., 64:144–163, 2017. 20. F. Schiavio. SpanTools. https://sourceforge.net/projects/spantool/. 21. W. Zielonka. Notes on finite asynchronous automata. ITA, 21(2):99–135, 1987.