Ricerc@Sapienza

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.