2019 Automata, Structures, and Verification Pole Day

IRIF's Automata, Structures, and Verification (ASV) pole will hold its annual workshop on Monday, January 21st, in room 3052 of the Sophie Germain building. Participation is open to everybody, and no registration is required.

The workshop will take place in room 3052, of the Sophie Germain building.

IORDANIS KERENIDIS (IRIF)

Title: Quantum algorithms for Machine Learning and Optimization.

Abstract:

We will present recent work on quantum algorithms for optimization and machine learning, including for recommendation systems, classification, clustering, as well as gradient descent and interior point methods. The talk will not assume any prior knowledge of quantum.

DANIELA PETRISAN (IRIF)

Title: A categorical approach to automata

Abstract:

In this talk I will present a systematic approach for understanding various forms of automata minimization. I will explain how to model automata in various categories and what are sufficient conditions to obtain the existence of a minimal automaton/recognizer for a given language. As examples of this unifying framework I will discuss the minimal subsequential transducer, syntactic algebras, but also minimization for a new class of automata called hybrid-set-vector automata.

MAHSA SHIRMOHAMMADI (LIS - Univ. Aix-Marseille & CNRS)

Title: Trace Refinement in Labelled Markov Decision Processes.

Abstract:

In this talk, we consider the trace-refinement problem for labelled Markov decision processes (MDPs). Given two MDPs, the trace-refinement problem asks whether for all strategies of the first MDP there exists a strategy of the second MDP such that the induced labelled Markov chains are trace-equivalent. We show that this problem is decidable in polynomial time if the second MDP is a Markov chain. However, we show that the general trace-refinement problem is undecidable, even if the first MDP is a Markov chain. Decidability of those problems was stated as open in 2008. We further study the decidability and complexity of the trace-refinement problem provided that the strategies are restricted to be memoryless.

JEREMY SIEK (Indiana University)

Title: The State of the Art in Gradual Typing

Abstract:

Gradual typing is an approach for designing programming languages that integrates static and dynamic type checking. Gradual typing gives the programmer fine-grained control over which regions of a program are statically checked and which regions are dynamically checked. Over the last decade, there has been renewed interest in such an integration partly due to the rise in popularity of dynamic languages. But as small programs grow into large programs, so does the need for early error detection and modularity, which is provided by static type checking. Gradual typing provides a practical migration path for dynamically typed programs to become more statically typed. This talk will give a glimpse at the state of the art in gradual typing. It will describe a) the major challenges in the design and implementation of gradually typed languages, b) the research that has addressed many of of these challenges, and c) the open problems that need to be solved. The research in gradual typing spans both theoretical and practical questions, from mechanized metatheory to efficient compilation.

AMAURY POULY (IRIF)

Title: Continuous models of computation: computability, complexity, universality

Abstract:

In 1941, Claude Shannon introduced a continuous-time analog model of computation, namely the General Purpose Analog Computer (GPAC). The GPAC is a physically feasible model in the sense that it can be implemented in practice through the use of analog electronics or mechanical devices. It can be proved that the functions computed by a GPAC are precisely the solutions of a special class of differential equations where the right-hand side is a polynomial. Analog computers have since been replaced by digital counterpart. Nevertheless, one can wonder how the GPAC could be compared to Turing machines.

A few years ago, it was shown that Turing-based paradigms and the GPAC have the same computational power. However, this result did not shed any light on what happens at a computational complexity level. In other words, analog computers do not make a difference about what can be computed; but maybe they could compute faster than a digital computer. A fundamental difficulty of continuous-time model is to define a proper notion of complexity. Indeed, a troubling problem is that many models exhibit the so-called Zeno's phenomenon, also known as space-time contraction.

In this talk, I will present results from my thesis that give several fundamental contributions to these questions. We show that the GPAC has the same computational power as the Turing machine, at the complexity level. We also provide as a side effect a purely analog, machine- independent characterization of P and Computable Analysis.

I will present some recent work on the universality of polynomial differential equations. We show that when we impose no restrictions at all on the system, it is possible to build a fixed equation that is universal in the sense it can approximate arbitrarily well any continuous curve over R, simply by changing the initial condition of the system.

If time allows, I will also mention some recent application of this work to show that chemical reaction networks are strongly Turing complete with the differential semantics.