We support the TCS4F — an initiative for reducing the carbon footprint. Learn more...

12–15 SEPTEMBER 2017

Tutorial day: 12 SEPTEMBER
Main Conference: 13–15 SEPTEMBER

edition

 London

The goal of Highlights conferences is to integrate the community working on logic, games and automata.

IMPORTANT DATES

Talk submission deadline: 5 June 2017, 7pm GMT (extended)
Notification: 12 June 2017
Registration deadline: 20 August 2017
Tutorial day: 12 September 2017
Conference: 13-15 September 2017

Registration is now open! closed

If you would still like to register, email the organisers: highlights17@qmul.ac.uk

PREVIOUS EDITIONS

  1. Highlights 2016 (Brussels, 6–9 September)
  2. Highlights 2015 (Prague, 15–18 September)
  3. Highlights 2014 (Paris, 2–5 September)
  4. Highlights 2013 (Paris, 18–21 September)

No proceedings

There are no proceedings. You present your best work, be it published elsewhere or yet unpublished.

Short

The conference is three days long. The contributed talks are around ten minutes.

Cheap

The participation costs are modest. London is easy to reach.

Everybody is doing it!

Let's use the conference model that is so successful in other fields, like mathematics.

Committees

KEYNOTE SPEAKERS

Mikołaj Bojańczyk
Sanjay Jain
Hung Ngo

TUTORIALS

Veronique Cortier
Damien Pous

INVITED SESSIONS

Patricia Bouyer
Alexandra Silva

PROGRAM COMMITTEE

Igor Walukiewicz (chair)
Parosh Aziz Abdulla
Christel Baier
Gilles Barthe
Michael Benedikt
Thomas Colcombet
Javier Esparza
Emmanuel Filiot
Paul Gastin
Mai Gherke
Bartek Klin
Barbara Konig
Antonin Kucera
Rupak Majumdar
David Monniaux
Luke Ong
Catuscia Palamidessi
Madhusudan Parthasarathy
Davide Sangiorgi
Thomas Schwentick
Sophie Tison

ORGANISING COMMITTEE

Matthew Hague (co-chair)
Nikos Tzevelekos (co-chair)
Paulo Oliva
Greta Yorsh
Andrew Lewis-Smith
Yu-Yang Lin

STEERING COMMITTEE

Dietmar Berwanger
Mikołaj Bojańczyk
Tomáš Brázdil
Thomas Colcombet
Anuj Dawar
Hugo Gimbert
Erich Grädel
Christof Löding
Aniello Murano
Moshe Vardi

Call for Presentations

CALL FOR PRESENTATIONS:

HIGHLIGHTS 2017 is the fifth conference on Highlights of Logic, Games and Automata that aims at integrating the community working in these fields. Papers from these areas are dispersed across many conferences, which makes them difficult to follow.

A visit to the Highlights conference should offer a wide picture of the latest research in the field and a chance to meet everybody in the community, not just those who happen to publish in one particular proceedings volume.

We encourage you to attend and present your best work, be it already published or not, at the Highlights conference.

SCOPE:

Representative areas include, but are not restricted to:

  • logic and finite model theory
  • automata theory
  • games for logic and verification

IMPORTANT GUIDELINES:

You submit a proposal for a presentation, not a paper. Hence, submissions should have a single author, who is the speaker. Since we expect you to present your favorite result of the year, there should be at most one submission per speaker. The abstract, of 1-2 pages, may include a list of coauthors.

There are no formal proceedings and we encourage submission of work presented elsewhere.

WHERE AND WHEN TO SUBMIT:

Talk submissions are done via the Highlights 2017 EasyChair site

The submission deadline is June 2, 2017 June 5, 7pm GMT (extended).
Notifications will be sent by June 12, 2017.

Keynote sessions

Keynote talks

Mikołaj Bojańjczyk: A Proof of Courcelle’s Conjecture on Recognisable Graph Classes

Sanjay Jain: Quasi Polynomial and FPT algorithms for parity games

Hung Ngo: Shannon-type inequalities, submodular width, and disjunctive datalog

Invited sessions

Patricia Bouyer: Games played on graphs: quantitative games, games with multi-objectives, non-zero sum games

