# Logic and Algorithms

*21 - 25 Jul 2008*

*Appleton Tower, University of Edinburgh*

### Organiser

Name | Institution |
---|---|

Dawar, Anuj | University of Cambridge |

Etessami, Kousha | University of Edinburgh |

Vardi, Moshe | Rice University |

PDF files of some presentations are available within the Programme section of this page.

**Scientific Advisory Committee**

Andrei Bulatov (Simon Fraser University)

Javier Esparza (Technical University, Munich)

Erich Grädel (Aachen University)

Phokion Kolaitis (IBM Almaden Research Centre)

Andrei Krokhin (Durham University)

Orna Kupferman (Hebrew University)

Leonid Libkin (University of Edinburgh)

Luke Ong (University of Oxford)

The main objective of the workshop on Logic and Algorithms is to tie together a number of new strands of research that have emerged from activity at the Isaac Newton Institute and to bring the diverse communities together again to share the insights gained by recent research. The areas that will be dealt with are as follows:

- Constraint Satisfaction
- Database Theory
- Computer-Aided Verification
- Games

Many themes and techniques cut across the various areas: the aim of the proposed workshop is to survey ongoing progress in logic and algorithms, with an emphasis on cross-cutting themes and techniques, and to bring some unity and synergy to the field.

Additional support for this workshop is provided by the Isaac Newton Institute. The Laboratory for Foundations of Computer Science will contribute towards the Milner Lecture.

Participation is by invitation only: those interested in attending should contact Anuj Dawar (anuj.dawar@cl.cam.ac.uk). There will be a contribution to local costs (including accommodation and subsistence) from awards to ICMS and the Organisers. Please note that there will be NO registration fee payable by participants for this workshop.

### Arrangements

**Venue **

The Workshop will be held in Lecture Theatre 1 of the Appleton Tower, University of Edinburgh. To view the Theatre and a list of the visual equipment available click here. Follow this link for a map showing the location of Appleton Tower.

**Travel**

Information about travel to the UK and Edinburgh is available here.

If you have requested accommodation (see below), travel information and directions to Pollock Halls can be found on the website for Edinburgh First, co-ordinators of the accommodation bookings, http://www.edinburghfirst.com/edinburghfirst/travel.asp . We recommend that you take a taxi to the Halls. It should cost around 6.00 GBP from the main railway station (Waverley Station) and between 16.00 and 21.00 GBP from Edinburgh airport. Alternatively there are frequent buses from the airport to Waverley Station, from where you can get a taxi to Pollock Halls. The second of these two maps of Pollock Halls shows the location of both Pollock Halls and Appleton Tower where the lectures will take place. It is approximately a 15 minute walk between the two sites.

Lothian buses charge £1.10 for a single, £2.50 for a day ticket. Please note that the exact fare is required and no change is given. There are several Lothian Buses from the centre of town to Pollock Halls: Service No. 30, 14, 33 or the X48 Park and Ride Bus. If you enter the Service No on the Lothian Buses webpage, you will be able to view the timetable for each service bus. Leave the bus at The Commonwealth Pool on Dalkeith Road. Pollock Halls is situated just behind The Commonwealth Pool.

**Accommodation**

ICMS has arranged en-suite rooms in university accommodation in Pollock Halls for participants who requested this.

**Pollock Halls of Residence**

18 Holyrood Park Road

Edinburgh, EH16 5AY**Reception Contact Numbers**

+44 (0)131 667 1971 (Tel)

+44 (0)131 668 3217 (Fax)

On arrival at Pollock Halls, ** please go to the Reception Building on your left**, where you will pick up your key and some further information. You can access your room after 14.00. If you arrive earlier you can leave your luggage at Reception. Pollock Halls has 24 hour reception.

Alternatively, those who wished to make their own arrangements may claim back the cost, with receipts, up to a maximum of 35.00 GBP per night for bed and breakfast. A list of Edinburgh accommodation of various sorts and prices can be found on the Accommodation Page on the ICMS web site. Section 4 is particularly relevant.

**Registration**

