ICMS

Jul 21, 2008 - Jul 25, 2008

Appleton Tower, University of Edinburgh

Organisers

Name	Institution
Dawar, Anuj	University of Cambridge
Etessami, Kousha	University of Edinburgh
Vardi, Moshe	Rice University

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.

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.

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
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
16.40 - 17.20	Yehuda Naveh (IBM, Haifa) Advances in constraint satisfaction for stimuli generation for functional hardware verification
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
11.40 - 12.20	Andrei Krokhin (Durham University) Hard CSPs have hard gaps at location 1
12.20 - 14.00	Lunch
14.00 - 14.40	Paul Gastin (École Normale Supérieure de Cachan) Distributed timed automata with independently evolving clocks
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

Wednesday 23 July

09.00 - 10.30	Wolfgang Thomas (RWTH, Aachen) Facets of strategy synthesis in infinite games
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
11.40 - 12.20	Matthew Hague (University of Oxford) Winning regions of pushdown parity games: a saturation method
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
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
11.40 - 12.20	Philipp Weis (University of Massachusetts Amherst) Lower bounds for formula size
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
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
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
10.30 - 11.00	Coffee/Tea
11.00 - 11.40	Stephan Kreutzer (University of Oxford) Computing excluded minors
11.40 - 12.20	Achim Blumensath (Technische Universität Darmstadt) The interpretation hierarchy for guarded second-order logic
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	Stefan Kiefer (Technische Universität München) Approximative methods for monotone systems of min-max-polynomial equations
15.20 - 15.50	Coffee/Tea
15.50 - 16.30	Patrice Ossona de Mendez (CNRS, Paris) Nowhere dense structures, theory and implications
16.30 - 17.10	Jaroslav Nesetril (Charles University, Prague) Many facets of dualities (FO and CSP context)

 

Presentations:

