Synthetic biology aims at the design of biological systems in a systematic way, a process whose hallmark characteristics closely resemble the composition of software: off-the-shelf parts and devices with standard connections, the usual ingredients for assembling components into increasingly complex systems.

Of course, a number of key enabling technologies are specifically biological, for example, DNA sequencing and fabrication. But, on the other hand, there is also a need for new models to cope with the complex and heterogeneous nature of biological systems. In this context, our starting point is to regard a network of interacting genes and proteins as a dynamic system evolving in time according to fundamental laws of reaction, diffusion and transport. These laws govern how a regulatory network, confronted by any set of stimuli, determines the appropriate response of a cell. This information processing system can be described in precise mathematical terms, resorting to state-of-art research on hybrid systems: transition systems, as typically studied in reactive software, but combining discrete, continuous and stochastic features. The corresponding notions of emerging behaviour, and techniques to express, analyse and verify both structural and behavioural properties, may bring a new understanding to this domain.

However, both fundamental and applied research is deeply needed here. On the one hand, such models and techniques are still an open domain. KLEE adopts a specific perspective: that of the theory of coalgebras, popularised as the "mathematics of transition systems" which provides a general way to express, reason and interrelate different notions of transition, shape and behaviour. Hybrid models, however, are notoriously hard to analyse and verify. In particular, there is a lack of tools for combining stochastic and physical constraints and to (automatically) transform non-computational models into efficient computational ones. On the other hand, if components are well understood in Software Engineering, such is not the case in biological systems. Bio devices, no matter how efficiently designed, develop over time highly complex and unforeseen interactions and redundancies.

Thus, the project will focus on:

- The development of coalgebraic models and logics for synthetic biological devices, combining discrete, continuous, stochastic behaviours;
- Their application to the analysis and validation of biological regulatory networks,
- The development of associated computational tools.

- Bio-components

(months: 1-18; Grants: Lic-6-UM) - Coalgebraic semantics for bio-components

(months: 7-30; Grants: Lic-6-UA) - Coalgebraic logics for verification of bio-complex systems

(months: 7-30; Grants: MSc-12-UM) - A reasoning hub for bio-components

(months: 13-36; Grants: MSc-12-UA, Lic-6-UA) - Case-studies in gene regulatory networks

(months: 13-36; Grants: Lic-6-UA)

The project is coordinated at HASLab INESC-TEC, University of Minho, in a partnership with CIDMA, University of Aveiro. It builds on the team's work for the last four years on coalgebraic software components. Given its interdisciplinary nature, a researcher in synthetic biology, in cooperation with the BIOCORE team at INRIA.

- [KLEE18] Proceedings of the First International Symposium Molecular Logic and Computational Synthetic Biology, Santiago, Chile, 17-18 December, 2018. Springer Lecture Notes in Computer Science (volume 11415), 2018. pdf link