There will be a combined Registration and Welcome Buffet from 18.30 to 20.30 on Sun 20 July, in the St Trinnean's Room, St Leonard's Hall, Pollock Halls (see map of Pollock above). Food will be available throughout that period and you may register at any time between 18.30 and 20.30.

Those who cannot register on Sun evening may do so at the workshop venue before the talks start on Mon morning.

**The 2008 Milner Lecture**

This lecture will take place in Lecture Theatre 1 in Appleton Tower at 17.15 on Wednesday 23 July. For full details click here. Following the lecture there will be a Reception in the Atrium of the Informatics Forum which is the new building directly opposite the entrance to Appleton Tower.

**Computer access**

At Registration you will be issued with a username, password and further information which will enable you to access either the wireless network or a public PC nearby. Appleton Tower is within a wireless zone as are parts of Pollock Halls.

**Meals and Refreshments**

There will be a Registration buffet in the St Trinneans Room in St Leonards Hall, Pollock Halls, on Sunday evening and a Workshop dinner on Thursday evening in the Prestonfield Room, John McIntyre Centre, Pollock Halls. A light lunch Mon-Fri and morning and afternoon refreshments will be provided in the Absorb Café area of the concourse outside Lecture Theatre 1 at Appleton Tower.

**Financial Matters**

The workshop grant will cover the cost of bed and breakfast accommodation at Pollock Halls. (Those who have made their own accommodation arrangements may claim back, with receipts, up to a maximum of 35.00 GBP per night). The buffet supper on Sun, a light lunch Mon-Fri, and the workshop dinner on Thurs evening will be provided free of charge to participants.

The majority of participants are covering their own travel. However, if we have agreed to reimburse some of your travel costs, this will be stated the 'Financial Arrangements' section of the 'Final Information' email. All reimbursement occurs after the workshop. You will be given a claim form at Registration and asked for your bank details to enable payment directly into your account. Please note that receipts are required for all expenses claimed. It would be useful if you can bring bank details to the workshop.

Please note that, in a change to earlier information published on this page, participants will no longer be required to pay the registration fee for the workshop.

### Programme

**Invited tutorial talks will be given by:**

Professor Rajeev Alur (University of Pennsylvania)

Dr Albert Atserias (UPC Barcelona)

Dr Martin Grohe (Humboldt University, Berlin)

Dr Phokion Kolaitis (IBM Almaden Research Centre)

Professor Andreas Podelski (University of Freiburg)

Professor Wolfgang Thomas (RWTH Aachen)

**Programme**

Monday 21 July

08.30 - 09.00 | Registration |

09.00 - 10.30 | Rajeev Alur (University of Pennsylvania)Marrying words and trees |

10.30 - 11.00 | Coffee/Tea |

11.00 - 11.40 | Mikolaj Bojanczyk (Warsaw University) Tree languages defined by formulas with one quantifier alternation |

11.40 - 12.20 | Balder ten Cate (University of Amsterdam)XPath, tree walking automata and transitive closure logic PDF of slides |

12.20 - 14.00 | Lunch |

14.00 - 15.30 | Andreas Podelski (University of Freiburg) Constraints in verification |

15.30 - 16.00 | Coffee/Tea |

16.00 - 16.40 | Alexander Malkis (University of Freiburg) Precise thread-modular verification PDF of slides |

16.40 - 17.20 | Achim Blumensath (Technische Universität Darmstadt) The interpretation hierarchy for guarded second-order logic |

17.20 - 18.00 | Joel Ouaknine (University of Oxford) On termination of linear programs and the Skolem problem |

Tuesday 22 July

09.00 - 10.30 | Albert Atserias (UPC, Barcelona) Finite model theory for constraint satisfaction problems, and back |

10.30 - 11.00 | Coffee/Tea |

11.00 - 11.40 | Hubie Chen (Universitat Pompeu Fabra) Quantifying Chandra-Merlin PDF of slides |

11.40 - 12.20 | Andrei Krokhin (Durham University) Hard CSPs have hard gaps at location 1 PDF of slides |

12.20 - 14.00 | Lunch |

14.00 - 14.40 | Paul Gastin (École Normale Supérieure de Cachan) Distributed timed automata with independently evolving clocks PDF of slides |