Presentation Details
Alur, Rajeev
Marrying words and trees
View Abstract Hide Abstract
We discuss the model of nested words for representation of data with both a linear ordering and a hierarchically nested matching of items. Examples of data with such dual linear-hierarchical structure include annotated linguistic data, executions of structured programs, and HTML/XML documents. Nested words generalize both words and ordered trees, and allow both word and tree operations. We define nested word automata---finite-state acceptors for nested words, and show that the resulting class of regular languages of nested words has all the appealing theoretical properties that the classical regular word languages enjoy. The linear encodings of nested words gives the class of visibly pushdown languages of words, and this class lies between balanced languages and deterministic context-free languages. 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.
Atserias, Albert
Finite model theory for constraint satisfaction problems, and back
View Abstract Hide Abstract
This tutorial will give an overview of the so-called logical approach to constraint satisfaction problems (CSPs). Special emphasis will be put on establishing connections between the main open questions concerning the classification of tractable CSPs and purely model-theoretic questions concerning finite-variable logics on finite structures.
Blumensath, Achim
The interpretation hierarchy for guarded second-order logic
View Abstract Hide Abstract
We study guarded second-order interpretations between classes of finite structures. The main result is a complete description of the resulting hierarchy. It is linear of order type omega + 3. Each level can be characterised in terms of a suitable variant of tree-width. Canonical representatives of the various levels are: the class of (i) all trees of height n, for n < omega; (ii) all paths; (iii) all trees; and (iv) all grids.
Bojanczyk, Mikolaj
Tree languages defined by formulas with one quantifier alternation
View Abstract Hide Abstract
This talk is part of a project to find effective characterizations of logics on trees, such as first-order logic or XPath. The new results concern formulas of first-order logic that have at most one quantifier alternation.
Chen, Hubie
Quantifying Chandra-Merlin
View Abstract Hide Abstract
Chandra and Merlin proved that three fundamental problems concerning relational structures and pp-formulas--relational homomorphism, conjunctive query containment, and conjunctive query evaluation--are reformulations of the same problem. What happens if we consider these three problems, but consider quantified conjunctive formulas (pp-formulas + universal quantification) in place of pp-formulas? We get three apparently different problems; for each of these three problems, there has been recent progress on understanding their complexity/computability. (The third has been shown to be decidable, giving a new decidability result for entailment in first-order logic.) I hope to give an account of these recent developments.
Duparc, Jacques
On the non-Borel mu-calculus formulae
View Abstract Hide Abstract
We define set theoretical operations in terms of mu-formulae. In particular, we introduce an operation given by the action of mu-definable topological properties over a class of models. 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.
Gastin, Paul
Distributed timed automata with independently evolving clocks
View Abstract Hide Abstract
We propose a model of distributed timed systems where each component is a timed automaton with a set of local clocks that evolve at a rate independent of the clocks of the other components. A clock can be read by any component in the system, but it can only be reset by the automaton that it belongs to. 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.
Gelade, Wouter
XML schema languages and succinctness of regular expressions
View Abstract Hide Abstract
There exist various different XML schema languages for the specification of sets of XML documents. These languages can all be abstracted by some kind of grammar formalism using regular expressions, possibly extended with additional operators. Furthermore, translations among these schema languages essentially reduce to performing operations, such as complement or intersection, on these regular expressions or translating extended expressions into normal expressions. Therefore, we study the succinctness of regular expressions and show that in many of the latter problems double exponential size increases can not be avoided.
Göller, Stefan
ICPDL with fixed points and nominals
View Abstract Hide Abstract
We consider the logic mu-ICPDL_Nom which extends the modal mu-calculus and PDL with intersection and converse of programs (ICPDL) and allows the usage of nominals. We show that every satisfiable mu-ICPDL_Nom formula that uses at most n nominals has a countable model of tree width at most n+2. By using this result, it is shown that satisfiability in mu-ICPDL_Nom is 2EXPTIME-complete. (joint work with Markus Lohrey)
Grohe, Martin
Algorithmic and finite model theory
View Abstract Hide Abstract
Many of the early results in finite model theory were negative, stating that well known results from classical model theory do not hold when restricted to the finite. Starting in the late 1990s (after earlier pioneering work by B. Courcelle), researchers in finite model theory looked more and more at restricted classes of structures, for example trees, planar graphs, structures of bounded tree width. For such classes, many positive results were obtained, including purely model theoretic results such as preservation theorems, results in descriptive complexity theory, and algorithmic meta theorems. 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.
Hague, Matthew
Winning regions of pushdown parity games: a saturation method
View Abstract Hide Abstract
We present a new algorithm for computing the winning regions of a parity game 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.
Jurdzinski, Marcin
A simple P-matrix linear complementarity problem for discounted games
View Abstract Hide Abstract
The values of a two-player zero-sum binary discounted game are characterized by a P-matrix linear complementarity problem (LCP). Simple formulas are given to describe the data of the LCP in terms of the game graph, discount factor, and rewards. Hence it is shown that the unique sink orientation (USO) associated with this LCP coincides with the strategy valuation USO associated with the discounted game. As an application of this fact, it is shown that Murty’s least-index method for P-matrix LCPs corresponds to both known and new variants of strategy improvement algorithms for discounted games.
Kiefer, Stefan
Approximative methods for monotone systems of min-max-polynomial
View Abstract Hide Abstract
A monotone system of min-max-polynomial equations (min-max-MSPE) over the variables X_1, ..., X_n has for every i exactly one equation of the form X_i = f_i(X_1, ..., X_n) where each f_i(X_1, ..., X_n) is an expression built up from polynomials with non-negative coefficients, minimum- and maximum-operators. The question of computing least solutions of min-max-MSPEs arises naturally in the analysis of certain stochastic games. Min-max-MSPEs generalize MSPEs for which convergence speed results of Newton's method have been recently established. We present the first two methods for approximatively computing least solutions of min-max-MSPEs which converge at least linearly. Whereas the first one converges faster, a single step of the second method is cheaper. We also show how to compute epsilon-optimal strategies for the maximizer.
Kolaitis, Phokion
Foundations and applications of schema mappings
View Abstract Hide Abstract
Schema mappings are high-level specifications that describe the relationship between two database schemas. Schema mappings constitute the essential building blocks in formalizing the main data inter-operability tasks, including data exchange and data integration. The aim of this tutorial is to present an overview of recent developments in the study of schema mappings with emphasis on their uses in data exchange and on results about operators for managing schema mappings.
Kreutzer, Stephan
Computing excluded minors
View Abstract Hide Abstract
By Robertson and Seymour's graph minor theorem, every minor ideal can be characterised by a finite family of excluded minors. (A minor ideal is a class of graphs closed under taking minors.) We study algorithms for computing excluded minor characterisations of minor ideals. We propose a general method for obtaining such algorithms, which is based on definability in monadic second-order logic and the decidability of the monadic second-order theory of trees. A straightforward application of our method yields algorithms that, for a given k, compute excluded minor characterisations for the minor ideal T_k of all graphs of tree width at most k, the minor ideal B_k of all graphs of branch width at most k, and the minor ideal G_k of all graphs of genus at most k. 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.
Krokhin, Andrei
Hard CSPs have hard gaps at location 1
View Abstract Hide Abstract
The PCP theorem is known to be equivalent to the existence of a constraint language for which Max CSP (the problem of maximising the number of satisfied constraints in an instance) has a hard gap at location 1, which means that it is NP-hard to distinguish between the satisfiable instances of the corresponding problem and those where at most some constant fraction of the constraints are satisfiable. We show that, for all constraint languages, for which CSP is known to be NP-complete, the corresponding Max CSP has hard gap at location 1, even with bounded variable occurrence.
Kucera, Tony
On the satisfiability problem for probabilistic CTL
View Abstract Hide Abstract
We present some recent results about the satisfiability problem for probabilistic CTL and its fragment.
Kwiatkowska, Marta
Game-based abstraction-refinement framework for probabilistic processes
View Abstract Hide Abstract
In the field of model checking, abstraction refinement has proved to be an extremely successful methodology for combating the state-space explosion problem. However, little practical progress has been made in the setting of probabilistic verification. In this paper we present a novel abstraction-refinement framework for Markov decision processes (MDPs), which are widely used for modelling and verifying systems that exhibit both probabilistic and nondeterministic behaviour. Our framework comprises an abstraction approach based on stochastic two-player games, two refinement methods and an efficient algorithm for the abstraction-refinement loop. The key idea behind the abstraction approach is to maintain a separation between nondeterminism present in the original MDP and nondeterminism introduced during the abstraction process, each type being represented by a different player in the game. Crucially, this allows lower and upper bounds to be computed for the values of reachability properties of the MDP. These give a quantitative measure of the quality of the abstraction and form the basis of the corresponding refinement methods. We describe a prototype implementation of our framework and present experimental results demonstrating automatic generation of compact, yet precise, abstractions for a large selection of real-world case studies.
Luttenberger, Michael
Derivation tree analysis for accelerated fixed-point computation
View Abstract Hide Abstract
We show that for several classes of idempotent semirings the least fixed-point of a polynomial system of equations X = f(X) is equal to the least fixed-point of a linear system obtained by "linearizing" the polynomials of f in a certain way. Our proofs rely on derivation tree analysis, a proof principle that combines methods from algebra, calculus, and formal language theory, and was first used in a STACS'07 paper to show that Newton's method over commutative and idempotent semirings converges in a linear number of steps. 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.
Malkis, Alexander
Precise thread-modular verification
View Abstract Hide Abstract
Thread-modular verification is a promising approach for the verification of concurrent programs. Its high efficiency is achieved by abstracting the interaction between threads. The resulting polynomial complexity (in the number of threads) has its price: many interesting concurrent programs cannot be handled due to the imprecision of the abstraction. We propose a new abstraction algorithm for thread-modular verification that offers both high degree precision and polynomial complexity. Our algorithm is based on a new abstraction domain that combines Cartesian abstraction with exception sets, which allow one to handle particular thread interactions precisely. Our experimental results demonstrate the practical applicability of the algorithm.
Naveh, Yehuda
Advances in constraint satisfaction for stimuli generation for functional hardware verification
View Abstract Hide Abstract
At the previous LAA at Cambridge I reviewed the state of the art in constraint satisfaction techniques for stimuli generation for functional verification of hardware design. In the current talk I will present the advances which took place during the last two years in this very active field. In particular, many new results are driven by the enormous pressure for time-to-market and by the increasing complexity of design. Among the results I'll describe are hybrid systematic/stochastic search for processor compliance verification, highly conditional constraint satisfaction problems (CSPs) for address translation verification, and new algorithms for debugging and analyzing the solution process for complex CSPs.
Nesetril, Jaroslav
Many facets of dualities (FO and CSP context)
View Abstract Hide Abstract
To follow
Ossona de Mendez, Patrice
Nowhere dense structures, theory and implications
View Abstract Hide Abstract
To follow
Otto, Martin
Bisimulation invariance over classes of transitive frames
View Abstract Hide Abstract
Expressive completeness results are obtained for bisimulation invariant FO and MSO queries on certain classes of (finite and infinite) transitive frames. Surprisingly, a new modality is needed to capture all bisimulation invariant first-order properties over the class of all finite transitive frames, and also over the class of all transitive frames without infinite irreversible paths - in marked contrast with the situation over the class of all transitive frames. Moreover the techniques extend to the bisimulation invariant fragment of MSO, which in fact collapses to FO though not to basic modal logic. We prove ariants/generalisations of corresponding theorems about Goedel-Loeb logic by de Jongh, Sambin and Smorynski. This is joint work with Anuj Dawar.
Ouaknine, Joel
On termination of linear programs and the Skolem problem
View Abstract Hide Abstract
A central problem in software verification concerns the termination of linear programs, i.e. programs consisting of (possibly nested) WHILE loops in which the guards, conditionals, and assignments are all linear (or affine). Consider the case of simple WHILE loops without conditionals, i.e. programs of the form: WHILE (Ax > c) do {x := Bx + d} where c and d are vectors, A and B are matrices, and x is a vector of variables. A longstanding open problem is whether termination for such programs is decidable, given an initial value for x (consisting of rational numbers, say). I will discuss some progress and ongoing work on this question, as well as relationships to the Skolem and Positivity problems in number theory, and to the analysis of Markov chains. This is joint work with James Worrell and Matt Daws.
Podelski, Andreas
Constraints in verification
View Abstract Hide Abstract
We will give a survey on recent program analysis and verification methods based on constraints. Constraints here appear in essentially two forms: to state the analysis/verification problem or as data structures in algorithms solving the analysis/verification problem.
Rossman, Benjamin
The first-order variable hierarchy on finite ordered structures
View Abstract Hide Abstract
To follow
ten Cate, Balder
XPath, tree walking automata and transitive closure logic
View Abstract Hide Abstract
We consider FO(monTC), a logic whose expressive power lies in-between FO and MSO. We establish an XPath fragment that is expressively complete for FO(monTC) on trees, as well as an automata theoretic characterization in terms of nested tree walking automata. Using the latter, we show that FO(monTC) is strictly less expressive than MSO on trees, thereby resolving a question that has been open for a while. (joint work with Luc Segoufin)
Tesson, Pascal
Towards a refinement of the complexity classification of CSPs
View Abstract Hide Abstract
Research on the complexity of constraint satisfaction problems has mostly focused as classifying CSPs as either solvable in polynomial time or NP-complete. We will discuss how the universal algebra framework that has proved so potent for these investigations, can also be used to further classify tractable cases of CSP in complexity classes within P. This opens the possibility of showing that each CSP is complete for some "reasonably standard" complexity class: this is already known to hold over the two-element domain and the results presented in this talk are a first step towards a generalization to larger domains of this classification.
Thomas, Wolfgang
Facets of strategy synthesis in infinite games
View Abstract Hide Abstract
The purpose of this tutorial is twofold: In the first part we address several motivations for an algorithmic analysis of infinite games. We start from classical problems in mathematical logic (uniformization of relations, complementation problems) and then address applications in computer science (model-checking, controller synthesis). 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.
Weis, Philipp
Lower bounds for formula size
View Abstract Hide Abstract
We are interested in the succinctness of the finite-variable fragments of first-order logic, and ultimately the trade-off between formula size and number of variables. Our motivation for investigating these problems comes from both purely model-theoretic questions about succinctness, and from the close relation to the trade-off between parallel time and number of processors in computational complexity. 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.
Wilke, Thomas
Complementation, disambiguation, and determinization of Büchi automata
View Abstract Hide Abstract
To follow
Wojtczak, Dominik
Automated analysis of probabilistic recursive models
View Abstract Hide Abstract
We will survey some probabilistic infinite state models (classes of countable state Markov Chains) that arise in automated probabilistic program analysis, analysis of queueing systems and natural language processing. We will describe the relationships between them, developments in their complexity analysis as well as their game extensions. Optimized algorithms for all of these models have been implemented in PReMo -- a Probabilistic Recursive Model analyzer. We will briefly describe these algorithms as well as some interesting comparative experimental results conducted with our tool. (This is joint work with Kousha Etessami and Mihalis Yannakakis).