Alexandra Silva: Model learning, automata and its applications

Tutorials

Veronique Cortier: Verification of security protocols

Damien Pous: Coinduction up to and automata algorithms

Venue

LOCATION

Highlights will take place in the Mile End campus of Queen Mary University of London. It will be located in particular in the People’s Palace (building n.16 in this campus map).

The closest tube stations are Stepney Green and Mile End. For travel planning to the venue we recommend using the “directions” option in this google map. You can use the postal code E1 4NS to locate the campus.

EATING

There are several options for eating or having a drink near Queen Mary. The cheapest option is the pub The Half Moon on Mile End Road situated between Queen Mary and Stepney Green Station. Nearby is the Turkish restaurant Efes (230 Mile End Road), and the more expensive but good quality Italian restaurant Verdi (237 Mile End Road).

Near Mile End Tube Station there is the chain chicken restaurant Nando’s (552 Mile End Road), the burger locale Greedy Cow (2 Grove Rd), the reasonably priced Persian restaurant Ariana (2 Midlothian Road) and The Morgan Arms (gastro pub, 43 Morgan Street).

There is an abundance of eating options throughout London, with good restaurants to be found in and around Brick Lane, Shoreditch, Soho, and beyond.  For the more well-known options, book ahead if possible, or expect to wait on the door.

ACCOMMODATION

We know of the following hotels that are reachable on foot in ~20 mins:

Moreover, there is a plethora of hotels easily reachable by tube from Queen Mary, especially in the Stratford Olympic park area (one stop from Mile End on the Central line — note this is London Stratford, not Shakespeare’s Stratford-upon-Avon!).

Finally, you may want to consider more affordable options like Airbnb (use usual caution when booking).

PUBLIC TRANSPORT

The best way to travel on the public transport system in London is by using a “contactless” credit card. The second best option is to purchase an Oyster card for a small deposit. This is a pay-as-you-go card which you can buy at tube stations or online (this service delivers the card to your home country). You can still buy single paper tickets but: (a) they are way more expensive, and (b) you cannot use them on buses.

There is no official London transport mobile app. The TfL Journey Planner website works well on mobile. Citymapper is a popular 3rd party travel app.

The cheapest travel option is to cycle to/from Queen Mary using city bikes. There are several docking stations around Queen Mary and the cycle superhighways offer routes largely segregated from traffic. The scheme costs £2 per 24 hours and you can make an unlimited number of journeys each lasting less than 30 minutes. Check their website for all details. There are thousands of available bikes all over London, however if your hotel is east of Queen Mary check on the map if there are docking stations nearby.

SOCIAL EVENTS

Pizza dinner

Wednesday 13 September, time 19:30
One Sixty City, 9 Stoney Lane, London E1 7BH

Directions from Queen Mary: District or Hammersmith and City line from Stepney Green to Aldgate East, then a short walk. Alternatively, bus 25 or 205 from Queen Mary University of London to Aldgate East.

Please ask the organisers if you would like to join.

Picnic

Thursday 14 September, time 19:00
Mile End Park, open space next to the Palm Tree pub

Directions from Queen Mary: follow the organisers.

NEARBY

Reachability Problems 2017
Royal Holloway University of London
7-9 September 2017
RP 2017

Programme

12

Tuesday 12 September

Registration

Tutorial

  • Damien Pous - Coinduction up to and automata algorithms: Coinduction up to and automata algorithms

    Authors: Damien Pous

    Abstract:

coffee

Tutorial

  • Damien Pous - Coinduction up to and automata algorithms: Coinduction up to and automata algorithms

    Authors: Damien Pous

    Abstract:

lunch

Tutorial

  • Veronique Cortier: Verification of security protocols

    Authors: Veronique Cortier

    Abstract:

    Cryptographic protocols aim at securing communications over insecure networks like the Internet. Over the past decades, numerous decision procedures and tools have been developed to automatically analyse the security of protocols. The field has now reached a good level of maturity with efficient techniques for the automatic security analysis of protocols. In this tutorial, after an overview of some famous protocols and flaws, we will explain how to formally model protocols and security properties and we will describe associated decision procedures.

