Formal Methods seminars

Their aim is to exchange ideas among group members and with other researchers, as well as to provide opportunities for postgraduates to present their work. (Up to September 2007, the seminars were joint with the Algorithms and Complexity group.)

Seminar organiser: Ranko Lazic

Summer term (19 April - 27 June 2009)

24 April 2009, 11am, CS1.01
Speaker: Jason Nurse
Title: Supporting the Comparison of Business-Level Security Requirements within Cross-Enterprise Service Development
Abstract: For businesses planning interactions online, particularly those using Web services, managing risks and accommodating each other's varying business-level security requirements is a complex but critical issue during development. Literature suggests numerous reasons that prohibit the simplistic adoption, or even comparison of requirements; examples apparent in the format used to express them, and processes employed to determine them. This paper presents the initial steps of an approach to ease this process, specially within the context of our cross-enterprise development methodology, BOF4WSS. Specifically, we focus on the design of an ontology to model key factors which influence requirement determination. This ontology will act as the basis for a future tool to state requirements and factors which influenced them, in a common, formal format, to allow for easier analysis and comparison across enterprises.
28 April 2009, 12noon, CS1.01
Speaker: John Fearnley
Title: The Complexity of Strategy Improvement For Parity Games
Abstract: This talk will give an overview of recent advances towards determining the precise complexity of strategy improvement for parity games. We will present the exponential time counter-example for the all-switches policy, which was recently discovered by Friedmann. We will discuss the implications of this counter-example with respect to the complexity of general strategy improvement for parity games. We will go on to show the techniques that we have developed for analysis of strategy improvement and we will show how Friedmann's counter-example can be adapted to provide a counter-example for a natural extension of the all-switches policy.
5 May 2009, 12noon, CS1.01
Speaker: Adrian Hudnott
Title: Efficient multiple simultaneous assignments
Abstract: In this talk I will outline an efficient method for implementing multiple simultaneous assignment in database systems. I will explain what is meant by multiple simultaneous assignment in the context of databases, why it's needed and the technical details of my proposed method and how I intend to implement it in Ingres DBMS. The proposed implementation method includes connections to research conducted across multiple areas of computer science, including query containment, multi-query optimization, minimum feedback vertex sets and multi-version concurrency control, along with many novel parts that I have developed specifically for the multiple simultaneous assignment problem.

Easter break (15 March - 18 April 2009)

24 March 2009, 12noon, CS1.01
Speaker: Stephane Demri (LSV, ENS Cachan, CNRS, INRIA Saclay)
Title: Modal Logics with Presburger constraints
Abstract: In this talk, we present an extended modal logic EML with regularity constraints and full Presburger constraints on the number of children that generalize graded modalities, also known as number restrictions in description logics. We show that the satisfiability problem for EML can be solved with polynomial space. This extends a well-known and non-trivial PSPACE upper bound for graded modal logic. Furthermore, we provide a detailed comparison with logics that contain Presburger constraints and that are dedicated to query XML documents. As an application, we provide a reduction from Sheaves logic SL into EML, which allows to improve the best known upper bound for SL satisfiability.
This is a joint work with Denis Lugiez (LIF, Marseille, France).

Spring term (4 January - 14 March 2009)

9 January 2009, 12noon, CS1.01
Speaker: Michal Rutkowski
Title: Average-Price/Reward Games on Hybrid Automata with Strong Resets
Abstract: We study price/reward games on hybrid automata with strong resets. They generalise priced games previously studied, and have applications in scheduling. We obtain decidability results by a translation to a novel class of finite graphs with price/reward information, and games assigned to edges. The cost and reward of an edge is determined by the outcome of the edge game that is assigned to it.

Summer term (20 April - 28 June 2008)

21 May 2008, 4pm, CS1.04
Speaker: Stephane Demri (LSV, ENS Cachan, CNRS, INRIA Saclay)
Title: On the almighty wand
Abstract: We investigate decidability, complexity and expressive power issues for (first-order) separation logic with one record field (herein called SEPL) and its fragments. SEPL can specify properties about the memory heap of programs with singly-linked lists. Separation logic with two record fields is known to be undecidable by reduction of finite satisfiability for classical predicate logic with one binary relation. We show that second-order logic is as expressive as SEPL and as a by-product we get undecidability of SEPL. This is refined by showing that SEPL without the separating conjunction is as expressive as SEPL, whence undecidable too. As a consequence, in SEPL the magic wand can simulate the separating conjunction. By contrast, we establish that SEPL without the magic wand is decidable with non-elementary complexity by reduction from satisfiability for the first-theory over finite words.
This is a joint work with Remi Brochenin and Etienne Lozes.

