Meetings

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

• Video

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^)

Compositional Reinforcement Learning from Logical Specifications

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

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

Topic: Compositional Reinforcement Learning from Logical Specifications.

Speaker: Suguman Bansal, NSF/CRA Computing Innovation Postdoctoral Fellow at the University of Pennsylvania.

Abstract

We study the problem of learning control policies for complex tasks given by logical specifications. Recent approaches automatically generate a reward function from a given specification and use a suitable reinforcement learning algorithm to learn a policy that maximizes the expected reward. These approaches, however, scale poorly to complex tasks that require high-level planning. In this work, we develop a compositional learning approach, called DIRL, that interleaves high-level planning and reinforcement learning. First, DIRL encodes the specification as an abstract graph; intuitively, vertices and edges of the graph correspond to regions of the state space and simpler sub-tasks, respectively. Our approach then incorporates reinforcement learning to learn neural network policies for each edge (sub-task) within a Dijkstra-style planning algorithm to compute a high-level plan in the graph. An evaluation of the proposed approach on a set of challenging control benchmarks with continuous state and action spaces demonstrates that it outperforms state-of-the-art baselines.

This is joint work with Kishor Jothimurugan, Osbert Bastani, and Rajeev Alur.

Short Bio

Suguman Bansal is an NSF/CRA Computing Innovation Postdoctoral Fellow in the Department of Computer and Information Sciences at the University of Pennsylvania. Her research interests lie at the intersection of Artificial Intelligence and Formal Methods. Specifically, she works on developing tools and techniques for the automated synthesis of computational systems that also offer formal guarantees of correctness.

She received her Ph.D. (2020) and M.S. (2016) in Computer Science from Rice University, and B.S. (with Honors) degree ( 2014) in Mathematics and Computer Science from Chennai Mathematical Institute. She is the recipient of the NSF CI Fellowship 2020, Future Faculty Fellowship 2019, EECS Rising Stars 2018, Andrew Ladd Fellowship 2016, and a Gold Medal at the ACM Student Research Competition at POPL 2016.

Material

• Video
• Slides (restricted access)

Natural Strategic Ability

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

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

Topic: Natural Strategic Ability.

Speaker: Vadim Malvone, Associate Professor in the Department of Computer Science and Networks (INFRES) of Télécom Paris.

Abstract

In game theory, as well as in the semantics of game logics, a strategy can be represented by any function from states of the game to the agent’s actions. That makes sense from the mathematical point of view, but not necessarily in the context of human behavior. This is because humans are quite bad at executing complex plans, and also rather unlikely to come up with such plans in the first place. In this work, we adopt the view of bounded rationality, and look only at “ simple” strategies in specifications of agents’ abilities. We formally define what “simple” means, and propose a variant of alternating-time temporal logic that takes only such strategies into account. We also study the model checking problem for the resulting semantics of ability.

Short Bio

Vadim Malvone is an Associate Professor in the Computer Science and Networks department (INFRES) of Télécom Paris. From November 2017 to June 2020, he was a postdoctoral researcher at the University of Evry under the supervision of Francesco Belardinelli. In February 2018, he obtained my Ph.D. in Computer Science at the University of Naples “Federico II”, with a thesis titled “Strategic Reasoning in Game Theory”, developed under the supervision of Aniello Murano. During his Ph.D. program, he was a visiting researcher at the Polish Academy of Sciences, under the supervision of Wojtek Jamroga. In July 2014, Vadim obtained his Master’s degree in Computer Science, with a thesis titled “Graded modalities in strategic reasoning” , developed under the supervision of Aniello Murano and Fabio Mogavero.

Material

• Paper
• Video (Passcode 8Mhk?9A2)

A Unifying Framework for Observer-Aware Planning: Non-Markovian Reward Perspective

When: Thursday, May 27, 2021, 3pm (CEST).

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

Topic: A Unifying Framework for Observer-Aware Planning: Non-Markovian Reward Perspective.

Speaker: Shuwa Miura, PhD student at the University of Massachusetts Amherst, supervised by Shlomo Zilberstein.

Abstract

Being aware of observers and the inferences they make about an agent’s behavior is crucial for successful multi-agent interaction. Existing works on observer-aware planning use different assumptions and techniques to produce observer-aware behaviors. We introduce a unifying framework for producing observer-aware behaviors called Observer-Aware MDP (OAMDP). We provide initial empirical evidence that OAMDPs can be used to improve interpretability of agent behaviors and establish complexity results for polynomial-horizon OAMDPs. OAMDP defines a particular class of non-Markovian Reward Decision Processes. Most previous work on non-Markovian reward have used a temporal logic over finite histories to describe non-Markovian rewards. We show complexity results for polynomial-horizon non-Markovian Reward Decision Processes with temporal logic, analogous to the results for OAMDP. We then discuss possible directions for future research.