From June 1, The department of Computer Science and Engineering at Chalmers University of Technology and the University of Gothenburg will make changes to the leadership of the CSE faculty. I will serve as the faculty chair, replacing Prof. Richard Johansson. Many Thanks, Richard for the magnificant work! I am looking forward for this new challenge!

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.