# Research subjects

- Foundations of concurrency theory and Petri nets
- Process discovery
- Asynchronous games on Petri nets
- Region theory and logics for concurrency

We study models and formal techniques for the specification, the analysis
and the synthesis of concurrent and distributed systems, considering
various aspects of modularity such as compositionality, refinement and
abstraction with the aim of preserving behavioural properties. The focus
is mainly on general Petri net theory, concurrent automata and the theory
of regions, in the framework of the theory of categories.

Process discovery consists in synthesizing the model of a process generating a given event log;
an event log consists of ordered sequences of records of occurred events.
In this line of research, we study how to develop, from a given event log,
Petri net models of multi-agent systems in a compositional way such that
the structure of the model explicitly shows the behavior of the individual agents and their interactions,
and in such a way that the correctness is guaranteed by construction.

We use asynchronous games to model the interaction between autonomous
agents.
Each agent may have a different goal, and acts on the system in
order to reach it.
We define the behaviour of each agent through a strategy; a strategy
is winning for an agent if he wins all the plays by following it.
We study how to determine whether a winning strategy exists and how to
synthesize it.
We are also interested in finding classes of logics that can express
useful goals for agents acting on concurrent systems.

The algebraic structure of the local states of a Petri net is an
orthomodular poset, the algebraic model of quantum logic. The main
aim of this research topic is the characterization of the orthomodular
posets generated by the state spaces of net systems and the study of
the relationships between the axiomatic basis founding net theory and
physical theories.