Summer break (1 July - 29 September 2007)

19 July 2007, 11am
Speaker: Carl Seger (Intel Strategic CAD Labs)
Title: Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice
Abstract: High performance floating point hardware is notoriously difficult to design correctly. In fact, until recently, the most expensive hardware bug encountered in industry, was the Intel FDIV bug in 1994 that lead to a charge of 450 million dollars against earnings. At the same time, floating point arithmetic is unique in that there is a fairly unambiguous specification, the IEEE 754 standard, which all implementations should obey. Unfortunately, bridging the gap between the mathematical specification of the standard and a low-level implementation is an extremely difficult task. At Intel we have developed an approach that combines the strengths of theorem proving with symbolic trajectory evaluation (a type of model checking), that allows us to completely verify the correctness of today's floating point units. In this talk I will discuss the evolution of this approach and discuss some of the results that have been obtained in addition to areas of future research.

Past talks

Summer term (22 April - 30 June 2007)

23 April 2007, 2pm
Speaker: Peter Krusche
Title: Efficient parallel string comparison
Abstract: The longest common subsequence (LCS) problem is a classical method of string comparison. It is well known how to solve the problem sequentally, however, in applications that require comparison of very large sequences it becomes interesting to solve this problem using parallel computers. Several coarse-grained algorithms for the LCS problem have been proposed in the past. However, none of these algorithms achieve scalable communication in the sense that the communication cost can be distributed among the processors in the parallel machine. Thus, scalable communication is advantageous particularly for low-bandwidth communication networks and parallel systems with a high number of processors. The talk will show a coarse-grained LCS algorithm with scalable communication which is work-optimal, synchronisation-efficient, and solves a more general problem of semi-local string comparison. The talk will also include a general introduction to algorithm engineering using the BSP model.
3 May 2007, 12noon
Speaker: Peter Meulemans (Arithmatica)
Title: An introduction to Arithmatica
Abstract: Arithmatica is a company of about 20 people based near Warwick, which specialises in hardware design services for multi-national semiconductor companies, with a focus on computation intensive ('datapath') designs.
We work on several levels to create optimal designs for ASIC or FGPA chips:
1) Synthesis of RTL into standard cell gate-level designs: We have our own datapath synthesis tool called CellMath Designer (CMD). CMD achieves higher clock speeds and reduced die areas and is licensed by some of the worlds largest and most advanced chip producers. The basis for our development is careful analysis of algorithms for arithmetic operators such as integer adders and multipliers as well as floating point operations. We hold several patents on implementations of these operators.
2) Efficient coding in RTL of datapath modules: We offer services to implement or optimise datapath designs. This was how Arithmatica first started in the market. Our extensive experience of efficient implementations allows us to improve on the implementations of our customers. Any knowledge gained here feeds into the CMD tool development.
3) Algorithmic level optimisation: We develop efficient solutions for particular datapath rich algorithms. We have an active R&D groups specialising in high performance DSP. Particular projects are: development of new detection and decoding algorithms for perpendicular magnetic recording; designing read channel for the new nano-scale probe storage device (as part of the European FP6 consortium involving IBM Zurich, ST Microelectronics, Plasmon, CEA LETI, the Fraunhofer Institute, the University of Aachen, the University of Twente, the University of Exeter and Arithmatica); designing coding and encryption schemes for the next generation digital archives (as part of a DTI project with the BBC, Xyratex, ITI and Ovonics).
8 May 2007, 12noon
Speaker: Ranko Lazic
Title: Algorithmic properties of logics and automata for trees with data
Abstract: I shall tell you about some nice recent work with Marcin Jurdzinski at the intersection of logic, automata and algorithms, with applications to the XPath query language for XML.
14 May 2007, 12noon
Speaker: Richard Warburton
Title: Verifying optimising compilers
Abstract: Formal verification of software has been the result of much interest from both the academic and industrial research communities over the past two decades. When verifying the actual software, rather than an algorithm, one relies on certain assumptions about the system behaviour, including that the compiler in use preserves semantics. Moreover, in optimising the program in question, modern compilers fundamentally alter the operations that the program performs and run a very real danger of introducing errors to the program in question. This motivates study into verification of the optimising phase of compilers. Since they are non-trivial applications in and of themselves, optimisers are also of interest in the context of verification. This talk presents several approaches to both completely verifying and also validating individual runs of compiler optimisations, and details some of my work in formalising a language for optimisation that has been named TRANS.
21 May 2007, 12noon
Speaker: Michal Rutkowski
Title: Hybrid games
Abstract: Hybrid systems formalise systems that combine discrete and continuous behaviour. The formalism is robust and the applications range from modelling traffic control to biological systems. This motivates a formal approach to the analysis of such systems. One of the possible techniques is solving games on hybrid systems. I will concentrate on solving minimal-cost reachability games and mean-payoff games. These games are played by two players, Min and Max whose goals are to minimise and maximise the payoff.
It is known that the reachability games on hybrid systems are in general undecidable. However, there are decidability results for certain subclasses, e.g., timed automata or o-minimal hybrid systems. We extend the study of o-minimal hybrid systems, by providing new techniques for solving optimal-cost reachability and mean-payoff games and by making the problem statement more general.
We also study the expressiveness of o-minimal hybrid systems. The technique proposed for solving the aforementioned games proves that, with respect to zero-sum games, even though equipped with sophisticated continuous dynamics, resulting in uncountable state spaces, these systems exhibit finite-state behaviour.
29 May 2007, 12noon
Speaker: Prahladh Harsha (TTI-Chicago)
Title: Short and Efficient PCPs - An overview of recent constructions
Abstract: The PCP theorem [AS, ALMSS] specifies a way of encoding any mathematical proof such that the validity of the proof can be verified probabilistically by querying the proof only at a constant number of locations. Furthermore, this encoding is complete and sound, i.e., valid proofs are always accepted while invalid proofs are accepted with probability at most 1/2. A natural question that arises in the construction of PCPs is by how much does this encoding blow up the original proof while retaining low query complexity.
The study of efficient probabilistic checkable proofs was initiated in the works of Babai et. al. [BFLS] and Feige at. al. [FGLSS] with very different motivation and emphases. The work of Babai et. al. considered the direct motivation of verifying proofs highly efficiently. In contrast, Feige et. al. established a dramatic connection between efficient probabilistically checkable proofs (PCPs) and the inapproximability of optimization problems.
In this talk, I'll review some of the recent works of Ben-Sasson et. al. [BGHSV'04, BGHSV'05], Dinur-Reingold [DR], Ben-Sasson and Sudan [BS'04] and Dinur [Din'06] that have led to the construction of PCPs that are at most a polylogarithmic factor longer than the original proof and furthermore, are checkable by a verifier running in time at most polylogarithmic in the length of the original proof.
An important ingredient in these constructions is a a new variant of PCPs called "PCPs of Proximity". These new PCPs facilitate proof composition, a crucial component in PCP construction. I'll outline how these new PCPs allow for shorter PCP constructions and efficient proof verification.
4 June 2007, 12noon
Speaker: Steve Matthews
Title: Efficiency oriented programming languages and semantics
Abstract: Following the rare example of Michel Schellekens, we consider how two familiar specialisms of theoretical computer science may find more common ground. Any given algorithm can be studied for properties such as its complexity, but, when coded up as a program, all that the typical programming language facilitates is the retention of sufficient information to enable the computer to (automatically) execute each step in the correct order. For example, how could a coding of Bubble Sort be automatically distinguished from a coding of Quick Sort to determine which program is using the algorithm having the least upper bound complexity? Such questions are undoubtedly difficult to address, and will remain so as long as thereremains an enormous gap between the complexity of algorithms and the denotational semantics of programming languages. The smaller the gap, the more we can contemplate programs continually analysing themselves at run time for their own algorithmic behaviour, and making improvements accordingly. In today's talk we will combine research from Mike Smyth on discrete spatial models, from Ulrich Hohle on many valued topology, with our own work on partial metric spaces to present an alternative approach to that of Schellekens to establishing connections between the discrete mathematics of present day algorithms research (i.e. graph theory) and the continuous mathematics traditionally used in denotational semantics (i.e. topology and domain theory).

Easter break (18 March - 21 April 2007)

2 April 2007, 10am
Speaker: Filip Murlak (Warsaw University)
Title: Topological complexity of regular tree languages
Abstract: The remarkable relations between topological and combinatorial complexity of regular languages were first observed by Klaus Wagner. In his seminal paper published in 1977 he described a hierarchy which coincided with the Wadge hierarchy restricted to regular omega-languages, and at the same time was a refinement of the Mostowski-Rabin index hierarchy. We will follow his steps and generalize these results to the case of trees.
I will present a complete description of the Wadge hierarchy of deterministically recognizable tree languages and a procedure to calculate the exact position of a given language in this hierarchy. I will also show a lower bound for the height of the Wadge hierarchy of weakly recognizable languages - a first step into the world of nondeterminism (joint work with Jacques Duparc).

Spring term (8 January - 17 March 2007)

15 January 2007, 12noon
Speaker: Thomas Brihaye (LSV, CNRS and ENS Cachan)
Title: Optimal reachability problem for weighted timed automata and games
Abstract: Weighted timed automata are natural models for embedded systems where, often, resources consumptions have to be modeled. Weighted timed automata extend classical timed automata with a cost function that maps every location and every edge to a nonnegative integer number. As a consequence, an accumulated cost can be associated to each run of a weighted timed automaton and optimization problems can be defined. The cost-optimal reachability problem asks, given a weighted timed automaton, what is the minimal accumulated cost of runs for reaching some given location? We prove that this problem is PSpace-Complete.
Weighted timed automata are models for closed systems, where every transition is controlled. If we want to distinguish between actions of a controller and actions of an environment we have to consider weighted timed games. In this context, we can ask if the controller can force the environment to update the control of the automaton in a way to reach a given location with a cost bounded by a given value. We can also ask to compute the optimal cost for that the controller can achieve. We prove that the two latter problems are undecidable.
22 January 2007, 12noon
Speaker: Arun Chakrapani Rao (Warwick Manufacturing Group)
Title: Verification projects involving Formal Methods at IARC
Abstract: In this talk, I will give an account of the experiences and learning from one of my research projects within the Premium Automotive R&D (PARD) programme. I will highlight some challenges faced, contributions made in terms of modelling and verification, and opportunities for the future. I will also briefly discuss my research within the new project called Evolutionary Validation of Complex Systems (EVoCS).
29 January 2007, 12noon
Speaker: Nikolaos Papanikolaou
Title: On Model-Checking Exogenous Quantum Logic: Complexity Aspects and Implementation
Abstract: Quantum computing and quantum information theory have attracted a lot of attention from the TCS community; this is no surprise given the massive computational power offered by the quantum computing paradigm, and the emergence of cryptographic protocols with unconditional security, to mention a couple of well-known results from the field. Moreover, the development of practical quantum cryptographic devices is now a reality. Yet quantum theory still remains a mystery to many, and the intricacies of quantum algorithms and protocols are understood but by a few practitioners. The question this talk tries to address is whether quantum protocols may be modelled and verified using a classical computer. In particular, the emphasis is put on quantum operations which may be classically simulated. A practical software tool for model-checking classically simulable protocols ("StabSim") is presented. The exogenous logic EQPL (developed at IST Lisbon), which is used in model-checking, is discussed, and a forthcoming temporal extension of the logic is briefly described.
5 February 2007, 12noon
Speaker: Alexander Tiskin
Title: Semi-local string comparison: algorithmic applications
Abstract: For two strings, the longest common subsequence (LCS) problem consists in comparing them by computing the length of their LCS. In a previous paper, we defined a more general form of string comparison, called "the all semi-local LCS problem", for which we proposed an efficient geometric output representation, and an algorithm based on fast implicit highest-score matrix multiplication. This algorithm turns out to be a useful plug-in, which allows to unify, and often to improve, various subsequence- related algorithms considered in the past. The talk will describe the main algorithm and several of its applications.
12 February 2007, 12noon
Speaker: Haris Aziz
Title: Computational issues in voting power
Abstract: Weighted voting games, in which voters are assigned varying weights are having increased significance in various political and economic organizations. They are used for structural or constitutional purposes and also used in joint stock companies where each shareholder gets votes in proportion to the ownership of a stock. The need for analysis of the voting power of the voters has led to various interesting mathematical and computational problems. These problems stem from classic formulation of Banzhaf index, Shapely-Shubik index and coalition formation.
Voting power indices of voters need to be calculated for huge voting games which is sometimes computationally intractable. There is need for complexity analysis, better approximation algorithms and effective heuristics in calculating voting power indices. I will try to present a survey of the computational issues in voting power (including some of my work) and outline research problems in this area.
26 February 2007, 12noon
Speaker: Timothy Davidson
Title: Modelling and Verification of the SECOQC Key Management Protocol
Abstract: Quantum Cryptography is now in the stage where there are commercial solutions on the market and large scale networks based on Quantum Key Distribution are becoming a reality.
QKD protocols have been around since 1984 promising unconditional security against eavesdroppers. In recent years these protocols have been physically implemented and it is now possible to distribute a key over a distance of more than 100km. The current focus is on extending what can be done over a single fibre channel in order to create complete networks.
The SECOQC project is a Europe-wide collaboration aimed at developing a global network for Secure Communication based on Quantum Cryptography. Part of the project is focused on designing the devices and cryptographic protocols that will ensure the security of the keys as they travel through the network.
In this talk I will describe the proposed protocol for the SECOQC key management module and my recent efforts at modelling and verification.
5 March 2007, 12noon
Speaker: Christian Sohler (University of Paderborn)
Title: Clustering Very Large Data Sets
Abstract: In this talk we develop a simple coreset construction for k-means and k-median clustering. A coreset is a small weighted set of points that approximates an (unweighted) set of points with respect to a (clustering) problem. We will show that given an arbitrary set of n points, it is possible to construct a weighted set of O(log n) points such that for any set of k centers the cost of both sets is within a factor of (1+\epsilon), for constant \epsilon and dimension of the input space. We show how coresets can be used to obtain a small space, insertion-only data structure that maintains a (1+\epsilon) approximation of the k-means problem (the result can be generalized to dynamic data structures). Such a data structure immediately gives a data streaming approximation algorithm for the k-means clustering problem, i.e. a space-bounded algorithm that processes an arbitrary ordered sequence of input points and computes a set of k centers that approximates the optimal solution to the k-means clustering problem within a factor of (1+\epsilon). Finally, we show that coresets can also be used to obtain a very efficient k-means implementation.

Autumn term (2 October - 9 December 2006)

3 October 2006, 4pm
Speaker: Ranko Lazic
Title: Safely Freezing LTL
Abstract: We consider the safety fragment of linear temporal logic with the freeze quantifier. The freeze quantifier is used to store a value from an infinite domain in a register for later comparison with other such values.
Our main result is that, for one register, satisfiability is ExpSpace-complete. The proof of ExpSpace-membership involves a translation to a new class of faulty counter automata. We also show that refinement and model checking problems are decidable but not primitive recursive, and that dropping the safety restriction, adding past-time temporal operators, or adding one more register, each cause undecidability of all three decision problems.
10 October 2006, 4pm
Speaker: Mike Paterson
Title: On Counting Homomorphisms to Directed Acyclic Graphs
Abstract: We give a "dichotomy theorem" for the problem of counting homomorphisms to directed acyclic graphs. Let H be a fixed directed acyclic graph. The problem is, given an input directed graph G, to determine how many homomorphisms there are from G to H.
We give a graph-theoretic classification, showing that for some digraphs H the problem is in P, while for all the rest of the digraphs H the problem is #P-complete. An interesting and unusual feature of this dichotomy is the rich supply of tractable graphs H with complex structure.
This is joint work with Martin Dyer and Leslie Goldberg.
17 October 2006, 4.30pm
Strachey Lecture by Tom Henzinger at the Oxford University Computing Laboratory
18 October 2006, 4pm
Speaker: Mikolaj Bojanczyk (Warsaw University)
Title: Forest algebra
Abstract: Instead of describing a regular language by its syntactic automaton (the minimal deterministic automaton), one can consider its syntactic semigroup. In some applications, the semigroup approach is more convenient than the automaton approach. This is especially true when one considers decision problems such as: "decide if a given regular language can be defined by a star-free expression".
Forest algebra is an attempt to provide a similar framework for regular languages of unranked trees. Use of forest algebra has already led to some progress. In particular, by inspecting the syntactic forest algebra of a regular language L, we can decide if L can be defined in temporal tree logics such as EF.
The big open problem in the field is: "decide if a given regular tree language can be defined by a formula of first-order logic".
This is joint work with Igor Walukiewicz.
24 October 2006, 4pm
Speaker: Vladimir Deineko (Warwick Business School)
Title: Special structures and exponential neighborhoods for NP-hard problems
Abstract: We consider specially structured matrices which occur in polynomially solvable cases of NP-hard problems such as the traveling salesman problem (TSP), the bipartite TSP, and the quadratic assignment problem. In most of these specially structured matrices the relevant restrictions have been formulated as the so-called four-point conditions: the inequalities involving distances between four cities. In our talk we classify all possible (symmetric) four-point conditions for the TSP and answer the question whether the TSP with the corresponding distance matrix can be solved in polynomial time or remains NP-hard. As a by-product of our classification we obtain new families of exponential neighborhoods for the TSP which can be searched in polynomial time and for which conditions on the distance matrix can be formulated so that the search for an optimal TSP solution can be restricted to these exponential neighborhoods. We discuss also the problem of recognizing special structures in permuted matrices.
31 October 2006, 4pm
Speaker: Michal Rutkowski
Title: The analysis of stationary states of gene regulatory networks using Petri nets
Abstract: I will introduce and formally define the notion of a stationary state for Petri nets. I will also propose a fully automatic method for finding such states. The proposed procedure makes use of the Presburger arithmetic to describe all possible stationary states. Finally we apply this novel approach to find stationary states of a gene regulatory network describing the flower morphogenesis of A. thaliana. This shows that the proposed method can be successfully applied in the study of biological systems.
7 November 2006, 4pm
Speaker: Marcin Jurdzinski
Title: Subexponential algorithms for solving parity games
Abstract: Solving parity games is polynomial time equivalent to the modal mu-calculus model checking problem and its exact computational complexity is an intriguing open problem: it is known to be in UP (unambiguous NP) and co-UP, but no polynomial time algorithm is known. This talk surveys a few recent algorithmic ideas which yield improved running time bounds for the problem. One is obtained by a reduction of parity games to the problem of finding the unique sink in a "unique sink orientation" of a hypercube and it yields a subexponential randomized algorithm. The other is a modification of a classical recursive algorithm for solving parity game that originates from the work of McNaughton and Zielonka and it yields a subexponential deterministic algorithm.
14 November 2006, 4pm
Speaker: Ashutosh Trivedi
Title: A strategy improvement algorithm for optimal time reachability games
Abstract: In an optimal time reachability game player Min (resp. Max) choses her moves so that the time to reach a given target configuration in a timed automaton is minimised (maximised). A value iteration based algorithm was proposed by Asarin and Maler in 1999 to compute epsilon-optimal strategies for both players. This talk complements their work by providing a strategy improvement algorithm for these games.
In this talk we introduce optimality equations, whose solutions give epsilon-optimal strategies for both players in an optimal time reachability game. In order to solve these equations effectively, we introduce the thin region abstraction which for every configuration has a finite number of symbolic timed moves. Then we present a strategy improvement algorithm which solves optimality equations for the thin optimal time reachability game.
21 November 2006, 1pm
Speaker: Arshad Jhumka
Title: Predicate detection in fault-prone systems
Abstract: Testing and monitoring distributed programs running on a distributed system involve the basic task of detecting whether a given predicate holds during the execution. Because of the uncertainties linked with distributed systems such as delays, detecting such a predicate is a non-trivial problem. This talk will first provide an overview of research in the area of global predicate detection in crash-affected distributed systems, and will also address the problem of detecting a global predicate in distributed systems that are affected by transient faults.
28 November 2006, 4pm
Speaker: Hugo Gimbert (LIX, Ecole Polytechnique)
Title: Stochastic Games with pure stationary optimal strategies
Abstract: We study zero-sum perfect information stochastic payoff games with finitely many states. Those games are natural model for controllable systems with stochastic behaviours. Solving controller synthesis problems is easy if one knows that the corresponding game admits optimal strategies that are pure and stationary. This problem has received a lot of attention in the simpler case of non-stochastic games.
We define the class of sub-mixing games and prove that they admit pure and stationary optimal strategies. As a corollary, we obtain a unified simple proof of several classical results, and generates new examples of decidable controller synthesis problems.
Part of this work is joint work with Wieslaw Zielonka.
30 November 2006, 4pm
Speaker: Hynek Mlnarik, Masaryk University, Brno
Title: Quantum Information Processing Overview
Abstract: Quantum information processing is an attractive field of computer science. Quantum phenomena were successfully used for exponential speedup of a solution of computationally hard problems like finding discrete logarithm or factorization of integers. Quantum laws can be used to teleport a quantum state over a space-like distance or establish a cryptographic key with high probability of eavesdropping detection.
In the talk we will describe basics of quantum information processing and several of its applications. We will discuss the difference to classical information processing and provide a brief overview of existing quantum programming languages and quantum process algebras.
5 December 2006, 4pm
Speaker: Rahul Savani
Title: Finding all Nash equilibria of a bimatrix game
Abstract: A bimatrix game is a basic model in non-cooperative game theory, with the most common solution concept being the Nash equilibrium. For bimatrix games, Nash equilibria are best understood geometrically. Recent results seem to make it unlikely that a polynomial-time algorithm for finding one Nash equilibrium exists. In this talk we consider the problem of finding *all* Nash equilibria of a bimatrix game. First, we will introduce the main concepts and geometric tools. Then, we will describe the state-of-the-art algorithms, which are based on linear programming and polyhedral computation, and report the results of computational experiments.
Joint work with David Avis, Gabriel Rosenberg, and Bernhard von Stengel

Summer term (19 April - 24 June 2006)

22 May 2006, 4pm, CS 1.01
Speaker: Doron Peled (Bar Ilan University)
Title: Specification and Verification using Message Sequence Charts
9 May 2006, 4pm, CS 1.04
Speaker: Ritesh Krishna
Title: Derivation of Process Algebraic Models of Biochemical Systems
24 April 2006, 11am, CS 1.04
Speaker: Alexander Tiskin
Title: Semi-local string comparison and maximum cliques in circle graphs

Easter break (12 March - 18 April 2006)

3 April 2006
Speaker: Ashutosh Trivedi
Title: Average payoff games
3 April 2006
Speaker: Nikolaos Papanikolaou
Title: A Framework for Automated Verification of Quantum Cryptographic Protocols
29 March 2006
Speaker: Pattarawit Polpinit
Title: Comparing parallel and sequential Selfish Routing in the Atomic Players setting
27 March 2006
Speaker: Markus Jalsenius
Title: Improved mixing bounds for the anti-ferromagnetic Potts model on Z2
27 March 2006
Speaker: Kasper Pedersen
Title: A scan Markov chain for sampling colourings

Spring term (4 January - 11 March 2006)

6 March 2006
Speaker: Aleksandar Dimovski
Title: A Counterexample-Guided Refinement Tool for Open Procedural Programs
27 February 2006
Speaker: Ranko Lazic
Title: LTL with the Freeze Quantifier and Register Automata

Autumn term (26 September - 3 December 2005)

22 November 2005
Speaker: Edith Elkind
Title: How hard is it to manipulate voting?
15 November 2005
Speaker: Doron Peled
Title: Efficient linear and partial order based verification of concurrent programs
1 November 2005
Speaker: David Lacey
Title: Symbolic software model checking using game semantics
11 October 2005
Speaker: Paul Goldberg
Title: The Computational Complexity of Finding a Nash Equilibrium
5 October 2005
Speaker: Nick Palmer
Title: PAC-learnability of Probabilistic DFA in terms of Variation Distance