log in

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!

Follow this registration link to register
email for inquiries: 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

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

Mikolaj Bojanczyk: 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.

Also cab sharing can be an option. Apart from the classic British black cabs (reasonable to use when 4 or 5 share the fare) there is an increasing presence of the cheaper Uber cars.

PICNIC

Location TBC. It will be in London.

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

    Authors: Damien Pous

    Abstract:

coffee

Tutorial

  • Damien Pous: 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

    Authors: Sanjay Jain

    Abstract:

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

    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

    Abstract:

    Abstract available in PDF.
  • Paul Brunet: The theory of languages

    Authors: Paul Brunet

    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:

    Abstract available in PDF.
  • Ismael Jecker: Bounded-Delay Determinization of Max-Plus Automata

    Authors: Ismael Jecker

    Abstract:

    Abstract available in PDF.

break

Branching VASS, quantitative games

  • 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.
  • 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.
  • Sylvain Schmitz: Perfect Half Space Games

    Authors: Sylvain Schmitz

    Abstract:

    Abstract available in PDF.
  • 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. (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:

    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

  • 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:

    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.
  • Murdoch Gabbay: Interleaved scope for games and automata

    Authors: Murdoch Gabbay

    Abstract:

    Abstract available in PDF.

lunch

Timed automata, distributed systems

  • Karin Quaas, Mahsa Shirmohammadi and James Worrell: Revisiting Reachability in Timed Automata

    Authors: Karin Quaas, Mahsa Shirmohammadi and James Worrell

    Abstract:

    In this talk, we revisit a fundamental result in real-time verification, namely that the binary reachability relation between configurations of a given timed automaton is definable in linear arithmetic over the integers and reals. In this paper we give a new and simpler proof of this result, building on the well-known reachability analysis of timed automata involving difference bound matrices. Using this new proof, we give an exponential-space procedure for model checking the reachability fragment of the logic parametric TCTL.
  • Étienne André: Liveness in L/U Parametric Timed Automata

    Authors: Étienne André

    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.
  • 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.
  • Andrzej Murawski and Nikos Tzevelekos: Higher-order linearisability

    Authors: Andrzej Murawski and Nikos Tzevelekos

    Abstract:

    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

    Authors: Borja Balle

    Abstract:

  • Frits Vaandrager - Title TBC: Title TBC

    Authors: Frits Vaandrager

    Abstract:

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:

    Abstract available in PDF.
  • 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:

    Abstract available in PDF.
  • 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:

    Abstract available in PDF.
  • Jan Obdrzalek: Logical Aspects of Shrub-Depth

    Authors: Jan Obdrzalek

    Abstract:

    Abstract available in PDF.

lunch

designed and delivered