Compositional Modeling of Biological Systems in CospanSpan(Graph)?

Abstract

In this paper we investigate the expressiveness of the compositional formalism of CospanSpan(Graph) in order to model biological systems: rst, 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

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 speci cation and veri cation 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 compositional, that is they lack a proper algebra. On the contrary, compositionality, 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, recon gurable network of interacting components.

Automata Theory and Biology are very close disciplines, with a long tradition of reciprocal in uences [ 3,15 ]. Many formalisms for modeling biological systems ? Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). 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 performing veri cations tasks as well. Speci cally, 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 rst time, in a compositional way. So, a complete speci cation 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 recon gurable networks of automata has been provided in a series of papers [ 14,13,19,11 ]. The algebra has a categorical avor, 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 nite graph, plus: (i) a nite set of interfaces (i.e., communication ports); (ii) a selected subset of states, in analogy to initial and nal states in classical automata; (iii) every transition has an e ect, maybe , on all the interfaces. Hence, it is an open system, not input/output. Suitable operations could be de ned 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 e ects on the common interfaces are possible; (iii) a sequential 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 synchrony. Di erent cardiac problems can occur, hence modern pacemakers are used in di erent ways: each of them has a di erent 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 ve components: (i) LRI Lower Rate Interval (ii) AVI Atrio-Ventricular Interval (iii) URI Upper Rate Interval (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 broadcasting transmission: S1 and S2 - respectively for AP and VS - which transmits the signal to di erent other components simultaneously.

The pacemaker shown here was modeled considering the heart in brachycardia or with a regular beat with 80 beats per minute. The constants TAVI, TLRI, TPVARP, TVRP, TURI and TPVAB described in [ 12 ] which control 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=flabelsg, 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 appropriate interval between atrial and ventricular activation so it de nes the longest interval between an atrial event and a ventricular event. If AVI does not detect any ventricular event (VS) after an atrial event (AS, AP), within TAVI, then AVI delivers a ventricular stimulation (VP). AVI has ve interfaces: LRI = fap; g, PVARP = fas; g, S2 = fvs; g, URI = f ; 1; 2g and S1 = fvp; g. The transitions are:

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

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 rst 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 di erent control mechanisms, one mediated by lactose and the other by glucose. The model, from [ 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 structural 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 signi 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 signi cant 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 e ective veri cation techniques, using tools that have been developed for Span(Graph) [ 20 ]. Further developments could be, for example, a di erent type of pacemaker and the integration of time and probability [ 8 ] in the description of the Heart-Pacemaker System.

References

1. R. Alur and D. L. Dill . A theory of timed automata . Theoretical Computer Science , 1994 .

2. J. Benabou . Introduction to Bicategories. Reports of the Midwest Category Seminar , 47 :1{ 77 , 1967 .

3. D. Besozzi , G. Mauri, G. Paun, 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) . Technical report , https://gianola.people.unibz.it, 2020 .

11. A. Gianola , S. Kasangian , and N. Sabadini . Cospan/Span(Graph) : an algebra for open, recon gurable 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 veri cation 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. Membrane 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 . Compositional 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. Perez-Jimenez. 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 nite asynchronous automata . ITA , 21 ( 2 ): 99 { 135 , 1987 .