coffee

Tutorial

  • Veronique Cortier: Verification of security protocols

    Authors: Veronique Cortier

    Abstract:

    Cryptographic protocols aim at securing communications over insecure networks like the Internet. Over the past decades, numerous decision procedures and tools have been developed to automatically analyse the security of protocols. The field has now reached a good level of maturity with efficient techniques for the automatic security analysis of protocols. In this tutorial, after an overview of some famous protocols and flaws, we will explain how to formally model protocols and security properties and we will describe associated decision procedures.

13

Wednesday 13 September

Invited Talk

  • Sanjay Jain - Quasi Polynomial and FPT algorithms for parity games: Quasi Polynomial and FPT algorithms for parity games

    Authors: Sanjay Jain

    Abstract:

    It is shown that parity games can be solved in quasipolynomial time. The runtime is improved from the previously best known n^O(sqrt(n)) to O(n^(log(m)+6)), where n is the number of nodes and m is the number of colours (priorities). The parameterised parity game — with n nodes and m distinct colours is proven to be in the class of fixed parameter tractable problems (FPT) when parameterised over m. The corresponding runtime is improved from O(n^Θ(m)) for fixed parameter m to an FPT-algorithm with runtime O(n^5+g(m)), where g(m) can be taken to be m^(m+6).

coffee

Games, logical theories

  • Marcin Jurdzinski and Ranko Lazic: Succinct progress measures for solving parity games

    Authors: Marcin Jurdzinski and Ranko Lazic

    Abstract:

    Abstract available in PDF.

  • John Fearnley: An Ordered Approach to Solving Parity Games in Quasi Polynomial Time and Quasi Linear Space

    Authors: John Fearnley, Sanjay Jain, Sven Schewe, Frank Stephan, and Dominik Wojtczak

    Abstract:

    Abstract available in PDF.

  • Quentin Hautem: Games with lexicographically ordered omega-regular objectives

    Authors: Quentin Hautem

    Abstract:

    Abstract available in PDF.

  • Nathanaël Fijalkow: Boundedness Games

    Authors: Nathanaël Fijalkow

    Abstract:

    Boundedness games are two player games played on graphs equipped with counters, where the winning condition for the first player is to ensure that the values of the counters remain bounded. They appeared in various contexts in the study of boundedness logics, in particular MSO + U by Bojanczyk and cost-MSO by Colcombet. Prominently, it was shown by Colcombet and Loeding that proving a finite-memory determinacy for boundedness games would imply the decidability of the Mostowski index problem for modal-mu calculus, a decades old open problem. The objective is this presentation is to report on the most recent results on boundedness games, and in particular on the decidability of a new special case of the Mostowski index problem.

  • Dmitry Chistikov: On the complexity of quantified integer programming

    Authors: Dmitry Chistikov and Christoph Haase

    Abstract:

    Quantified integer programming is the the problem of deciding assertions of the form “Q x_k … forall x_2 exists x_1 : A x geq c” where vectors of variables x_k, …, x_1 form the vector x, all variables are interpreted over N (alternatively, over Z), and A and c are a matrix and vector over Z of appropriate sizes. We show that quantified integer programming with alternation depth k is complete for the k-th level of the polynomial hierarchy. Abstract available in PDF.

  • Murdoch Gabbay: Interleaved scope for games and automata

    Authors: Murdoch Gabbay

    Abstract:

    Abstract available in PDF.

break

Transducers

  • Luc Dartois: On Reversible Transducers

    Authors: Luc Dartois

    Abstract:

    Abstract available in PDF.

  • Gabriele Puppis: Untwisting two-way transducers in elementary time

    Authors: Gabriele Puppis

    Abstract:

    Abstract available in PDF.

  • Bruno Guillon: Which classes of origin graphs are generated by transducers?

    Authors: Bruno Guillon

    Abstract:

    Abstract available in PDF.

  • Johanna Björklund: Tree-to-graph transductions

    Authors: Johanna Björklund

    Abstract:

    Abstract available in PDF.

  • Henrik Björklund: Order-Preserving DAG Grammars: Parsing, Complexity, and Learning

    Authors: Henrik Björklund

    Abstract:

    Abstract available in PDF.

  • Nathan Lhote: A Decidable Logic for Transductions with Regular Synthesis

    Authors: Nathan Lhote

    Abstract:

    Abstract available in PDF.

