INFINITY 2019

Program

9:05 – 9:10	Welcome CHAIR: Sven Schewe, University of Liverpool, UK
9:15 – 10:15	Sanjay Jain , Nationl University of Singapore Near polynomial time algorithms for Parity Games Abstract: This talk will explain the Quasi Polynomial time algorithm for parity games given by Calude et al (STOC 2017). The run time of this algorithm is O(nlog(m)+6), where $n$ is the number of nodes and $m$ is the number of colours. When parameterized over $m$, the number of colours, the problem is fixed parameter tractable with runtime of O(n5+g(m)), where g(m) is mm+6. This algorithm was improved by Jurdzinski and Lazic (LICS 2017) and Fearnley et al (SPIN 2017) to make it simultaneously in near linear space. Lehtinen (LICS 2018) introduced the notion of register index complexity which is logarithmic in the number of nodes. A parity game with register index complexity k, can be solved in time mO(k) * nO(1) which provides another quasipolynomial time algorithm for parity games.
10:15 – 10:45	Coffee Break
10:45 – 11:45	Lijun Zhang, Institute of Software, China Academy of Sciences Omega-automata learning algorithms and its applications Abstract: Learning-based automata inference techniques have received significant attention from the community of formal system analysis. In general, the primary applications of automata learning in the community can be categorized into two: improving efficiency and scalability of verification and synthesizing abstract system model for further analysis. Most of the results in the literature focus on checking safety properties or synthesizing finite behavior models of systems/programs. On the other side, Büchi automaton is the standard model for describing liveness properties of distributed systems. Unlike the case for finite automata learning, learning algorithms for Büchi automata are very rarely used in our community. In this talk, we present algorithms to learn a Büchi automaton from a teacher who knows an omega-regular language. The algorithm is based on learning a formalism named family of DFAs (FDFAs) recently proposed by Angluin and Fisman. The main catch is that we use a classification tree structure instead of the standard observation table structure. The worst case storage space required by our algorithm is quadratically better than the table-based algorithm. We implement the first publicly available library ROLL (Regular Omega Language Learning), which consists of all omega-regular learning algorithms available in the literature and the new algorithms proposed in this paper. Further, with our tool, we demonstrate how our algorithm can be exploited in classical automata operations such as complementation checking and in the model checking context.
11:45 – 13:00	Lunch Break
13:30 – 14:30	Laure Daviaud, City University of London Solving mean-payoff parity games in pseudo-quasi polynomial time Abstract: Mean-payoff parity games extend parity games, enforcing one of the player to ensure a quantitative objective (minimise some cost) as well as the usual parity condition that Prof. Jain will discuss during the first talk. I will present a pseudo-quasi polynomial time algorithm to solve these games.
14:30 – 15:00	Coffee Break
15:00 – 16:00	Ashutosh Trivedi, University of Colorado Boulder Reinforcement Learning and Formal Requirements Abstract: Reinforcement learning is an approach to controller synthesis where agents rely on reward signals to choose actions in order to satisfy the requirements implicit in reward signals. Oftentimes non-experts have to come up with the requirements and their translation to rewards under significant time pressure, even though manual translation is time-consuming and error-prone. For safety-critical applications of reinforcement learning, a rigorous design methodology is needed and, in particular, a principled approach to requirement specification and to the translation of objectives into the form required by reinforcement learning algorithms. Formal logic provides a foundation for the rigorous and unambiguous requirement specification of learning objectives. However, reinforcement learning algorithms require requirements to be expressed as scalar reward signals. We discuss a recent technique, called limit-reachability, that bridges this gap by faithfully translating logic-based requirements into the scalar reward form needed in model-free reinforcement learning. This technique enables the synthesis of controllers that maximize the probability to satisfy given logical requirements using off-the-shelf, model-free reinforcement learning algorithms.