Meetings


Formal Synthesis of Supervisory Controllers under Linear Temporal Logic Constraints

When: Thursday, October 21, 2021, 3pm (CEST).

Where: Zoom online, check the address in the Google Calendar Event.

Topic: Formal Synthesis of Supervisory Controllers under Linear Temporal Logic Constraints.

Speaker: Ami Sakakibara, Postdoctoral researcher at the Division of Decision and Control Systems, KTH Royal Institute of Technology, Sweden.

Abstract

We consider a supervisory control problem of a discrete event system (DES), which is discrete-state, event-driven dynamical system model, in the presence of uncontrollable events. We aim to design an on-line supervisory controller that enforces the DES to satisfy a complex mission described by an syntactically co-safe linear temporal logic (scLTL) formula. In the precomputation process, we first compute a ranking function on the product automaton of the DES and an acceptor for the specification. The ranking function returns the minimum number of steps required to reach an accepting state from each state and embeds the influence of logical uncertainties modeled by uncontrollable events. We also show how to extend the ranking-function-based approach for different settings such as LTL over finite traces and multi-agent systems. The effectiveness of the proposed method is demonstrated in an illustrative example of a surveillance problem.

Short Bio

Ami Sakakibara is a postdoctoral researcher at the Division of Decision and Control Systems, KTH Royal Institute of Technology, Sweden, collaborating with Prof. Dimos Dimarogonas. She completed her PhD at the Graduate School of Engineering Science, Osaka University, Japan, under the supervision of Prof. Toshimitsu Ushio. Her research interests lie in formal synthesis, supervisory control, game theory, and reinforcement learning.


Automated Creation and Decomposition of Reward Machines for Multiagent Reinforcement Learning

When: Friday, September 24, 2021, 3pm (CEST).

Where: Zoom online, check the address in the Google Calendar Event.

Topic: Automated Creation and Decomposition of Reward Machines for Multiagent Reinforcement Learning.

Speaker: Giovanni Varricchione, PhD Student at Utrecht University.

Abstract

Recent years saw the introduction of reward machines (RM) in reinforcement learning (RL). An RM is a Mealy machine used to define the reward function of learning agents depending on its current state. Intuitively, a state of an RM is a high-level representation of either the agent’s (or team’s if in a multi-agent setting) behavior so far or of the stage of completion of a task. RMs can then be used to easily define rewards. In this talk, I will describe our novel approach that uses RMs and planning to train teams of agents.

I will first present (Neary, Wu, Xu, Topcu in AAMAS 2021), in which a multi-agent setting is considered. To overcome various issues of the setting, like non-stationarity, a team RM is decomposed into multiple ones, one per agent, that are then used to train their corresponding agents. We improve on this work in two ways: (i) by automatically generating the team and individual RMs, and (ii) by training agents using an option-based framework in conjunction with a strategy. We generate high-level uniform strategies using MCMAS, a model checker for multi-agent systems. Given that the strategy obtained is uniform, we can easily generate the agents’ RMs from it, and then use them to train their agents. Finally, as strategies are specified in terms of high-level actions, we can train agents to execute them using options, a known concept in the RL literature. Preliminary results show that the automatically generated RMs lead to similar performance when compared to the hand-crafted ones of Neary et al., and that the main approach of Neary et al. is outperformed by our option-based one.

This talk is based on a joint work with Natasha Alechina, Mehdi Dastani and Brian Logan.

Material


Goal Recognition and Deception of Rational and Irrational Agents

When: Thursday, July 15, 2021, 10am (CEST).

Where: Zoom online, check the address in the Google Calendar Event.

Topic: Goal Recognition and Deception of Rational and Irrational Agents.

Speaker: Sebastian Sardinã, Professor at RMIT University.

Abstract

The plan/activity/intention/goal recognition problem is the task of identifying an agent’s intent by observing its behaviour. Traditionally, the problem has involved matching a sequence of observations to a plan in a pre-defined plan library;the winning plan being the one that “best” matches the observations. Recent developments dispense with the overhead of a plan library and instead—based on the assumption that the observed agent is behaving rationally—take a cost-based approach and use classical planning technology to generate candidate plans as needed over a domain model. In this talk, we will review this cost-based approach to goal recognition and some recent results, both for general task planning and path planning. We will present a preliminary framework of deception, and techniques to handle irrational and deceptive agents when performing goal recognition.

This is a summary of a stream of work done together with Dr. Peta Masters (now at Melbourne University) and has appeared at AAMAS’17, IJCAI’17, JAIR’18, AAMAS’19 and AIJ’21.

Material


Synthesis via Input/Output Separation

When: Thursday, July 8, 2021, 2:30pm (CEST).

Where: Zoom online, check the address in the Google Calendar Event.

Topic: Synthesis via Input/Output Separation.

Speaker: Dror Fried, Senior Lecturer at the Open University of Israel.

Abstract