lunch

Separability, max-plus automata

  • Sławomir Lasota: Nondeterminism does not make regular separability harder

    Authors: Sławomir Lasota

    Abstract:

    Abstract available in PDF.

  • Lorenzo Clemente: Regular Separability of Parikh Automata

    Authors: Lorenzo Clemente

    Abstract:

    Abstract available in PDF.

  • Wojciech Czerwiński: Regular Separability of One Counter Automata

    Authors: Wojciech Czerwiński

    Abstract:

    Abstract available in PDF.

  • Nicolas Mazzocchi: Decidable Weighted Expressions with Presburger Combinators

    Authors: Nicolas Mazzocchi

    Abstract:

    Abstract available in PDF.

  • Guillermo Perez: Bounded-Regret Determinization of Max-Plus Automata

    Authors: Guillermo Perez

    Abstract:

    We give tight complexity bounds for the problem of determining if a given max-plus automaton is bounded-regret determinizable. This generalizes results of Aminof et al. regarding determinization of max-plus automata by pruning. More precisely, we study strategies to resolve the non-determinism of a max-plus automaton on the fly: for every word (given letter by letter) the strategy yields a run of the automaton. The regret of the strategy is then defined as the maximal difference between the value of a constructed run for a word and the value assigned to that word by the automaton. We establish that, given a max-plus automaton and a regret bound, determining if there is a strategy with regret of at most that bound, is EXP-complete. Extended Abstract.

  • Ismael Jecker: Bounded-Delay Determinization of Max-Plus Automata

    Authors: Ismael Jecker

    Abstract:

    Abstract available in PDF.

break

Branching VASS, quantitative games

  • Diego Figueira, Ranko Lazic, Jerome Leroux, Filip Mazowiecki and Gregoire Sutre: Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One

    Authors: Diego Figueira, Ranko Lazic, Jerome Leroux, Filip Mazowiecki and Gregoire Sutre

    Abstract:

    Abstract available in PDF.

  • Filip Mazowiecki: Timed pushdown automata and branching vector addition systems

    Authors: Filip Mazowiecki

    Abstract:

    We prove that non-emptiness of timed register pushdown automata is decidable in doubly exponential time. This is a very expressive class of automata, whose transitions may involve state and top-of-stack clocks with unbounded differences. It strictly subsumes pushdown timed automata of Bouajjani et al., dense-timed pushdown automata of Abdulla et al., and orbit-finite timed register pushdown automata of Clemente and Lasota. Along the way, we prove two further decidability results of independent interest: for non-emptiness of least solutions to systems of equations over sets of integers with addition, union and intersections with natural numbers and their complement; and for reachability in one-dimensional branching vector addition systems with states and subtraction. Both are in exponential time.

  • Conrad Cotton-Barratt, Andrzej Murawski and Luke Ong: ML and Extended Branching VASS

    Authors: Conrad Cotton-Barratt, Andrzej Murawski and Luke Ong

    Abstract:

    Abstract available in PDF.

  • Sylvain Schmitz: Perfect Half Space Games

    Authors: Thomas Colcombet, Marcin Jurdziński, Ranko Lazić, and Sylvain Schmitz

    Abstract:

    We introduce perfect half space games, in which the goal of Player 2 is to make the sums of encountered multi-dimensional weights diverge in a direction which is consistent with a chosen sequence of perfect half spaces (chosen dynamically by Player 2). We establish that the bounding games of Jurdziński et al. (ICALP 2015) can be reduced to perfect half space games, which in turn can be translated to the lexicographic energy games of Colcombet and Niwiński, and are positionally determined in a strong sense (Player 2 can play without knowing the current perfect half space). We finally show how perfect half space games and bounding games can be employed to solve multi- dimensional energy parity games in pseudo-polynomial time when both the numbers of energy dimensions and of priorities are fixed, regardless of whether the initial credit is given as part of the input or existentially quantified. This also yields an optimal 2-EXPTIME complexity with given initial credit, where the best known upper bound was non-elementary. Abstract available in PDF; paper presented at LICS 2017 and available from arXiv.

  • Alexander Weinert: Quantitative Reductions and Vertex-Ranked Games

    Authors: Alexander Weinert

    Abstract:

    Abstract available in PDF.

  • Martin Zimmermann: The First-order Logic of Hyperproperties

    Authors: Martin Zimmermann

    Abstract:

    Abstract available in PDF.