14.40 - 15.20 | Stefan Göller (University of Leipzig) ICPDL with fixed points and nominals |

15.20 - 16.00 | Michael Luttenberger (Technical University of Munich) Derivation tree analysis for accelerated fixed-point computation |

16.00 - 16.30 | Coffee/Tea |

16.30 - 17.10 | Pascal Tesson (University of Laval) Towards a refinement of the complexity classification of CSPs |

17.10 - 17.50 | Martin Otto (Technische Universität Darmstadt) Bisimulation invariance over classes of transitive frames PDF of slides |

Wednesday 23 July

09.00 - 10.30 | Wolfgang Thomas (RWTH, Aachen) Facets of strategy synthesis in infinite games PDF of slides |

10.30 - 11.00 | Coffee/Tea |

11.00 - 11.40 | Thomas Wilke (Christian-Albrechts-Universität zu Kiel) Complementation, disambiguation, and determinization of Büchi automata PDF of slides |

11.40 - 12.20 | Stefan Kiefer (Technische Universität München) Approximative methods for monotone systems of min-max-polynomial equations PDF of slides |

12.20 - 14.00 | Lunch |

Free afternoon | |

17.15 | MILNER LECTURE in Lecture Theatre 1, Appleton Tower |

**Thursday 24 July**

09.00 - 10.30 | Phokion Kolaitis (IBM Almaden Research Centre) Foundations and applications of schema mappings PDF of slides |

10.30 - 11.00 | Coffee/Tea |

11.00 - 11.40 | Benjamin Rossman (Massachusetts Institute of Technology)The first-order variable hierarchy on finite ordered structures Powerpoint slides |

11.40 - 12.20 | Philipp Weis (University of Massachusetts Amherst)Lower bounds for formula size PDF of slides |

12.20 - 14.00 | Lunch |

14.00 - 14.40 | Tony Kucera (Masaryk University) On the satisfiability problem for probabilistic CTL |

14.40 - 15.20 | Marta Kwiatkowska (University of Oxford) Game-based abstraction-refinement framework for probabilistic processes PDF of slides |

15.20 - 16.00 | Dominik Wojtczack (University of Edinburgh) Automated analysis of probabilistic recursive models |

16.00 - 16.30 | Coffee/Tea |

16.30 - 17.10 | Wouter Gelade (Hasselt University)XML schema languages and succinctness of regular expressions PDF of slides |

17.10 - 17.50 | Jacques Duparc (University of Lausanne) On the non-Borel mu-calculus formulae |

19.30 | Workshop Dinner in The Prestonfield Room, John McIntyre Centre, Pollock Halls |

Friday 25 July

09.00 - 10.30 | Martin Grohe (Humboldt University of Berlin) Algorithmic and finite model theory PDF of slides |

10.30 - 11.00 | Coffee/Tea |

11.00 - 11.40 | Stephan Kreutzer (University of Oxford) Computing excluded minors PDF of slides |

11.40 - 12.20 | Yehuda Naveh (IBM, Haifa) Advances in constraint satisfaction for stimuli generation for functional hardware verification |

12.20 - 14.00 | Lunch |

14.00 - 14.40 | Marcin Jurdzinski (University of Warwick) A simple P-matrix linear complementarity problem for discounted games |

14.40 - 15.20 | Patrice Ossona de Mendez (CNRS, Paris) Nowhere dense structures, theory and implications |

15.20 - 16.00 | Jaroslav Nesetril (Charles University, Prague) Many facets of dualities (FO and CSP context) |

16.00 | Coffee/Tea and close of workshop |

### Presentations

We argue that for algorithmic verification of structured programs, instead of viewing the program as a context-free language over words, one should view it as a regular language of nested words (or equivalently, as a visibly pushdown language), and this would allow model checking of many properties that are not expressible in existing specification logics.

We also study the relationship between ordered trees and nested words, and the corresponding automata: while the analysis complexity of nested word automata is the same as that of classical tree automata, they combine both bottom-up and top-down traversals, and enjoy expressiveness and succinctness benefits over tree automata.

