Dr. Yehia Abd Alrahman
logo of University of gothenburg Dr. Yehia Abd Alrahman
Göteborgs Universitet
Department of Computer Science and Engineering
Formal Methods Division
Phone: +46 31 772 60 54
Email: Göteborgs Universitet -- Research
Office: EDIT 5483
Address: Rännvägen 6B , 412 96 Göteborgs, Sweden

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.

Research Projects

During my career I have been carrying research activities in the following projects:

D-SynMA: Distributed Synthesis from Single to Multiple Agents

ERC icon
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.