coffee

Invited session: Quantitative games, games with multi-objectives, non-zero sum games

  • Ocan Sankur: Admissibility in quantitative graph games

    Authors: Ocan Sankur

    Abstract:

    Admissibility has been studied for games of infinite duration with Boolean objectives. In this talk, we recall the computation of admissible strategies for these games, and explain the application for multiplayer controller synthesis. We then extend this study to games of infinite duration with quantitative objectives. We show that, under the assumption that optimal worst-case and cooperative strategies exist, admissible strategies are guaranteed to exist. Second, we give a characterization of admissible strategies using the notion of adversarial and cooperative values of a history, and we characterize the set of outcomes that are compatible with admissible strategies. Finally, we show how these characterizations can be used to design algorithms to decide relevant quantitative verification and synthesis problems.

  • Mickael Randour: Rich behavioral models: illustration on journey planning

    Authors: Mickael Randour

    Abstract:

    I will illustrate rich behavioral models in games and Markov decision processes through applications to journey planning in an uncertain environment. The shortest path problem asks to find a path of minimal length between a source vertex and a destination vertex within a weighted graph. It can be used to model minimization of travel time between two places in a town where the environment (traffic, weather, etc) is perfectly predictable. I will first discuss how it can be generalized to more realistic stochastic environments, in which case one usually wants to minimize its expected time to destination, or to maximize its chances to reach the destination within a given time. To that end, I will use (discrete) Markov decision processes. Then, I will present recent extensions allowing to reason about richer types of travel strategies (choice of route, mean of transport, etc): strategies that take into account both the length of a journey and its cost, strategies that minimize the expected travel time while providing strong guarantees on the worst-case travel time (i.e., when considering the environment as an opponent in a two-player game), and more. I will focus on the modeling power of the different models through natural application scenarios of the everyday life.

14

Thursday 14 September

Invited Talk

  • Mikolaj Bojanczyk: A Proof of Courcelle’s Conjecture on Recognisable Graph Classes

    Authors: Mikolaj Bojanczyk

    Abstract:

    Courcelle’s conjecture says that for classes of bounded treewidth, definability in MSO is the same as recognisability. More precisely, consider the following notions: (D) a class of graphs is called MSO definable if it can be defined in monadic second-order logic (with counting quantifiers). (R) a class of graphs is called recognisable if for each k there is a tree automaton which recognises width k tree decompositions of graphs satisfying the property. Many natural graph classes are easily seen to satisfy (D), e.g. graphs with Hamiltonian (or Euler) paths, or 3-colourable graphs. Courcelle’s Theorem says that (D) implies (R). Courcelle’s Conjecture says that (R) implies (D) for classes of bounded tree width. In the talk, I will discuss a proof of this conjecture. Slides https://www.mimuw.edu.pl/~bojan/slides/graph-reco/ (Joint work with Michał Pilipczuk)

    Download presentation

coffee