There is a rapidly growing literature related to nested words, and we will briefly survey results on languages infinite nested words, nested trees, temporal logics over nested words, and new decidability results based on visibility. We will also illustrate how this research benefits from, and contributes to, extensive prior work in databases and program verification.

logics on finite structures.

When considering definability by alternation free formulae, we obtain the still conjectured mu-calculus counterpart of the Wadge hierarchy for weakly alternating tree automata. Building on it, we investigate non Borel sets definable by mu-formulae - sets for which very little is known - by introducing actions of Pi^1_1 complete sets. From these we elaborate a first conjecture on the fine topological complexity of sets of models of mu-formulae.

We investigate three natural semantics : existential, universal and reactive (game) semantics. The first one is suited in order to check that the system is safe and avoids negative specifications. The other two are useful to verify that the system satisfies positive specifications. We show that the existential and the reactive semantics are decidable whereas the universal semantics is not.

In this tutorial, I will give an introduction to the graph structure theory underlying this work, and I will explain how the structure theory can be used to obtain various results in algorithmic and finite model theory.

played over a pushdown system. This method extends the saturation techniques introduced by Bouajjani, Esparza and Maler and independently by Finkel, Willems and Wolper.

Previous solutions to this problem, due to Serre and independently to Cachat,

use an exponential reduction to a finite-state game. Our algorithm provides the

first extension of saturation techniques to parity games. We use finite word automata to represent sets of pushdown configurations, which consist of a

control state and a stack of characters from a finite alphabet. We begin with a

small automaton, and, using a fixed point characterisation of the winning

regions, expand the automaton until the algorithm is complete. Hence, in

some fortunate cases, the exponential blow-up may be avoided.

Using Hague and Ong's saturation-based algorithm for backwards reachability

analysis of higher-order pushdown systems, this technique generalises naturally

to the higher-order case.

Our main results are concerned with constructions of new minor ideals from given ones. Answering a question that goes back to Fellows and Langston, we prove that there is an algorithm that, given excluded minor characterisations of two minor ideals C and D, computes such a characterisation for the ideal Ccup D.

Furthermore, we obtain an algorithm for computing an excluded minor characterisation for the class of all apex graphs over a minor ideal C, given an excluded minor characterisation for C. (An apex graph over C is a graph G from which one vertex can be removed to obtain a graph in C.) A corollary of this result is a uniform ftp-algorithm for the ``distance k from planarity'' problem.

Our results lead to efficient generic algorithms for computing the least fixed-point. We use these algorithms to derive several consequences, including an O(N^3) algorithm for computing the throughput of a context-free grammar (obtained by speeding up the O(N^4) algorithm of Caucal et al.), and a generalization of Courcelle's result stating that the downward-closed image of a context-free language is regular.

The second part is devoted to the algorithmic solution of infinite games. We review the basic automata theoretic methodology, which combines two main techniques: the reduction of games to special cases (in particular, the "parity games"), and the solution of parity games by positional winning strategies.

In this talk we will present a game for size lower bounds, introduced by Adler and Immerman (2003), and implicitly used in the work of Grohe and Schweikardt (2004) on the succinctness of first-order logic on linear orders. We will then outline our ongoing work on using this game to attack some open questions about succinctness.

a) complementing Büchi automata,

b) turning Büchi automata into equivalent unambiguous Büchi automata, and

c) turning Büchi automata into equivalent deterministic automata.

(Joint work with Detlef Kähler)

### Participants

Name | Institution |
---|---|

Rajeev, Alur | University of Pennsylvania |

Timos, Antonopoulos | University of Cambridge |

Marcelo, Arenas | PUC, Chile |

Albert, Atserias | UPC, Barcelona |

Pablo, Barcelo | University of Chile |

Bruno, Berstel | ILOG, France |

Achim, Blumensath | Technische Universität Darmstadt |

Mikolaj, Bojanczyk | Warsaw University |

Julian, Bradfield | University of Edinburgh |

Andrei, Bulatov | Simon Fraser University |

Catarina, Carvalho | Durham University |

Hubie, Chen | Universitat Pompeu Fabra |

