I have been selected to participate in the 10th Research Leader Initiative REAL10, 2024-2025
Announcement
The initiative is designed for the future research leaders at the University
of Gothenburg and covers leadership, group development, ethics, gender, grant
writing and utilisation. Only 1 out 5 nominations in each department can be selected.
I am happy to be selected to represent the CSE department in this round.
I have been promoted to Associate Professor in Computer Science @ GU on Nov 2023, and I accepted a Senior Lecturer position @ CSE Dept. starting Mar 2024
Announcement
Stay tuned! I will soon announce a Postdoc postion (& maybe a Ph.D position) on Correct-By-Design of Autonomous Systems (Contact me!).
The position will be hosted by the Formal Methods (FM)
research unit and supervised by me. The objective of the project is to
develop novel methods and algorithms for automatic production of correct-by-design
situated autonomous systems. That is, systems that live on autonomous machines
(such as robots) and populate a shared physical space. Such machines can influence
each other by merely moving/modifying the space. Situated Autonomous systems are
expected to operate while co-existing with other machines and/or humans. Thus,
there is a pressing demand to make them safe, reliable, and robust to sudden changes.
A Ph.D position for Correct-By-Design of Autonomous Systems is available 2023 (Contact me!) Project Details
Announcement
The Ph.D. position that I am advertising will be hosted by the Formal Methods (FM)
research unit and supervised by me. The objective of the Ph.D. project is to
develop novel methods and algorithms for automatic production of correct-by-design
situated autonomous systems. That is, systems that live on autonomous machines
(such as robots) and populate a shared physical space. Such machines can influence
each other by merely moving/modifying the space. Situated Autonomous systems are
expected to operate while co-existing with other machines and/or humans. Thus,
there is a pressing demand to make them safe, reliable, and robust to sudden changes.
From Jan 2021, I am the principal investigator of
"synTM:
Synthesis of
Teamwork
Multi-Agent
Systems". Vetenskapsrådet
Abstract
The increasing adoption of robots in industry creates a demand to enable robots to interact in order to
form teamwork Multi-Agent Systems (MAS) - a set of collaborative agents that interact and behave as if
they were a single capable agent, pursuing a set of joint goals. Teamwork MAS are important because of
workload sharing and the fact that the capabilities of a team exceed the ones of an individual.
Correct-by-design techniques that ensure their safety and reliability are emerging, but are not that
advanced. Namely, Reactive Synthesis - the auto-production of correct programs from declarative
specifications - is a viable candidate. It permits producing robust programs with assurances on
correctness and guarantees on meeting design goals. However, reactive synthesis can only be used to
produce either individual robots or co-existing ones that are not collaborative.SynTM will extend reactive
synthesis to enable the development of teamwork MAS. This is important because correct-by-design teamwork
MAS will revolutionize our lives if successfully employed in safety critical systems, e.g., smart
factories and autonomous driving.To pursue our goal, we plan to develop: an interaction formalism with
novel concepts for contextual and coordination events; an interaction-aware specification logic that
generalizes reactivity; synthesis algorithms that produce interacting programs from logical
specifications; and tools for analysis, implementation, and to evaluate the generated code.
Modelling and Verification of Reconfigurable Multi-Agent Systems (Accepted)
Y. Abd Alrahman, N. Piterman
In JAAMAS (the official journal of the International Foundation
for Autonomous Agents and Multi-Agent Systems.) (29 June 2021)
Abstract
We propose a formalism to model and reason about reconfigurable multi-agent systems.
In our formalism, agents 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.
Inspired by existing multi-robot systems, we represent a
system as a set of agents (each with local state),
executing independently and
only influence each other by means of message exchange.
Agents are able to sense their local states and
partially their surroundings.
We extend \ltl to be able to reason explicitly about the intentions of agents in the interaction and their communication protocols.
We also study the complexity of satisfiability and model-checking of this extension.
Yehia Abd Alrahman has been appointed as a
Visiting Scholar in the Simons Institute beginning April 15, 2021.
University of California, Berkely,USA.
Abstract
The Simons Institute for the Theory of Computing is the world's leading venue for collaborative
research in theoretical computer science. Established on July 1, 2012 with a grant of $60 million
from the Simons Foundation, the Institute is housed in Calvin Lab, a dedicated building on the UC
Berkeley campus. The Simons Institute brings together the world's leading researchers in theoretical
computer science and related fields, as well as the next generation of outstanding young scholars, to
explore deep unsolved problems about the nature and limits of computation.
Synthesis of Run-To-Completion Controllers for Discrete Event Systems (Accepted)
Y. Abd Alrahman, V. Braberman and
N. D'Ippolito and
N. Piterman and
S. Uchitel,
American Control Conference 2021 , ACC 2021
May 26-28, 2021, New Orleans, Louisiana, USA.
Abstract
A controller for a Discrete Event System must achieve its goals
despite that its environment being capable of resolving race
conditions between controlled and uncontrolled events.Assuming
that the controller loses all races is sometimes unrealistic.
In many cases, a realistic assumption is that the controller
sometimes wins races and is fast enough to perform multiple actions
without being interrupted. However, in order to model this
scenario using control of DES requires introducing foreign
assumptions about scheduling, that are hard to figure out correctly.
We propose a more balanced control problem, named
run-to-completion (RTC), to alleviate this issue.
RTC naturally supports an execution assumption in
which both the controller and the environment are guaranteed
to initiate and perform sequences of actions, without
flooding or delaying each other indefinitely. We consider
control of DES in the context where specifications are given
in the form of linear temporal logic. We formalize the RTC
control problem and show how it can be reduced to a standard
control problem.
Reconfigurable Interaction for MAS Modelling (Accepted)
Y. Abd Alrahman, G. Perelli, N. Piterman
19thInternational Conference on Autonomous Agents and Multiagent Systems, AAMAS 2020
May 9-13, 2020, Auckland, New Zealand.
Abstract
We propose 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 extend LTL to be able to reason explicitly about
the intentions of the different agents and their interaction protocols. We also
study the complexity of satisfiability and model-checking of this extension.
Programming Interactions in Collective-Adaptive Systems by relying on Attribute-based Communication
(Accepted)
Y. Abd Alrahman, R. De Nicola, M. Loreti
Science of Computer Programming Journal, Sci. Comput. Program.
(2020).
Abstract
Collective adaptive systems are new emerging computational systems consisting of a large number of
interacting components and featuring complex behaviour. These systems are usually distributed,
heterogeneous, decentralised and interdependent, and are operating in dynamic and possibly unpredictable
environments. Finding ways to understand and design these systems and, most of all, to model the
interactions of their components, is a difficult but important endeavour. In this article we propose a
language-based approach for programming the interactions of collective-adaptive systems by relying on
attribute-based communication; a paradigm that permits a group of partners to communicate by considering
their run-time properties and capabilities. We introduce AbC, a foundational calculus for attribute-based
communication and show how its linguistic primitives can be used to program a complex and sophisticated
variant of the well-known problem of Stable Allocation in Content Delivery Networks. Also other
interesting case studies, from the realm of collective-adaptive systems, are considered. We also
illustrate the expressive power of attribute-based communication by showing the natural encoding of other
existing communication paradigms into AbC.
A Distributed API for Coordinating AbC Programs (Accepted)
Y. Abd Alrahman, G. Garbi
International Journal on Software Tools for Technology Transfer, STTT 2020.
Abstract
Collective-adaptive systems exhibit a particular notion of interaction where environmental conditions
largely influence interactions. Previously, we proposed a calculus, named AbC, to model and reason about
CAS. The calculus proved to be effective by naturally modelling essential CAS features. However, the
question on the tradeoff between its expressiveness and its efficiency, when implemented to program CAS
applications, is to be answered. In this article, we propose an efficient and distributed coordination
infrastructure for AbC. We prove its correctness and we evaluate its performance. The main novelty of our
approach is that AbC components are infrastructure agnostic. Thus the code of a component does not specify
how messages are routed in the infrastructure but rather what properties a target component must satisfy.
We also developed a Go API, named GoAt, and an Eclipse plugin to program in a high-level syntax which can
be automatically used to generate matching Go code. We showcase our development through a non-trivial case
study.