Stochastic games

  • Richard Mayr: On Strong Determinacy of Countable Stochastic Games

    Authors: Richard Mayr

    Abstract:

    Abstract available in PDF.

  • Sven Schewe: Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games

    Authors: Sven Schewe

    Abstract:

    2.5 player parity games combine the challenges posed by 2.5 player reachability games and the qualitative analysis of parity games. These two types of problems are best approached with different types of algorithms: strategy improvement algorithms for 2.5 player reachability games and recursive algorithms for the qualitative analysis of parity games. We present a method that—in contrast to existing techniques—tackles both aspects with the best suited approach and works exclusively on the 2.5 player game itself. The resulting technique is powerful enough to handle games with millions of states.

  • Dominik Wojtczak: Parity Objectives in Countable MDPs

    Authors: Dominik Wojtczak

    Abstract:

    We study countably infinite MDPs with parity objectives, and special cases with a bounded number of colors in the Mostowski hierarchy (including reachability, safety, Buchi and co-Buchi). In finite MDPs there always exist optimal memoryless deterministic (MD) strategies for parity objectives, but this does not generally hold for countably infinite MDPs. In particular, optimal strategies need not exist. For countable infinite MDPs, we provide a complete picture of the memory requirements of optimal (resp., ϵ-optimal) strategies for all objectives in the Mostowski hierarchy. Extended abstract available in PDF.

  • Patrick Totzke: MDPs with Energy-Parity Objectives

    Authors: Patrick Totzke

    Abstract:

    Abstract available in PDF.

  • Jan Kretinsky: Value Iteration for Mean-payoff in Markov Decision Processes

    Authors: Jan Kretinsky

    Abstract:

    Abstract available in PDF.

  • Lubos Korenciak: Mean-Payoff Optimization in Continuous-Time Markov Chains with Parametric Alarms

    Authors: Lubos Korenciak

    Abstract:

    Abstract available in PDF.

break

Higher order, abstract automata, and languages

  • Matthew Hague: Domains for Higher-Order Games

    Authors: Matthew Hague

    Abstract:

    We study two-player inclusion games played over word-generating higher-order recursion schemes. While inclusion checks are known to capture verification problems, two-player games generalise this relationship to include program synthesis. In such games, non-terminals of the grammar are controlled by opposing players. The goal of the existential player is to avoid producing a word that lies outside of a regular language of unsafe words. We contribute a new domain that provides a representation of the winning region of such games. Our domain is based on (functions over) potentially infinite Boolean formulas with words as atomic propositions. We develop an abstract interpretation framework that we instantiate to abstract this domain into a domain where the propositions are replaced by states of a finite automaton. This second domain is therefore finite and we obtain, via standard fixed point techniques, a direct algorithm for the analysis of two-player inclusion games. We show, via a second instantiation of the framework, that our finite domain can be optimised, leading to a (k+1)EXP algorithm for order-k recursion schemes. We give a matching lower bound, showing that our approach is optimal. Since our approach is based on standard Kleene iteration, existing techniques and tools for fixed point computations can be applied.

  • Paweł Parys: Recursion Schemes and the WMSO+U Logic

    Authors: Paweł Parys

    Abstract:

    We study the weak MSO logic extended by the unbounding quantifier (WMSO+U), expressing the fact that there exist arbitrarily large finite sets satisfying a given property. We prove that it is decidable whether the tree generated by a given higher-order recursion scheme satisfies a given sentence of WMSO+U. Abstract available in PDF.

  • Thomas Colcombet: Automata in Glued Vector Spaces

    Authors: Thomas Colcombet

    Abstract:

    Abstract available in PDF.

  • Daniela Petrisan: Automata as Functors

    Authors: Daniela Petrisan

    Abstract:

    Abstract available in PDF.

  • Szymon Toruńczyk: On computability and tractability for infinite sets

    Authors: Szymon Toruńczyk

    Abstract:

    Abstract available in PDF.

  • Paul Brunet: The theory of languages

    Authors: Paul Brunet

    Abstract:

    Abstract available in PDF.

lunch

Timed automata, distributed systems

  • Étienne André: Liveness in L/U Parametric Timed Automata

    Authors: Étienne André

    Abstract:

    We study timed systems in which some timing features are unknown parameters. Parametric timed automata are a classical formalism for such systems but for which most interesting problems are undecidable. Lower-bound/upper-bound parametric timed automata (L/U-PTAs) achieve decidability for reachability properties by enforcing a separation of parameters used as upper bounds in the automaton constraints, and those used as lower bounds. We further study L/U-PTAs by considering liveness related problems. We prove that: (1) the existence of at least one parameter valuation for which there exists an infinite run in the automaton is PSPACE-complete; (2) the existence of a parameter valuation such that the system has a deadlock is however undecidable; (3) the problem of the existence of a valuation for which a run remains in a given set of locations exhibits a very thin border between decidability and undecidability. Abstract also available in PDF.

  • Alessio Lomuscio: Verifying Fault-tolerance in Parameterised Multi-Agent Systems

    Authors: Alessio Lomuscio

    Abstract:

    Abstract available in PDF.

  • Francesco Belardinelli: Verification of Broadcasting Multi-Agent Systems against an Epistemic Strategy Logic

    Authors: Francesco Belardinelli

    Abstract:

    Abstract available in PDF.

  • Tomas Masopust: Universality of Partially Ordered NFAs

    Authors: Tomas Masopust

    Abstract:

    Abstract available in PDF.