Participants

Name	Institution
Alur, Rajeev	University of Pennsylvania
Antonopoulos, Timos	University of Cambridge
Arenas, Marcelo	PUC, Chile
Asarin, Eugene	LIAFA, Université Paris Diderot & CNRS
Atserias, Albert	UPC, Barcelona
Barcelo, Pablo	University of Chile
Berstel, Bruno	ILOG, France
Blumensath, Achim	Technische Universität Darmstadt
Bojanczyk, Mikolaj	Warsaw University
Bradfield, Julian	University of Edinburgh
Bulatov, Andrei	Simon Fraser University
Carvalho, Catarina	Durham University
Chen, Hubie	Universitat Pompeu Fabra
Cheney, James	University of Edinburgh
Coja-Oghlan, Amin	University of Edinburgh
Dalmau, Victor	Universitat Pompeu Fabra
Dawar, Anuj	University of Cambridge
Duparc, Jacques	University of Lausanne
Egri, Laszlo	McGill University
Esparza, Javier	Technische Universität München
Etessami, Kousha	University of Edinburgh
Gastin, Paul	École Normale Supérieure de Cachan
Geerts, Floris	University of Edinburgh
Gelade, Wouter	Hasselt University
Göller, Stefan	University of Leipzig
Grohe, Martin	Humboldt University of Berlin
Gutierrez, Julian	University of Edinburgh
Haddad, Axel	École Normale Superieur de Cachan
Hague, Matthew	University of Oxford
He, Yuguo	University of Cambridge
Hella, Lauri	University of Tampere
Hernich, Andre	University of Frankfurt
Holm, Bjarki	University of Cambridge
Hunter, Paul	University of Oxford
Immerman, Neil	University of Massachussets Amherst
Jurdzinski, Marcin	University of Warwick
Kalorkoti, Kyriakos	University of Edinburgh
Kiefer, Stefan	Technische Universität München
Kolaitis, Phokion	IBM Almaden Research Centre
Kreutzer, Stephan	University of Oxford
Krokhin, Andrei	Durham University
Kucera, Tony	Masaryk University
Kwiatkowska, Marta	University of Oxford
Larose, Benoit	Concordia University
Leconte, Michel	ILOG, France
Libkin, Leonid	University of Edinburgh
Liu, Jie	Chinese Academy of Sciences
Lohrey, Markus	University of Leipzig
Luttenberger, Michael	Technical University of Munich
Malkis, Alexander	University of Freiburg
Martin, Barnaby	Durham University
Mayr, Richard	University of Edinburgh
Naveh, Yehuda	IBM, Haifa
Nesetril, Jaroslav	Charles University, Prague
Ong, Luke	University of Oxford
Ossona de Mendez, Patrice	CNRS, Paris
Otto, Martin	Technische Universität Darmstadt
Ouaknine, Joel	University of Oxford
Parys, Pawel	University of Warsaw
Piterman, Nir	Imperial College London
Podelski, Andreas	University of Freiburg
Pullum, Geoffrey	University of Edinburgh
Richerby, David	University of Leeds
Rossman, Benjamin	Massachusetts Institute of Technology (MIT)
Santhanam, Rahul	University of Edinburgh
Schweikardt, Nicole	University of Frankfurt
Schwentick, Thomas	Technische Universität Dortmund
Segoufin, Luc	INRIA, France
Sirangelo, Cristina	University of Edinburgh
Stewart, Iain	Durham University
Stirling, Colin	University of Edinburgh
Szeider, Stefan	Durham University
ten Cate, Balder	University of Amsterdam
Tesson, Pascal	University of Laval
Thomas, Wolfgang	RWTH, Aachen
Ummels, Michael	RWTH Aachen
Väänänen, Jouko	University of Amsterdam
Valeriote, Matt	McMaster University
Vardi, Moshe	Rice University
Vollmer, Heribert	Leibniz University Hannover
Weber, Volker	Technische Universität Dortmund
Weinstein, Scott	University of Pennsylvania
Weis, Philipp	University of Massachusetts Amherst
Widjaja To, Anthony	University of Edinburgh
Wilke, Thomas	Christian-Albrechts-Universität zu Kiel
Wojtczak, Dominik	University of Edinburgh
Wong, Karianto	RWTH, Aachen
Worrell, James	University of Oxford
Zivny, Stanislav	University of Oxford