Many problems in computational biology can be formalized by using (labelled) graphs. It is then necessary to measure the distance between such models for reasoning on them.
A possible notion of distance relies on graph isomorphism, that is one of the best known problems in computer science and is also the most demanding notion of equivalence between two graphs: essentially, it requires that two given graphs only differ in the names of their nodes. Less demanding notions of equivalence can be devised, by following well-known paths in concurrency theory.
Notably, bisimulation-based equivalences have been proved very fruitful in efficiently checking when two given (labelled) graphs can be considered the same. Furthermore, equivalences can be usually captured by some form of modal logic, that can be then efficiently used to verify equivalences of two systems by well-known automatic techniques known as Model Checking.
In this project, we propose a logic-based approach for facing graph equivalence, ranging from isomorphism to more liberal forms of equivalence. We first aim at devising modal logics able to characterize (labelled) graph isomorphism and other notions of equivalences. In this, we can take inspiration on works done in concurrency both for Labelled Transition Systems and for Event Structures. Once devised the proper logics able to capture the considered equivalences, we aim at adapting known model checking techniques to prove (or disprove) equivalence.
The main application of our results is the calculation of a distance used by some of the project members to measure similarity between given graphs that represent particular aspects of computational biology, like phylogenies or molecular interactions. Such a distance has been so far expressed in term of isomorphism, but less demanding notions can be considered, mostly if their associated proof techniques turn out to be more efficient.
Many logics for equivalences on (labeled) graph-based formalisms have been proposed in the literature so far; we aim at tailoring the proposals that better cope with the kinds of graphs and then adapting the distance devised for biological systems based on isomorphism. Indeed, apart from some recent work of two project members, no logical-based characterization of graph isomorphism has been devised so far. So, a first attempt could be to investigate the many bisimulation-based equivalences for labeled transition systems, automata and event structures, and discover which ones better cope with the kinds of graphs under consideration. Indeed, since the graphs considered for the biological applications have very precise shapes, we think that it should be possible to easily adapt or define new equivalences whose associated logics allow for efficient model checking algorithms.
Furthermore, adapting known equivalences from concurrency theory to the biological formalisms under consideration can also provide new ideas for other distance notions; such new notions could turn out to be more easily characterizable in logical terms and/or more efficient to algorithmically model check. We expect the new distances been defined like to one that relies on isomorphism, but by exploiting a different notion of equivalence. This can easily give rise to a spectrum of graph distances, with some notion implying others, that can be differently used according to the domain of interest. For each of them, we also imagine to provide a set of verification techniques, arising from the modal logics characterizing the various equivalences and their associated model checking algorithms.
We want to stress that members of this research group are within the Interdepartment Center S.T.I.T.C.H. (Sapienza information-based Technology InnovaTion Center for Health https://web.uniroma1.it/stitch/). This is for us a great opportunity to interact with researchers in medicine, who will provide us some interesting real-life scenarios to lead our experiments. Moreover, we interact with the Evolutionary Biology Lab at INRIA, Grenoble, and this puts us in contact with biologists, proposing us many applicative contexts. Furthermore, two project members already collaborate with researchers in Padova university, that are some of the best experts in logics for graph-based formalisms. We are sure that we will be able to take advantage by the relations with these multidisciplinary research areas, both in terms of gaining real-life problems to solve and in terms of verifying the applicability of our solutions.
Because of the practical impact of our research, a fundamental part of the project will be the development and execution of many experiments on real case studies provided by the medical and biology partners. This is a time consuming task that none of the project members can afford. For this reason, we need a research grant to hire a post-doc for one year. Ideally, this person should set up, run and analyze all the experiments. According to the outcomes obtained, this post-doc should also interact with the project members and suggest better notions of distance, of equivalence notions, and/or of model checking techniques. Hence, in principle, this person should have many competencies, ranging from programming skills to more theoretical and foundational ones.
Finally, we observe that our research group has variegated competences, from theoretical computer science to algorithmics, from formal methods to bioinformatics, from network medicine to logics, from parallel systems to wireless networks. This is a richness, because we will have the opportunity to apply techniques used in our original scientific fields to the subject of this project and will be able to retrieve many results present in the literature, hidden under several names and contexts, that have been designed to solve completely different problems. We have already experienced that this approach of meeting all together on a problem, each coming from a different field of computer science, is successful and leads to strong results.