break

Verification

  • Emanuele D'Osualdo: Deciding Secrecy of Security Protocols with Well Structured Transition Systems

    Authors: Emanuele D’Osualdo

    Abstract:

    Abstract available in PDF.

  • Chih-Duo Hong: Learning to prove safety over parameterised concurrent systems

    Authors: Chih-Duo Hong

    Abstract:

    Abstract available in PDF.

  • Stefan Jaax: Towards Efficient Verification of Population Protocols

    Authors: Stefan Jaax

    Abstract:

    Abstract available in PDF.

  • Nikos Tzevelekos: Higher-order linearisability

    Authors: Andrzej Murawski and Nikos Tzevelekos

    Abstract:

    Linearisability is a central notion for verifying concurrent libraries: a library is proven correct if its operational history can be rearranged into a sequential one that satisfies a given specification. Until now, linearisability has been examined for libraries in which method arguments and method results were of ground type, including libraries parameterised with such methods. In this paper we extend linearisability to the general higher-order setting: methods can be passed as arguments and returned as values. A library may also depend on abstract methods of any order. Extended abstract available in PDF.

  • Radu Grigore: Java Generics Are Turing Complete

    Authors: Radu Grigore

    Abstract:

    Abstract available in PDF.

  • Xiaowei Huang: Safety Verification of Deep Neural Networks

    Authors: Xiaowei Huang

    Abstract:

    Abstract available in PDF.

coffee

Invited session: Model learning, automata and its applications

  • Borja Balle - Title TBC: Learning Automata with Hankel Matrices

    Authors: Borja Balle

    Abstract:

    The Hankel matrix is a fundamental tool in the theory of weighted automata. In this talk we will describe a general framework for learning automata with Hankel matrices. Our framework provides a unified view of many classical and recent algorithms for learning automata under different learning paradigms, including query learning algorithms, spectral learning algorithms, and Hankel matrix completion algorithms.

  • Frits Vaandrager: Model learning

    Authors: Frits Vaandrager

    Abstract:

    Model learning, a.k.a. active automata learning, is emerging as a effective technique for obtaining state machine models of software components. In this tutorial, I will give a brief introduction to the area, highlight how model learning helped to find standard violations in implementations of the TCP, TLS and SSH protocols, and discuss recent work on the use of SMT solvers for model learning and algorithms for model learning of timed systems.

15

Friday 15 September

Invited Talk

  • Hung Ngo: Shannon-type inequalities, submodular width, and disjunctive datalog

    Authors: Hung Ngo

    Abstract:

    This talk overviews recent results on bounding the output size and on efficiently evaluating a disjunctive datalog rule, given input statistics such as relation sizes, functional dependencies, and degree bounds. These are the kind of statistics prevalent in database query evaluation, and our results apply to aggregate queries as well. The disjunctive datalog query evaluation problem is fairly general, as both conjunctive query evaluation and the basic constraint satisfaction problem are special cases. These new combinatorial and algorithmic results are built up on a fundamental connection between query evaluation and Shannon-type inequalities. It was observed in different contexts over the past 40 years that information-theoretic inequalities can be used to bound combinatorial quantities. First, one can derive (sometimes tight) output size bounds of conjunctive queries and disjunctive datalog rules using Shannon-type inequalities. This talk discusses these bounds and techniques. Second, we shall show how one can turn a proof of an information-inequality into an efficient algorithm to evaluate such queries. The algorithm’s runtime is bounded by a generalized version of the submodular width of the query (a recent notion developed by Daniel Marx), which is optimal modulo complexity-theoretic assumptions. The talk is based on joint works with Mahmoud Abo Khamis and Dan Suciu.

