But it was one thing to release a population
of virtual agents inside a computer's memory to solve a problem. It was another thing to set real agents free in the real world.
During my career I have been carrying research activities in the following projects:
D-SynMA: Distributed Synthesis from Single to Multiple Agents
I work on an ERC Consolidator Project, named D-SynMA: Distributed
Synthesis from Single to Multiple Agents.
We developed a formalism to model and reason about multi-agent systems.
We allow agents to interact and communicate in different modes
so that they
can pursue joint tasks;
agents may dynamically synchronize, exchange data, adapt their
behaviour, and reconfigure their communication interfaces.
The formalism defines a local behaviour based on shared variables and a
global one based on message passing.
We extended LTL to be able to reason explicitly about the intentions
of the different agents and their interaction protocols.
Currently, we are exploiting the interaction mechanisms
in our formalism to conduct verification analysis compositionally.
We want to find a compositional solution to the distributed synthesis problem.
AbC: Attribute-based Communication
We proposed a process calculus, named AbC, to study the behavioural theory
of interactions in collective-adaptive systems by relying on attribute-based
communication. An AbC system consists of a set of parallel components each
of which is equipped with a set of attributes. Communication takes place
in an implicit multicast fashion, and interaction among components is
dynamically established by taking into account connections as determined
by predicates over their attributes. The structural operational semantics
of AbC is based on Labelled Transition Systems that are also used to
define bisimilarity between components. Labelled bisimilarity is in
full agreement with a barbed congruence, defined by relying on simple
basic observables and context closure. The introduced equivalence is
used to study the expressiveness of AbC in terms of encoding aspects
of broadcast channel-based interactions and to establish formal
relationships between system descriptions at different levels of abstraction.
FILIERASICURA: Ensuring safe operation of power distribution grids
I worked on a project to ensure safe operation of power distribution grids.
The idea is that future power grids will comprise a large number of components,
each potentially able to carry out operations autonomously. Clearly, in order
to ensure safe operation of the grid, individual operations must be coordinated among
the different components. Since operation safety is a global property, modelling
component coordination typically involves reasoning about systems at a global
level. In this project, we proposed a language for specifying grid operation
control protocols from a global point of view. We showed how such global
specifications can be used to automatically synthesise local controllers
of individual components, and that the distributed implementation
yielded by such controllers operationally corresponds to the global specification.