James, Cheney | University of Edinburgh (local participant - attending talks only) |

Amin, Coja-Oghlan | University of Edinburgh (local participant - attending talks only) |

Victor, Dalmau | Universitat Pompeu Fabra |

Anuj, Dawar | University of Cambridge |

Jacques, Duparc | University of Lausanne |

Laszlo, Egri | McGill University |

Javier, Esparza | Technische Universität München |

Kousha, Etessami | University of Edinburgh |

Paul, Gastin | École Normale Supérieure de Cachan |

Floris, Geerts | University of Edinburgh |

Wouter, Gelade | Hasselt University |

Stefan, Göller | University of Leipzig |

Martin, Grohe | Humboldt University of Berlin |

Julian, Gutierrez | University of Edinburgh (local participant - attending talks only) |

Axel, Haddad | École Normale Superieur de Cachan (attending talks only) |

Matthew, Hague | University of Oxford |

Yuguo, He | University of Cambridge |

Lauri, Hella | University of Tampere |

Andre, Hernich | University of Frankfurt |

Bjarki, Holm | University of Cambridge |

Paul, Hunter | University of Oxford |

Neil, Immerman | University of Massachussets Amherst |

Marcin, Jurdzinski | University of Warwick |

Kyriakos, Kalorkoti | University of Edinburgh (local participant - attending talks only) |

Stefan, Kiefer | Technische Universität München |

Phokion, Kolaitis | IBM Almaden Research Centre |

Stephan, Kreutzer | University of Oxford |

Andrei, Krokhin | Durham University |

Tony, Kucera | Masaryk University |

Marta, Kwiatkowska | University of Oxford |

Benoit, Larose | Concordia University |

Michel, Leconte | ILOG, France |

Michel, Leconte | ILOG, France |

Leonid, Libkin | University of Edinburgh |

Jie, Liu | Chinese Academy of Sciences (attending talks only) |

Markus, Lohrey | University of Leipzig |

Michael, Luttenberger | Technical University of Munich |

Alexander, Malkis | University of Freiburg |

Barnaby, Martin | Durham University |

Richard, Mayr | University of Edinburgh (local participant - attending talks only) |

Yehuda, Naveh | IBM, Haifa |

Jaroslav, Nesetril | Charles University, Prague |

Patrice, Ossona de Mendez | CNRS, Paris |

Martin, Otto | Technische Universität Darmstadt |

Joel, Ouaknine | University of Oxford |

Pawel, Parys | University of Warsaw |

Nir, Piterman | Imperial College London |

Andreas, Podelski | University of Freiburg |

Geoffrey, Pullum | University of Edinburgh (local participant - attending talks only) |

David, Richerby | University of Leeds |

Benjamin, Rossman | Massachusetts Institute of Technology |

Rahul, Santhanam | University of Edinburgh |

Nicole, Schweikardt | University of Frankfurt |

Thomas, Schwentick | Technische Universität Dortmund |

Luc, Segoufin | INRIA, France |

Cristina, Sirangelo | University of Edinburgh (local participant - attending talks only) |

Iain, Stewart | Durham University |

Colin, Stirling | University of Edinburgh |

Stefan, Szeider | Durham University |

Balder, ten Cate | University of Amsterdam |

Pascal, Tesson | University of Laval |

Wolfgang, Thomas | RWTH, Aachen |

Michael, Ummels | RWTH Aachen |

Jouko, Väänänen | University of Amsterdam |

Matt, Valeriote | McMaster University |

Moshe, Vardi | Rice University |

Heribert, Vollmer | Leibniz University Hannover |

Volker, Weber | Technische Universität Dortmund |

Scott, Weinstein | University of Pennsylvania |

Philipp, Weis | University of Massachusetts Amherst |

Anthony, Widjaja To | University of Edinburgh (local participant - attending talks only) |

Thomas, Wilke | Christian-Albrechts-Universität zu Kiel |

Dominik, Wojtczak | University of Edinburgh |

Karianto, Wong | RWTH, Aachen |

James, Worrell | University of Oxford |

Stanislav, Zivny | University of Oxford |