I am currently involved in four different research lines. Most of them involve Petri nets (PN) and Labelled Transition Systems (LTS) in one form or another.
PN and LTS are two kinds of automata suitable for expressing and analysing concurrency. They differ in that PN depict true concurrency, while LTS rely on interleaving semantics. During my graduate studies, I focused on the algebraic structures that one can derive from PN models. PN can be used to describe distributed systems, but also the processes they execute. On PN models of processes, the concurrency relation helps define a closure operator that generates a lattice according to Birkhoff's theorem. On the other hand, the set of regions of elementary systems, generate a different class of algebraic structure that has interesting links to quantum logic.
Several interesting problems are still open regarding the latter, and I regularly take a new shot at trying to solve one or the other. The most notable (and difficult) of these problems is to determine the stability of regional algebras. You can download a short presentation of the problem here.
Colleagues: Luca Bernardinello, Carlo Ferigato, Lucia Pomello
PN and LTS have traditionally been the theoretical ground for formal verification. Formal verification is the field concerned with determining, with mathematical rigour, that a given system satisfies properties of interest. These usually regard aspects that are interesting, even critical, for industrial systems. In general these properties are described in one or another logical language gathered under the class of the so called Temporal Logics (TL). There are different scientific schools addressing this concern. Formal verification refers to a school interested mostly in generic algorithms that allow for verifying any formula of a given TL on LTS. The term Model Checking usually refers to the verification of particular properties on PN, and it usually exploits structural properties of the system to address more specific problems. In this framework, I mostly focus on the verification of non-interference, and my approach is somewhat at the boundary between formal verification and model checking. There are several notions of non-interference, and it has been shown that some are undecidable. I obviously focus on the other ones. In general, the problem is to determine whether an observer that knows the complete structure of a system can infer information on the state of a hidden part by observing an overt part of it. I have developed an algorithm that allows one to detect information breaches in this sense, and I am currently extending it to work on different classes of models. Its original formulation has been published in open access, you can find it here (Algorithm 2).
Colleagues: Görkem Kilinç Soylu, Federica Adobbati
Traditionally, in mathematical logic (and in particular in proof theory) proofs are built by applying rules in some deduction system. Hilbert and Gentzen style calculi describe the rules that allow to reduce a target formula to a set of premise formulas, in such a way that proving the target formula amounts to proving (each or some of) the derived formulas. In this framework, structural rules describe equivalence of formulas with respect to how its subformulas appear. For instance, in a propositional setting, (A and B) is equivalent to (B and A) under the rule of exchange, and the rule of contraction implies that (A and A) is equivalent to simply A. (The equivalence here means that they allow to prove the same formulas). Substructural logics are described by systems that lack one or the other structural rule. When the missing structural rules are contraction, or weakening, the multiplicity of subformulas becomes relevant, and formulas (and even sequents) may be encoded as vectors over the natural numbers. The subformula property ensures that the dimension of such vectors remains bounded. The subformula property states that for each formula that is provable, a proof of it exists that exhibits only its subformulas. This property can be shown of particular logics by describing an appropriate deduction system. The encoding of formulas (or sequents) as vectors straightforwardly encodes the deduction system as a vector addition system, which in turn is essentially just a Petri net. Deciding whether a proof exists for a given formula is easily encoded as the covering problem for unbounded Petri nets. Well Structured Transition Systems are models that are suitable for representing the state space of such systems, and they have been successfully used to determine tight upper bounds for the complexity of the covering problem on several extensions of vector addition systems. (An excellent account by Schmitz and Schnoebelen can be found here.) In this line of research we are testing the limits of these techniques in their application to proof theory. So far, we have abstracted its essential elements, a first draft can be found here.
Colleagues: Revantha (D.R.S.) Ramanayake, Amirhossein Akbar Tabatabai
Guarded Attribute Grammars (GAGs) are a model of computation that is particularly suited for distributed computation, user centric applications, co-inductive data processing, and many more... Despite its many nice features (modular program description, guarded recursion, data-process duality) it has never been particularly popular in the computer science community, and was only shortly effective in the early 90's as a technical artefact for compiling functional languages. While working at Inria, professor Eric Badouel taught me everything there is to know about them, as he was particularly fond of the model. I am now myself trying to push the model, to display its effectiveness both a the theoretical and application levels. You can find an intuitive description of the model here.
Prof. Badouel was leading a project meant to exploit GAGs until his recent retirement, and I have found myself steering the project in new exciting directions since then.
We have developed a prototype that uses this computation paradigm to distribute programs in a simple and straightforward way.
Using a service orchestrator to manage application deployments on arbitrary distributed infrastructures, our prototype lets one write their programs in an easy to use programming language, that is interpreted as a Guarded Attribute Grammar by the engine we have developed. This lets the programmer take care of the application logic, while our prototype will maximise its distribution so as to best exploit the computational resources available. In this project, I need to give particular credit to Joskel Ngoufo Tagueu, who has done an astounding job in its development. The code of the prototype can be found on github, and a short presentation of the project can be downloaded here.
Colleagues: Eric Badouel, Maurice Tchendji Tchoupé, Joskel Ngoufo Tagueu