coffee

Databases

  • Alexandre Vigny: Constant delay enumeration for First Order queries over classes of graphs with local bounded expansion

    Authors: Alexandre Vigny

    Abstract:

    Abstract available in PDF.

  • Nils Vortmeier: An implementation of dynamic complexity

    Authors: Nils Vortmeier

    Abstract:

    Abstract available in PDF.

  • Dominik D. Freydenberger: A Logic for Document Spanners

    Authors: Dominik D. Freydenberger

    Abstract:

    Document spanners are a formal framework for information extraction that was introduced by Fagin, Kimelfeld, Reiss, and Vansummeren (PODS 2013, JACM 2015). One of the central models in this framework are core spanners, which formalize the query language AQL that is used in IBM`s SystemT. As shown by Freydenberger and Holldack (ICDT 2016, ToCS 2017), there is a connection between core spanners and ECreg, the existential theory of concatenation with regular constraints. The present paper further develops this connection by defining SpLog, a fragment of ECreg that has the same expressive power as core spanners. This equivalence extends beyond equivalence of expressive power, as we show the existence of polynomial time conversions between SpLog and core spanners. Consequences and applications include alternative way of defining relations for spanners, a pumping lemma for core spanners, and insights into the relative succinctness of various classes of spanner representations and their connection to graph querying languages.

  • Mikaël Monet: Probabilistic Graph Homomorphism: Combined Complexity

    Authors: Mikaël Monet

    Abstract:

  • Joanna Ochremiak: Proof complexity of constraint satisfaction problems

    Authors: Joanna Ochremiak

    Abstract:

    Abstract available in PDF.

  • Simone Bova and Fabio Mogavero: Herbrand Property, Finite Quasi-Herbrand Models, and a Chandra-Merlin Theorem for Quantified Conjunctive Queries

    Authors: Simone Bova and Fabio Mogavero

    Abstract:

    Abstract available in PDF.

break

Automata on infinite objects, Logics

  • Alexander Rabinovich: Determinization of Parity automata

    Authors: Alexander Rabinovich

    Abstract:

    Abstract available in PDF.

  • Salomon Sickert: From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata

    Authors: Salomon Sickert

    Abstract:

    Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL specification into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formula. In this talk a single exponential translation from limit-deterministic Büchi automata (LDBA) to DPA is sketched, and it is shown that it can be concatenated with a recent efficient translation from LTL to LDBA to yield a double exponential, “Safraless” LTL-to-DPA construction. This talk is based on work at TACAS’17 and is joint work with Javier Esparza (Technische Universität München), Jan Kretinsky (Technische Universität München), and Jean-Francois Raskin (Universite libre de Bruxelles).

  • Tobias Meggendorfer: Index appearance record for transforming Rabin automata into parity automata

    Authors: Tobias Meggendorfer

    Abstract:

    Abstract available in PDF.

  • Michaël Cadilhac: A Crevice on the Crane Beach: Finite-Degree Predicates

    Authors: Michaël Cadilhac

    Abstract:

    First-order logic (FO) over words is shown to be equiexpressive with FO equipped with a restricted set of numerical predicates, namely the order, a binary predicate MSB0, and the finite-degree predicates: FO[Arb] = FO[<, MSB0, Fin]. The Crane Beach Property (CBP), introduced more than a decade ago, is true of a logic if all the expressible languages admitting a neutral letter are regular. Although it is known that FO[Arb] does not have the CBP, it is shown here that the (strong form of the) CBP holds for both FO[<, Fin] and FO[<, MSB0]. Thus FO[<, Fin] exhibits a form of locality and the CBP, and can still express a wide variety of languages, while being one simple predicate away from the expressive power of FO[Arb]. The counting ability of FO[<, Fin] is studied as an application.

  • Jan Obdrzalek: Logical Aspects of Shrub-Depth

    Authors: Jan Obdrzalek

    Abstract:

    Abstract available in PDF.

  • Hsi-Ming Ho: MightyL: A Compositional Translation from MITL to Timed Automata

    Authors: Hsi-Ming Ho

    Abstract:

    Abstract available in PDF.

lunch

designed and delivered

superskrypt.pl