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)
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
Alur, Rajeev
Marrying words and trees
View AbstractWe 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.
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 AbstractThis 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.
logics on finite structures.
Blumensath, Achim
The interpretation hierarchy for guarded second-order logic
View AbstractWe 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 AbstractThis 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 AbstractChandra 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 AbstractWe 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.
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 AbstractWe 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.
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 AbstractThere 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 AbstractWe 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 AbstractMany 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.
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 AbstractWe 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.
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 AbstractThe 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 AbstractA 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 AbstractSchema 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 AbstractBy 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.
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 AbstractThe 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 AbstractWe 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 AbstractIn 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 AbstractWe 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.
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 AbstractThread-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 AbstractAt 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 AbstractTo follow
Ossona de Mendez, Patrice
Nowhere dense structures, theory and implications
View AbstractTo follow
Otto, Martin
Bisimulation invariance over classes of transitive frames
View AbstractExpressive 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 AbstractA 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 AbstractWe 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 AbstractThe k-variable logic FO^k consists of first-order sentences in which every subformula has at most k free variables. The hierarchy of bounded variable logics FO^1, FO^2, ... is strict in terms of expressive power on finite structures (as, for example, FO^k cannot express "the universe has size >k"). I will discuss a recent result that the bounded variable >hierarchy is strict on finite *ordered* structures. (It was previously an open question whether FO^3 = FO in the presence of linear order.) The key technical result is a circuit lower bound which implies that the class of finite ordered graphs containing a k-clique is not definable in FO^(k/4).
ten Cate, Balder
XPath, tree walking automata and transitive closure logic
View AbstractWe 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 AbstractResearch 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 AbstractThe 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.
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 AbstractWe 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.
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 unified
View AbstractWe present, based on Muller and Schupp's procedure for turning alternating tree automata into non-deterministic ones, a uniform framework for:
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)
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)
Wojtczak, Dominik
Automated analysis of probabilistic recursive models
View AbstractWe 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 |
|---|---|
| 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 |