David Jaz Myers Mirco Giacobbe Diptarko Roy 2025 2 7 https://forest.topos.site/djm-00CP/ https://forest.topos.site/djm-00CP /djm-00CP/ On the representability of Lyapunov-type functions section This is a note to write down ideas generated during the ARIA Safeguarded AI workshop in York, Feb. 3 - 7 2025. These ideas were the result of collaboration with Mirco Giacobbe and Diptarko Roy.In short, the main observation of this note is that the Lyapunov-type functions which witness the satisfaction of LTL formulas concerning non-deterministic discrete-time discrete-space automata are representable in a double categorical systems theory of such automata, nicely matching my proposal for assume-guarantee reasoning via tight bimodules between systems theories (in this case, a restriction of the tight-hom bimodule of the aforementioned systems theory). As a result, I have a proposal for the general shape of the compositionality of Lyapunov-type functions, which I hope will be a useful guide in future collaboration with Mirco and Dip aiming towards the development of a fully compositional theory of Lyapunov-type guarantees on system behavior.I will adopt the terminology and point of view of my book, specifically the first three chapters, for the rest of this note.We begin with a generalization of the double category of Spivak lenses, also known as the "Grothendieck double construction" of the indexed category in my ACT 2020 paper (see also Definition 3.5.0.6 of my book), to allow for inequations in the notion of morphism of systems. If you aren't deep into categories, feel free to skip to definition below.David Jaz Myers202527https://forest.topos.site/djm-00CQ/https://forest.topos.site/djm-00CQ/djm-00CQ/double category of lenses and colax squares.constructionLet be a 2-category (strictly) indexed by a 1-category . We define the strict double category of charts, lenses, and colax squares as follows: The tight category of is the Grothendieck construction of the indexed category of the underlying indexed category of . The loose category of is the Grothendieck construction of the indexed category of the pointwise opposite of the underlying indexed category of . A square =4pt, Rightarrow, from=0, to=1] \end {tikzcd} ]]> consists of a commuting square as on the left and a 2-cell in as on the right: =11pt, Rightarrow, from=1-5, to=2-3] \arrow ["{f_1^{\flat }}", from=1-5, to=2-5] \arrow ["{j_2}"', from=2-1, to=2-2] \arrow [Rightarrow, no head, from=2-3, to=2-4] \arrow ["{f_1^{\ast }j_2^{\sharp }}"', from=2-4, to=2-5] \end {tikzcd} ]]> Composition of squares is given by whiskering in the appropriate direction. For loose composition of the following squares =4pt, Rightarrow, from=0, to=2] \arrow ["\beta ", shorten <=4pt, shorten >=4pt, Rightarrow, from=1, to=3] \end {tikzcd} ]]> we form the whisker as in the following diagram: =13pt, Rightarrow, from=1-3, to=2-1] \arrow ["{j_1^{\ast }f_2^{\flat }}"', from=1-3, to=2-3] \arrow ["\alpha "', shorten <=11pt, shorten >=11pt, Rightarrow, from=1-5, to=2-3] \arrow ["{f_1^{\flat }}", from=1-5, to=2-5] \arrow [Rightarrow, no head, from=2-1, to=2-2] \arrow [Rightarrow, no head, from=2-1, to=3-1] \arrow ["{j_1^{\ast }f_2^{\ast }j_4^{\sharp }}"', from=2-2, to=2-3] \arrow [Rightarrow, no head, from=2-3, to=2-4] \arrow [Rightarrow, no head, from=2-3, to=3-3] \arrow ["{f_1^{\ast }j_2^{\sharp }}"', from=2-4, to=2-5] \arrow [Rightarrow, no head, from=2-5, to=3-5] \arrow ["{j_2^{\ast }f_1^{\ast }j_4^{\sharp }}"', from=3-1, to=3-3] \arrow ["{f_1^{\ast }j_2^{\sharp }}"', from=3-3, to=3-5] \end {tikzcd} ]]> For tight composition of squares: =4pt, Rightarrow, from=0, to=1] \arrow ["\beta ", shorten <=4pt, shorten >=4pt, Rightarrow, from=1, to=2] \end {tikzcd} ]]> we form the whisker as in the following diagram: =14pt, Rightarrow, from=1-3, to=2-1] \arrow ["{f_1^{\flat }}", from=1-3, to=2-3] \arrow [Rightarrow, no head, from=2-1, to=2-2] \arrow ["{j_1^{\ast }f_2^{\ast }f_4^{\flat }}"', from=2-1, to=4-1] \arrow ["{f_1^{\ast }j_2^{\sharp }}"', from=2-2, to=2-3] \arrow ["{f_1^{\ast }j_2^{\ast }f_4^{\flat }}"', from=2-2, to=3-2] \arrow ["{f_1^{\ast }\beta }"', shorten <=9pt, shorten >=9pt, Rightarrow, from=2-3, to=4-2] \arrow ["{f_1^{\ast }f_4^{\flat }}", from=2-3, to=4-3] \arrow [Rightarrow, no head, from=3-2, to=4-2] \arrow [Rightarrow, no head, from=4-1, to=4-2] \arrow ["{f_1^{\ast }f_3^{\ast }j_3^{\sharp }}"', from=4-2, to=4-3] \end {tikzcd} ]]> Checking the associativity and interchange laws is straightforward but tedious. Dually, we define to be the double category of lenses and lax squares: =11pt, Rightarrow, from=2-3, to=1-5] \arrow [Rightarrow, no head, from=2-3, to=2-4] \arrow ["{f_1^{\ast }j_2^{\sharp }}"', from=2-4, to=2-5] \end {tikzcd} ]]>With construction in hand, we are able to define the systems theory of interest: non-deterministic discrete-time discrete-space Moore machines.David Jaz Myers202527https://forest.topos.site/djm-00CR/https://forest.topos.site/djm-00CR/djm-00CR/non-deterministic discrete-time discrete-space Moore machinesdefinitionLet whose underlying indexed category sends a set to the bi-kleisli category of the comonad over the powerset monad (see Definition 2.6.4.1 and Theorem 2.6.4.5 of Reference ), equipped with a 2-category structure of pointwise containment: for . Define the double category of -arenas to be the double category with its feet replaced (Theorem 3.1.1 of Reference ) by the deterministic charts (the inclusion of the Grothendieck construction of the category of determinsitic charts (Definition 3.3.0.1 of Reference )). We define the systems theory of non-deterministic discrete-time discrete-space Moore machines (henceforth, "-machines" for short) to be the systems theory with interface double category associated to the section of the indexed category . Explicitly: A -machine is a lens (loose morphism of ) of the form , which explicitly consists of two maps We say that is the interface of the system . (See Definition 2.1.0.1 of Reference .) A morphism of such systems (also known as a refinement) is a square =4pt, Rightarrow, from=0, to=1] \end {tikzcd} ]]> in . Explicitly, this consists of a deterministic chart , together with a map on states so that For all states , we have . For all and , we have (Compare these conditions to those of Definition 3.3.0.4 of Reference for deterministic automata.) This notion of systems theory is a slight generalization of the one which appears in my book; namely, the morphisms involve a containment rather than an equality. This allows more maps between systems to be morphisms, and enables us to see more concepts as representable.As a warmup, before getting into the representability of Lyapunov functions, let's see how traces of -machines are representable by a simple system.David Jaz Myers202528https://forest.topos.site/djm-00CS/https://forest.topos.site/djm-00CS/djm-00CS/traces of -machinesdefinitionLet be a -machine. Given a sequence of inputs and a sequence of outputs, a -trace of is a sequence of states so that For all , . For all , .David Jaz Myers202528https://forest.topos.site/djm-00CU/https://forest.topos.site/djm-00CU/djm-00CU/The clock -machinedefinitionDefine the clock -machine as follows: The set of states of the clock system is , the natural numbers. We output the time , and take no input (more precisely, the clock takes in a dummy input symbol ). We expose the entire state, taking . The update deterministically ticks the clock.David Jaz Myers202528https://forest.topos.site/djm-00CT/https://forest.topos.site/djm-00CT/djm-00CT/traces of -machines are representable by the clock systemtheoremtraces of -machines are representable by the clock -machine.David Jaz Myers202528https://forest.topos.site/djm-00CT-proof/https://forest.topos.site/djm-00CT-proof/djm-00CT-proof/proof of theorem .proofA morphism to a system consists of (as described in definition ): A chart , which consists of maps and . We note that is equivalently a sequence . A map giving a sequence of states. and this data is required to satisfy the two conditions for all (and , which we can elide): The last condition is an over-wrought way of saying that . Therefore, such maps are precisely traces. Note that the chart of a trace specifies the sequence of inputs, a necessary component to understand the system behavior. We'll see that the Lyapunov-style functions are representable, and similarly the chart component of that representability will encode the various goals of a Lyapunov function.Let's begin with the simple case of a Lyapunov function which witnesses that a system evolves towards a goal. Our goal will be to prove that a system eventually reaches some goal .David Jaz Myers202529https://forest.topos.site/djm-00CV/https://forest.topos.site/djm-00CV/djm-00CV/reach Lyapunov functiondefinitionLet be a -machine. A labelling of outputs consists of a family of goal subsets for each . Given a labelled , a reach Lyapunov function for is a map satisfying the following condition: For all and , if then Usually, we would not allow for different goals on every input; we would want for a fixed goal set for all inputs. The generalization is suggested by the coming representability result, and could play a role in compositionality. It's something to watch out for, but I will say later how I think we can restrict ourselves to the case that is constant in .Let's see the representative for the above notion of Lyapunov function.David Jaz Myers202529https://forest.topos.site/djm-00CW/https://forest.topos.site/djm-00CW/djm-00CW/reach spec -machinedefinitionWe define the reach spec -machine as follows: The interface is where is interpreted as the set of boolean expressions in the symbol , up to logical equivalence. We call the elements of the labels. The output set is a singleton . The state space is , the natural numbers. The expose function is the unique such function. The update function is defined by We think of as the condition which the Lyapunov function must satisfy on states labelled by . David Jaz Myers2025210https://forest.topos.site/djm-00CX/https://forest.topos.site/djm-00CX/djm-00CX/reach Lyapunov functions for -machines are representabletheoremFor a -machine , A family of goals for is represented by a chart . Given a goal , a Lyapunov function for this goal is equivalently a map of -machines =5pt, Rightarrow, from=0, to=1] \end {tikzcd} ]]>David Jaz Myers2025213https://forest.topos.site/djm-00DG/https://forest.topos.site/djm-00DG/djm-00DG/Remark on definition remark Now, the point of exhibiting a Lyapunov function is to witness the satisfaction of a system property. If we can exhibit a reach Lyapunov function, then the system should actually reach the goal. At the level of generality expressed above, this is not the case. We need to restrict the kinds of systems involved, and the kinds of maps allowed to go into the representor so that our theorem holds; this follows my proposal for the use of tight bimodules between loose bimodules as the compositional theory of model validation, since these restrictions can be understood as restricting the hom tight-bimodule of -machines, and then constraining which maps appear in it.Let me be clear on that above point: with the definition as given above, we have two issues First, if the system can halt in some state (that is, if for some ), then a Lyapunov function does not guarantee we reach the goal. This is because the condition on a Lyapunov function quantifies over , and is therefore trivially satisfied if that set is empty. This problem is fixed by restricting to systems for which is always non-empty (which is a perfectly good restriction, as the non-empty powerset monad is a submonad of the powerset monad). As remarked on above, we are allowing for a family of goals which can switch with the input . However, to talk about "the" goal, we need this family to be constant in . We therefore want to restrict to labellings for which is constant in . Luckily, such charts which are constant in the top component form a two-sided ideal in the category of charts, and so constitute a sub-bimodule of the hom tight-bimodule of -machines. It's worth thinking very carefully about this, and I haven't yet. Now let's turn to the more general problem of verifying LTL formulas. I will summarize the approach used by Mirco and Dip in their recent paper on Streett martingales; at least, I will give my rough understanding of the approach. Any errors in the following are my own.First, we need to have a tool in our toolbelt: Streett automata.David Jaz Myers2025210https://forest.topos.site/djm-00CZ/https://forest.topos.site/djm-00CZ/djm-00CZ/deterministic Streett automatondefinition A deterministic Streett automaton is a deterministic finite automaton together with a finite set of Streett pairs where are subsets of and a start state . A Streett automaton is considered to run on an infinite trace of its inputs , and it accepts this if for each , the trace of its behavior starting at either visits finitely many times or infinitely many times. David Jaz Myers2025210https://forest.topos.site/djm-00CY/https://forest.topos.site/djm-00CY/djm-00CY/Streett automata recognize the -regular languagesremarkEvery language accepted by a deterministic Streett automaton is -regular, and vice-versa every -regular language is accepted by a determinstic Streett automaton. !Comment: Where do I cite this from? ! David Jaz Myers2025210https://forest.topos.site/djm-00D0/https://forest.topos.site/djm-00D0/djm-00D0/Translation of LTL formulates into -regular languagestheoremThe -words satisfied by a linear time logic formula is an -regular language.David Jaz Myers2025210proofSee this wikipedia page.This is all standard stuff that I just didn't know. More to the point, this stuff is effective --- we can actually compute the Streett automaton that accepts the traces satisfied by an LTL formula in the context .David Jaz Myers2025213https://forest.topos.site/djm-00DE/https://forest.topos.site/djm-00DE/djm-00DE/Lyapunov representor for an LTL formuladefinitionLet be an LTL formula defined over atomic propositions and let be the Streett automaton accepting its satisfied formulas with Streett pairs .Given positive real coefficients 0]]>, we define the Lyapunov representor for as follows: The interface is . The set of states is , the set of -tuples of functions from states on the states of the Streett automaton accepting . The expose function is the unique function , while the update is given by defining to be the set of all tuples such that for all and : If , then . If , then . If , then . 2025213https://forest.topos.site/djm-00DF/https://forest.topos.site/djm-00DF/djm-00DF/explicationLet's see what a map into the Lyapunov representor for an LTL formula looks like.Let be a system. A chart consists of a function , labelling the outputs of this system by sets of propositions in the atomic formula . This takes the role of the observation function from page 8 of Reference ; specifically, we take , presuming that this is actually constant in (following remark ). A map consists of functions , which play the role of the from page 9 of ibid.. I will note at this point that if we need parameter sets also, we can fold them into the definition of the Lyapunov representor as a further exponent, giving us a state space . Such a map is a morphism of systems when for any and , we have Running through the definition of the terms involved, we see that this means that for all and (and, if we kept them in, parameters ), we have: If , then . If , then . If , then . These conditions correspond to conditions (17), (18) and (19) of ibid., page 9, remembering that the post-distribution defined there given by the formula (14) corresponds precisely to, in the possibilistic setting, for . Now that we know that these Lyapunov certificates are representable, double categorical systems theory suggests a way to try and compose these. Let me write that down and muse about what it suggests. I will say that this is not the only thing I could try, it's just the most straightforward. First, let's recall how -machines compose. Suppose we have systems and . A composition pattern which composes and into some new interface is a lens consisting of We say that is a wiring diagram if it just involves product projections and diagonals (duplication and deletion of variables) --- see Chapter 1 of Reference . For simplicity, let's assume that is deterministic, and therefore consists of two functions . Now, consider the following diagram: =16pt, Rightarrow, from=2-1, to=1-2] \arrow ["{{c_1 \choose !} \otimes {c_2 \choose !}}"', "\shortmid "{marking}, from=2-1, to=2-2] \arrow ["\nu "', from=2-1, to=3-1] \arrow ["{{\alpha \choose !}}"', "\shortmid "{marking}, from=2-2, to=2-3] \arrow [equals, from=2-3, to=3-3] \arrow [shorten <=90pt, shorten >=90pt, Rightarrow, from=3-1, to=2-3] \arrow ["{{c_w \choose !}}"', "\shortmid "{marking}, from=3-1, to=3-3] \end {tikzcd} ]]> If we had such a diagram, then we could compose the two Lyapunov functions and (witnessing and respectively) into a third , where is itself meant to be some kind of composite (informed by ) of the two formulas. There are three unknowns in the above diagram: The composite spec , its primitives , and the composite labelling . The composition pattern , which consists of a map (if deterministic, though it could be taken non-deterministic to land in instead). This constrains , since we must be able to extract subsets of and from it. The above right square says that If and are non-deterministic, then the above equation becomes a containment. Note that if is surjective, then the above equation determines ; we could also minimally define a non-deterministic by the above equation on the image of . Finally, must be a Lyapunov function for the composite system . David Jaz Myers2025217https://forest.topos.site/djm-00DH/https://forest.topos.site/djm-00DH/djm-00DH/Special case of a Lyapunov compositionalityexample To get some idea of what we could do here, let's consider a special case. We can fix to be the diagonal, and to be the identity too (which can always be arranged; we aren't obligated to hide any variables). The above right square then forces , which works when . Making these restrictions, let's see what we could use. For simplicitly, let's take to just be the conjunction; we may then take with (that is, many Streett pairs), and so we deduce the following constraints on : For all and satisfying the three conditions of definition for and and , we have If , then If , then If , then These conditions will be satisfied by the sum , setting and . We therefore conclude with the following theorem: David Jaz Myers2025217https://forest.topos.site/djm-00DI/https://forest.topos.site/djm-00DI/djm-00DI/sum of Lyapunov functions is Lyapunov, sometimestheorem Suppose that and are Lyapunov functions witnessing the satisfaction of two LTL formulas, and let be a composition pattern such that for all , and . Define . Then gives a Lyapunov function witnessing on the coupling of with . Note that if we presume that is constant in , then the above condition is trivially satisfied. Therefore, theorem intuitively says that we should just be able to add the Lyapunov functions to witness a conjunction. In general, we can see that a more general compositionality theorem will require us to understand the ways that Streett automata compose according to the composition of their formulas. I would suggest looking first at regular composition, which only uses and ; these composites of formulas can be built functorially out of wiring diagrams for systems, and we should be able to give a functoriality for Streett automata out of this. References Alessandro Abate Mirco Giacobbe Diptarko Roy 2024 https://forest.topos.site/abate-2024-stochastic/ https://forest.topos.site/abate-2024-stochastic /abate-2024-stochastic/ Stochastic Omega-Regular Verification and Control with Supermartingales Reference 10.1007/978-3-031-65633-0_18 David Jaz Myers 2021 https://forest.topos.site/myers-2021-double/ https://forest.topos.site/myers-2021-double /myers-2021-double/ Double Categories of Open Dynamical Systems (Extended Abstract) Reference 10.4204/eptcs.333.11 Kenny Courser 2020 https://forest.topos.site/courser-2020-open/ https://forest.topos.site/courser-2020-open /courser-2020-open/ Open Systems: A Double Categorical Perspective Reference 10.48550/ARXIV.2008.02394 David Jaz Myers https://forest.topos.site/myers-2021-book/ https://forest.topos.site/myers-2021-book /myers-2021-book/ Categorical Systems Theory Reference http://davidjaz.com/Papers/DynamicalBook.pdf Context Backlinks Related David Jaz Myers 2025 2 7 https://forest.topos.site/djm-00CR/ https://forest.topos.site/djm-00CR /djm-00CR/ non-deterministic discrete-time discrete-space Moore machines definition Let whose underlying indexed category sends a set to the bi-kleisli category of the comonad over the powerset monad (see Definition 2.6.4.1 and Theorem 2.6.4.5 of Reference ), equipped with a 2-category structure of pointwise containment: for . Define the double category of -arenas to be the double category with its feet replaced (Theorem 3.1.1 of Reference ) by the deterministic charts (the inclusion of the Grothendieck construction of the category of determinsitic charts (Definition 3.3.0.1 of Reference )). We define the systems theory of non-deterministic discrete-time discrete-space Moore machines (henceforth, "-machines" for short) to be the systems theory with interface double category associated to the section of the indexed category . Explicitly: A -machine is a lens (loose morphism of ) of the form , which explicitly consists of two maps We say that is the interface of the system . (See Definition 2.1.0.1 of Reference .) A morphism of such systems (also known as a refinement) is a square =4pt, Rightarrow, from=0, to=1] \end {tikzcd} ]]> in . Explicitly, this consists of a deterministic chart , together with a map on states so that For all states , we have . For all and , we have (Compare these conditions to those of Definition 3.3.0.4 of Reference for deterministic automata.) David Jaz Myers 2025 2 7 https://forest.topos.site/djm-00CQ/ https://forest.topos.site/djm-00CQ /djm-00CQ/ double category of lenses and colax squares. construction Let be a 2-category (strictly) indexed by a 1-category . We define the strict double category of charts, lenses, and colax squares as follows: The tight category of is the Grothendieck construction of the indexed category of the underlying indexed category of . The loose category of is the Grothendieck construction of the indexed category of the pointwise opposite of the underlying indexed category of . A square =4pt, Rightarrow, from=0, to=1] \end {tikzcd} ]]> consists of a commuting square as on the left and a 2-cell in as on the right: =11pt, Rightarrow, from=1-5, to=2-3] \arrow ["{f_1^{\flat }}", from=1-5, to=2-5] \arrow ["{j_2}"', from=2-1, to=2-2] \arrow [Rightarrow, no head, from=2-3, to=2-4] \arrow ["{f_1^{\ast }j_2^{\sharp }}"', from=2-4, to=2-5] \end {tikzcd} ]]> Composition of squares is given by whiskering in the appropriate direction. For loose composition of the following squares =4pt, Rightarrow, from=0, to=2] \arrow ["\beta ", shorten <=4pt, shorten >=4pt, Rightarrow, from=1, to=3] \end {tikzcd} ]]> we form the whisker as in the following diagram: =13pt, Rightarrow, from=1-3, to=2-1] \arrow ["{j_1^{\ast }f_2^{\flat }}"', from=1-3, to=2-3] \arrow ["\alpha "', shorten <=11pt, shorten >=11pt, Rightarrow, from=1-5, to=2-3] \arrow ["{f_1^{\flat }}", from=1-5, to=2-5] \arrow [Rightarrow, no head, from=2-1, to=2-2] \arrow [Rightarrow, no head, from=2-1, to=3-1] \arrow ["{j_1^{\ast }f_2^{\ast }j_4^{\sharp }}"', from=2-2, to=2-3] \arrow [Rightarrow, no head, from=2-3, to=2-4] \arrow [Rightarrow, no head, from=2-3, to=3-3] \arrow ["{f_1^{\ast }j_2^{\sharp }}"', from=2-4, to=2-5] \arrow [Rightarrow, no head, from=2-5, to=3-5] \arrow ["{j_2^{\ast }f_1^{\ast }j_4^{\sharp }}"', from=3-1, to=3-3] \arrow ["{f_1^{\ast }j_2^{\sharp }}"', from=3-3, to=3-5] \end {tikzcd} ]]> For tight composition of squares: =4pt, Rightarrow, from=0, to=1] \arrow ["\beta ", shorten <=4pt, shorten >=4pt, Rightarrow, from=1, to=2] \end {tikzcd} ]]> we form the whisker as in the following diagram: =14pt, Rightarrow, from=1-3, to=2-1] \arrow ["{f_1^{\flat }}", from=1-3, to=2-3] \arrow [Rightarrow, no head, from=2-1, to=2-2] \arrow ["{j_1^{\ast }f_2^{\ast }f_4^{\flat }}"', from=2-1, to=4-1] \arrow ["{f_1^{\ast }j_2^{\sharp }}"', from=2-2, to=2-3] \arrow ["{f_1^{\ast }j_2^{\ast }f_4^{\flat }}"', from=2-2, to=3-2] \arrow ["{f_1^{\ast }\beta }"', shorten <=9pt, shorten >=9pt, Rightarrow, from=2-3, to=4-2] \arrow ["{f_1^{\ast }f_4^{\flat }}", from=2-3, to=4-3] \arrow [Rightarrow, no head, from=3-2, to=4-2] \arrow [Rightarrow, no head, from=4-1, to=4-2] \arrow ["{f_1^{\ast }f_3^{\ast }j_3^{\sharp }}"', from=4-2, to=4-3] \end {tikzcd} ]]> Checking the associativity and interchange laws is straightforward but tedious. Dually, we define to be the double category of lenses and lax squares: =11pt, Rightarrow, from=2-3, to=1-5] \arrow [Rightarrow, no head, from=2-3, to=2-4] \arrow ["{f_1^{\ast }j_2^{\sharp }}"', from=2-4, to=2-5] \end {tikzcd} ]]> David Jaz Myers 2025 1 23 https://forest.topos.site/djm-00B6/ https://forest.topos.site/djm-00B6 /djm-00B6/ double category of Spivak lenses definition The double category (often just for short) of Spivak lenses (Reference ) for the fibration is defined to be the span construction of the adequate triple associated to : https://forest.topos.site/david-jaz-myers/ https://forest.topos.site/david-jaz-myers /david-jaz-myers/ David Jaz Myers author davidjaz@topos.institute Topos Research UK, Oxford (UK) https://forest.topos.site/diptarko-roy/ https://forest.topos.site/diptarko-roy /diptarko-roy/ Diptarko Roy person https://forest.topos.site/mirco-giacobbe/ https://forest.topos.site/mirco-giacobbe /mirco-giacobbe/ Mirco Giacobbe person Contributions