- [CFM20] M. Chaves, D. Figueiredo, M. Martins. “Boolean dynamics revisited through feedback interconnections”. Natural Computing, 19(1), pp 29-49, 2020. DOI: 10.1007/s11047-018-9716-8 pdf link
- [GMB19] L. Gomes, A. Madeira, L. S. Barbosa. “Generalising KAT to Verify Weighted Computations”. Sci. Annals of Computer Science, 29 (2), pp 141-184, 2019. DOI: 10.7561/SACS.2019.2.141 pdf link
- [HN20] D. Hofmann, P. Nora. “Hausdorff coalgebras”. Applied Categorical Structures, 28 (5), pp 773-806, Springer, 2020. DOI: 10.1007/s10485-020-09597-8. pdf link
- [GMB20a] L. Gomes, A. Madeira, L. S. Barbosa. “Introducing Synchrony in Fuzzy Automata”. Electronic Notes in Theoretical Computer Science, 348, pp 43-60, 2020. DOI: https://doi.org/10.1016/j.entcs.2020.02.004 pdf link
- [GTBV20] J. D. Guimarães, C. Tavares, L. S. Barbosa, M. I. Vasilevskiy. “Simulation of non-radiative energy transfer in photosynthetic systems using a quantum computer”. Complexity (Special Issue Foundations and Applications of Process-based Modeling of Complex Systems), vol. 2020, Hindawi-Wiley. DOI: https://doi.org/10.1155/2020/3510676 pdf link
- [Bar22] L. S. Barbosa. "Coalgebra for the working software engineer". Jour. Applied Logics, 9 (1), pp 41-92, 2022. URL, pdf link
- [BMMH21] P. Blackburn, M. A. Martins, M. Manzano, A. Huertas. "Exorcising the phantom zone". Information and Computation, Elsevier, 2021, 104754. URL, pdf link
- [CM21] D. Costa, M. A. Martins. "Non-dual modal operators as a basis for 4-valued accessibility relations in Hybrid logic". J. Log. Algebraic Methods Program. 121, pp 100679, 2021. DOI: 10.1007/978-3-030-63882-5_9 pdf link
- [GMB21] L. Gomes, A. Madeira, L. S. Barbosa. "A semantics and a logic for Fuzzy Arden Syntax". Soft Computing, Springer, 25 (9), pp 6789-6805, 2021. DOI: 10.1007/s00500-021-05593-9 pdf link
- [HKM21] R. Hennicker, A. Knapp, A. Madeira. "Observational interpretations of hybrid dynamic logic with binders and silent transitions". J. Log. Algebraic Methods Program. 122, pp 100698, 2021. DOI: 10.1016/j.jlamp.2021.10069 pdf link
- [SMF21] R. Santiago, M. A. Martins, D. Figueiredo. "Introducing fuzzy reactive graphs: a simple application on biology". Soft Computing, Springer, 25 (9), pp 6759—6774, 2021. DOI: 10.1007/s00500-020-05353-1 pdf link
- [OB21] M. Oliveira, L. S. Barbosa. "Quantum Bayesian decision-making". Foundations Sci., Springer, 2021. DOI: https://doi.org/10.1007/s10699-021-09781-6 pdf link
- [BMM22] M. R. F. Benevides, A. Madeira, M. A. Martins. "Graded epistemic logic with public announcement". J. Log. Algebraic Methods Program. 125: 100732, 2022. DOI: 10.1016/j.jlamp.2021.100732 pdf link
- [CSMF22] S. Campos, R. Santiago, M. A. Martins, D. Figueiredo. "Introduction to reversal fuzzy switch graphs". Sci. Comput. Program. 216, pp 102776, 2022. DOI: 10.1016/j.scico.2022.102776 pdf link