Decomposition is a commonly used technique in various algorithms in formal methods. When we observe systems that describe a relation between inputs and outputs, a decomposition, or separation, of the system to input and output components seems only natural. Specifically in synthesis, where the challenge is to construct a strategy or a function that is essentially from inputs to outputs. But what sense does it really make? After all, the specification given by the user, is intended to describe an involved relation between the input and output parts. As such, the algorithms obtained so far are designed to exploit this tight correspondence between inputs and outputs towards strategy generation. In this talk I show how we use input/output separation for synthesis in both areas of Boolean functional synthesis and reactive synthesis. For Boolean functional synthesis I describe how to separate every Boolean formula to input and output components. In reactive synthesis I describe applications in which it is natural for the designer to write specifications that separate inputs and outputs. For both areas, I show how to exploit this separation towards more efficient synthesis algorithms. This talk is based on joint works with Gal Amram, Suguman Bansal, Supratick Chackraborty, Lucas Tabajara, Moshe Vardi, and Gera Weiss.

Short Bio

Dror Fried is a senior lecturer (assistant professor) in the Open University of Israel. He did his PhD in Ben-Gurion University in artificial intelligence, and his postdoc in Rice University in formal methods with Moshe Vardi’s CAVR group. His interests include formal methods, logic in computer science and automated reasoning.

Material


Synthesis From Temporal Specifications

When: Thursday, June 24, 2021, 3pm (CEST).

Where: Zoom online, check the address in the Google Calendar Event.

Topic: Synthesis From Temporal Specifications.

Speaker: Nir Piterman, Associate Professor at the University of Gothenburg.

Abstract

In this talk I will present the GR(1) approach to synthesis, the automatic production of designs from their temporal logic specifications. We are interested in reactive systems, systems that continuously interact with other programs, users, or their environment and specifications in linear temporal logic. Classical solutions to synthesis use either two player games or tree automata. I will give a short introduction to the technique of using two player games for synthesis.

The classical solution to synthesis requires the usage of deterministic automata. This solution is 2EXPTIME-complete, is quite complicated, and does not work well in practice. I will present a syntactic approach that restricts the kind of properties users are allowed to write. It turns out that this approach is general enough and can be extended to cover many properties written in practice.

I will survey some results in model-driven development and robot control.

Short Bio

Nir Piterman completed his PhD in 2005 at the Weizmann Institute of Science under the supervision of Amir Pnueli. Between 2005-2007 he was a postdoc in Tom Henzinger’s group in the Ecoloe Polytechnique Federal de Lausanne. Between 2007-2010 he was a research Fellow in Imperial College London working with Michael Huth. Then, he joined the University of Leicester in 2010 as a Lecturer, was promoted to Reader/Associate Professor in 2012. In March 2019 he joined the Department of Computer Science and Engineering at the University of Gothenburg as a Universitets Lektor / Associate Professor.

Material

  • Video (Passcode: X?+96uYw)

Tractable Novelty Exploration over Continuous and Discrete Sequential Decision Problems

When: Thursday, June 17, 2021, 12pm (CEST).

Where: Zoom online, check the address in the Google Calendar Event.

Topic: Tractable Novelty Exploration over Continuous and Discrete Sequential Decision Problems.

Speaker: Nir Lipovetzky, Senior Lecturer in Artificial Intelligence at the University of Melbourne.

Abstract

Sequential decision problems, where an agent is trying to find a sequence of actions to maximise a utility function or to satisfy a goal condition, have been the focus of different research communities. This talk focuses on the latest advances over width-based planning algorithms, which have shown to yield state-of-the-art AI Planners that rely mostly on structural exploration features, rather than goal-oriented heuristics.

Width-based planners search for a solution using a measure of the novelty of states, where states need to be defined over a set of features. It is known that state novelty evaluation is exponential on the cardinality of the set of features. In this talk, I will address two limitations of current width-based planning: 1) How to define state features over continuous dynamics, where the space of features is unbounded, and 2) present new methods to obtain approximations of novelty linear in the cardinality of the set of features instead of exponential.

I will discuss the performance of the resulting polynomial planners over discrete sequential decision problems ( classical planning) and compare over continuous problems with PPO, a state-of-the-art DRL algorithm. The continuous problems are “classical control” benchmarks from openAI gym.

Short Bio

Nir Lipovetzky is a Senior Lecturer in Artificial Intelligence at the School of Computing and Information Systems, The University of Melbourne. He’s a member of the Agent Lab group. He completed his PhD at the Artificial Intelligence and Machine Learning Group, Universitat Pompeu Fabra, under the supervision of Prof. Hector Geffner. Then, he was a research fellow for 3 years under the supervision of Prof. Peter Stuckey and Prof. Adrian Pearce, working on solving Mining Scheduling problems through automated planning, constraint programming and operations research techniques.

His research focuses on how to introduce different approaches to the problem of inference in sequential decision problems, as well as applications to autonomous systems.

Material

  • Video (Passcode 7e5@pNu^)