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: 7 August 2017
Tutorial day: 12 September 2017
Conference: 13-15 September 2017

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: Recognisability equals MSO definability for graphs of bounded treewidth

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

Program

12

2017.09.12

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: Verification of security protocols

    Authors: Veronique Cortier

    Abstract:

coffee

Tutorial

  • Veronique Cortier - Verification of security protocols: Verification of security protocols

    Authors: Veronique Cortier

    Abstract:

13

2017.09.13

Invited Talk

  • Sanjay Jain - Quasi Polynomial and FPT algorithms for parity games: 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: Succinct progress measures for solving parity games

    Authors: Marcin Jurdzinski and Ranko Lazic

    Abstract:

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

    Authors: John Fearnley

    Abstract:

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

    Authors: Quentin Hautem

    Abstract:

  • Nathanaël Fijalkow - Boundedness Games: Boundedness Games

    Authors: Nathanaël Fijalkow

    Abstract:

  • Dmitry Chistikov - On the complexity of quantified integer programming: On the complexity of quantified integer programming

    Authors: Dmitry Chistikov

    Abstract:

  • Paul Brunet - The theory of languages: The theory of languages

    Authors: Paul Brunet

    Abstract:

break

Transducers

  • Luc Dartois - On Reversible Transducers: On Reversible Transducers

    Authors: Luc Dartois

    Abstract:

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

    Authors: Gabriele Puppis

    Abstract:

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

    Authors: Bruno Guillon

    Abstract:

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

    Authors: Johanna Björklund

    Abstract:

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

    Authors: Henrik Björklund

    Abstract:

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

    Authors: Nathan Lhote

    Abstract:

lunch

Separability, max-plus automata

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

    Authors: Sławomir Lasota

    Abstract:

  • Lorenzo Clemente - Regular Separability of Parikh Automata: Regular Separability of Parikh Automata

    Authors: Lorenzo Clemente

    Abstract:

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

    Authors: Wojciech Czerwiński

    Abstract:

  • Nicolas Mazzocchi - Decidable Weighted Expressions with Presburger Combinators: Decidable Weighted Expressions with Presburger Combinators

    Authors: Nicolas Mazzocchi

    Abstract:

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

    Authors: Guillermo Perez

    Abstract:

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

    Authors: Ismael Jecker

    Abstract:

break

Branching VASS, quantitative games

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

    Authors: Filip Mazowiecki

    Abstract:

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

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

    Abstract:

  • Diego Figueira, Ranko Lazic, Jerome Leroux, Filip Mazowiecki and Gregoire Sutre - Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One: 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:

  • Sylvain Schmitz - Perfect Half Space Games: Perfect Half Space Games

    Authors: Sylvain Schmitz

    Abstract:

  • Alexander Weinert - Quantitative Reductions and Vertex-Ranked Games: Quantitative Reductions and Vertex-Ranked Games

    Authors: Alexander Weinert

    Abstract:

  • Martin Zimmermann - The First-order Logic of Hyperproperties: The First-order Logic of Hyperproperties

    Authors: Martin Zimmermann

    Abstract:

coffee

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

  • Ocan Sankur - Title TBC: Title TBC

    Authors: Ocan Sankur

    Abstract:

  • Mickael Randour - Title TBC: Title TBC

    Authors: Mickael Randour

    Abstract:

14

2017.09.14

Invited Talk

  • Mikolaj Bojanczyk - Recognisability equals MSO definability for graphs of bounded treewidth: Recognisability equals MSO definability for graphs of bounded treewidth

    Authors: Mikolaj Bojanczyk

    Abstract:

coffee

Stochastic games

  • Richard Mayr - On Strong Determinacy of Countable Stochastic Games: On Strong Determinacy of Countable Stochastic Games

    Authors: Richard Mayr

    Abstract:

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

    Authors: Sven Schewe

    Abstract:

  • Dominik Wojtczak - Parity Objectives in Countable MDPs: Parity Objectives in Countable MDPs

    Authors: Dominik Wojtczak

    Abstract:

  • Patrick Totzke - MDPs with Energy-Parity Objectives: MDPs with Energy-Parity Objectives

    Authors: Patrick Totzke

    Abstract:

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

    Authors: Jan Kretinsky

    Abstract:

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

    Authors: Lubos Korenciak

    Abstract:

break

Higher order, abstract automata

  • Matthew Hague - Domains for Higher-Order Games: Domains for Higher-Order Games

    Authors: Matthew Hague

    Abstract:

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

    Authors: Paweł Parys

    Abstract:

  • Thomas Colcombet - Automata in Glued Vector Spaces: Automata in Glued Vector Spaces

    Authors: Thomas Colcombet

    Abstract:

  • Daniela Petrisan - Automata as Functors: Automata as Functors

    Authors: Daniela Petrisan

    Abstract:

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

    Authors: Szymon Toruńczyk

    Abstract:

  • Murdoch Gabbay - Interleaved scope for games and automata: Interleaved scope for games and automata

    Authors: Murdoch Gabbay

    Abstract:

lunch

Timed automata, distributed systems

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

    Authors: Karin Quaas, Mahsa Shirmohammadi and James Worrell

    Abstract:

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

    Authors: Étienne André

    Abstract:

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

    Authors: Hsi-Ming Ho

    Abstract:

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

    Authors: Alessio Lomuscio

    Abstract:

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

    Authors: Francesco Belardinelli

    Abstract:

  • Tomas Masopust - Universality of Partially Ordered NFAs: Universality of Partially Ordered NFAs

    Authors: Tomas Masopust

    Abstract:

break

Verification

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

    Authors: Emanuele D’Osualdo

    Abstract:

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

    Authors: Chih-Duo Hong

    Abstract:

  • Stefan Jaax - Towards Efficient Verification of Population Protocols: Towards Efficient Verification of Population Protocols

    Authors: Stefan Jaax

    Abstract:

  • Andrzej Murawski and Nikos Tzevelekos - Higher-order linearisability: Higher-order linearisability

    Authors: Andrzej Murawski and Nikos Tzevelekos

    Abstract:

  • Radu Grigore - Java Generics Are Turing Complete: Java Generics Are Turing Complete

    Authors: Radu Grigore

    Abstract:

  • Xiaowei Huang - Safety Verification of Deep Neural Networks: Safety Verification of Deep Neural Networks

    Authors: Xiaowei Huang

    Abstract:

coffee

Invited session: Model learning, automata and its applications

  • Borja Balle - Title TBC: Title TBC

    Authors: Borja Balle

    Abstract:

  • Frits Vaandrager - Title TBC: Title TBC

    Authors: Frits Vaandrager

    Abstract:

15

2017.09.15

Invited Talk

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

    Authors: Hung Ngo

    Abstract:

coffee

Databases

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

    Authors: Alexandre Vigny

    Abstract:

  • Nils Vortmeier - An implementation of dynamic complexity: An implementation of dynamic complexity

    Authors: Nils Vortmeier

    Abstract:

  • Dominik D. Freydenberger - A Logic for Document Spanners: A Logic for Document Spanners

    Authors: Dominik D. Freydenberger

    Abstract:

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

    Authors: Mikaël Monet

    Abstract:

  • Joanna Ochremiak - Proof complexity of constraint satisfaction problems: Proof complexity of constraint satisfaction problems

    Authors: Joanna Ochremiak

    Abstract:

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

    Authors: Simone Bova and Fabio Mogavero

    Abstract:

break

Automata on infinite objects, Logics

  • Alexander Rabinovich - Determinization of Parity automata: Determinization of Parity automata

    Authors: Alexander Rabinovich

    Abstract:

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

    Authors: Salomon Sickert

    Abstract:

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

    Authors: Tobias Meggendorfer

    Abstract:

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

    Authors: Michaël Cadilhac

    Abstract:

  • Jan Obdrzalek: Logical Aspects of Shrub-Depth

    Authors: Jan Obdrzalek

    Abstract:

lunch

designed and delivered