- [GJN18] S. Goncharov, J. Jakob, R. Neves. “A semantics for hybrid iteration”. Proc. CONCUR - 29th International Conference on Concurrency Theory, LIPIcs, 118, pp 1-17, 2018. DOI: 10.4230/LIPIcs.CONCUR.2018.22 pdf link
- [GMJB19] L. Gomes, A. Madeira, M. Jain, L. S. Barbosa. “On the Generation of Equational Dynamic Logics for Weighted Imperative Programs”. Proc. ICFEM - 21st International Conference on Formal Engineering Methods. Springer LNCS, 11852, pp 154-169, 2019. DOI: 10.1007/978-3-030-32409-4_10 pdf link
- [GN19] S. Goncharov, R. Neves. “An Adequate While-Language for Hybrid Computation”, Proc. PPDP - 21st International Symposium on Principles and Practice of Programming Languages, ACM, pp 1-15, 2019. DOI: 10.1145/3354166.3354176 pdf link
- [FB18] D. Figueiredo, L. S. Barbosa. “Reactive Models for Biological Regulatory Networks”. Proc. MLCBS – International Symposium on Molecular Logic and Computational Synthetic Biology, Springer LNCS (11415), pp. 74-88, 2018. DOI: 10.1007/978-3-030-19432-1_5 pdf link
- [FRMC19] D. Figueiredo, E. Rocha, M. A. Martins, M. Chaves. “rPrism – A Software for Reactive Weighted State Transition Models”. Proc. HSB19 - Hybrid Systems Biology. HSB 2019. Springer LNCS, 11705, pp 165-174, 2019. DOI: 10.1007/978-3-030-28042-0_11 pdf link
- [G19] L. Gomes. “On the Construction of Multi-valued Concurrent Dynamic Logics”. Proc. DaLí – 2nd International Workshop on Dynamic Logic: New Trends and Applications”. Springer LNCS 12005, pp 218-226, 2019. DOI: 10.1007/978-3-030-38808-9_14 pdf link
- [HKMM19] R. Hennicker, A. Knapp, A. Madeira, F. Mindt. “Behavioural and Abstractor Specifications for a Dynamic Logic with Binders and Silent Transitions”. Proc.DaLí – 2nd International Workshop on Dynamic Logic: New Trends and Applications”. Springer LNCS 12005, pp 209-217, 2019. DOI: 10.1007/978-3-030-38808-9_2 pdf link
- [T19] C. Tavares. “A Dynamic Logic for QASM Programs”. Proc.DaLí – 2nd International Workshop on Dynamic Logic: New Trends and Applications”. Springer LNCS 12005, pp 209-217, 2019. DOI: 10.1007/978-3-030-38808-9_13c pdf link
- [SMCBBT19] L. Southier, M. Mazzetto, D. Casanova, M. Barbosa, L.S. Barbosa, M. Teixeira. “Combining Advantages from Parameters in Modeling and Control of Discrete Event Systems”. Proc. EFTA - 24th IEEE International Conference on Emerging Technologies and Factory Automation, IEEE, pp 370-377, 2019. DOI: 10.1109/ETFA.2019.8869175
- [Bar20] L. S. Barbosa. “Software engineering for quantum advantage”. ICSEW'20: Proceedings of the IEEE/ACM 42nd International Conference on Software Engineering Workshop. pp 427-429, IEEE. DOI: https://doi.org/10.1145/3387940.3392184 pdf link
- [LRBS20] Ai Liu, R. Neves, L. S. Barbosa, Sun Meng. “Effectful Components and Program Equivalence”. WADT 2020, 25th International Workshop on Algebraic Development Techniques (on-line communication), 2020. pdf link
- [GNP20] S. Goncharov, R. Neves, J. Proença. “Implementing Hybrid Semantics: From Functional to Imperative”. 17th International Colloquium on Theoretical Aspects of Computing, Springer Lecture Notes in Computer Science (12545), Springer, pp 262—282, 2020. DOI: 10.1007/978-3-030-64276-1_14 pdf link
- [FNB20] V. Fernandes, R. Neves, L. S. Barbosa. “A type system for simple quantum processes”. Proc. TYPES 2020, 26th International Conference on Types for Proofs and Programs, 2020 (on-line publication). URL, pdf link
- [CSMF20] S. Campos, R. Santiago, M. A. Martins, D. Figueiredo. "Reversal Fuzzy Switch Graphs". Brazilian Symp. On Formal Methods, Springer Lecture Notes in Computer Science (12475), pp 137–154 pdf link
- [BMM21] M. R. F. Benevides, A. Madeira, M. A. Martins. "Proof Calculi to Epistemic Logics with Structured Knowledge". Proc. Fundamentals of Software Engineering. FSEN 2021, Hojjat, H., Massink, M. (eds), Lecture Notes in Computer Science (12818), pp 53-68, 2021. DOI: 10.1007/978-3-030-89247-0_4 pdf link
- [SSB21a] A. Sequeira, L. P. Santos, L. S. Barbosa. "Generalised Quantum Tree Search". Proc IEEE/ACM 2nd International Workshop on Quantum Software Engineering, IEEE pp 39-40, 2021. DOI: 10.1109/Q-SE52541.2021.00015 pdf link
- [SSB21b] A. Sequeira, L. P. Santos, L. S. Barbosa. "Quantum Tree-based Planning". IEEE Access 9, pp 125416-125427, 2021. DOI: 10.1109/ACCESS.2021.3110652 pdf link
- [DN22] F. Dahlqvist, R. Neves. "An Internal Language for Categories Enriched over Generalised Metric Spaces". Proc. 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), pp 16:1-16-18, 2022. DOI: 10.4230/LIPIcs.CSL.2022.16 pdf link

- [F19] Daniel Figueiredo. "Logic foundations and computational tools for synthetic biology". PhD thesis, Univ Aveiro, 2019 pdf link
- [N19] Pedro Nora. "Kleisli dualities and Vietoris coalgebras". PhD thesis, Univ Aveiro, 2019 pdf link
- [T22] Carlos Tavares. "Foundations for Quantum algorithms and Complexity". PhD thesis, Univ Minho, 2022 pdf link
- [G22] Leandro Gomes. "Weighted computations: semantics and program logics". PhD thesis, Univ Minho, 2022 pdf link

- [O19] Michael Oliveira. "On Quantum Bayesian Networks”. MSc dissertation, Univ Minho, 2019 pdf link
- [V19] Vitor Fernandes. "Integration of time in a quantum process algebra". MSc dissertation, Univ Minho, 2019 pdf link
- [S20] Sofia Oliveira. "Flexible molecular alignment: An Industrial case study on quantum algorithmic techniques". MSc dissertation, Univ Minho, 2020 pdf link
- [G20] José Diogo Guimarães. "Simulation of quantum biology: Quantum simulation of photosynthesis". MSc dissertation, Univ Minho, 2020 pdf link
- [A20] André Sequeira. "Quantum-enhanced Reinforcement Learning". MSc dissertation, Univ Minho, 2020 pdf link
- [S21] Jaime Santos. "Quantum Random Walks". MSc dissertation, Univ Minho, 2021 pdf link
- [C21] Ana Cruz. "Paraconsistent Logics". MSc dissertation, Univ Minho, 2021 pdf link