ABOUT 
Computer Science Seminars and Short CoursesUseful links:
Semester 2, 2010/11Seminar programme
Seminar detailsInteger Representations: Towards Efficient Counting in the Bit Probe Model
Srinivasa Rao Satti (Seoul National University, Korea ) We
consider the problem of representing integers in close to
optimal number of bits to support increment and decrement
operations efficiently. We study the problem in the bit
probe model and analyse the number of bits read and written
to perform the operations, both in the worstcase and in the
averagecase. We propose representations with different
tradeoffs between the space used and the number of bits
probed. We also study the problem of representing integers
to support addition and subtraction operations. We propose a
representation that uses n + O(log n) bits to represent
integers in the range [0, ... ,2^n  1] which supports
addition and subtraction operations, improving the space
complexity of an earlier representation by Munro and Rahman
[Algorithmica, 2010]. We also show various tradeoffs
between the operation times and the space complexity.
This is a joint work with Gerth S. Brodal, Mark Greve and
Vineet Pandey
Coalgebraic logic for knowledge representation and reactive systems
Lutz Schröder (Bremen, Germany) Modal logic is
currently one of the most successful logical formalisms in
computer science, in particular through its role as the basis
for temporal logics on the one hand, and for description
logics on the other hand. While modal logics are standardly
equipped with a relational semantics, many modes of expression
found both in knowledge representation and in the more
detailed modelling of reactive systems, in particular where
these involve uncertainty or multiple agents, require
substantial extensions or modifications of relational
semantics. Coalgebraic logic serves as a unified semantic and
algorithmic framework for such modalities. We give an
introduction to coalgebraic logic and then present a specific
result on timedout tableaux for coalgebraic fixed point
logics (joint work with Yde Venema) in more detail.
Isomorphisms of types in the presence of higherorder references
Pierre Clairambault (Bath) We
investigate the problem of type isomorphisms in a programming
language with higherorder references. We first recall the
gametheoretic model of higherorder references by Abramsky,
Honda and McCusker. Solving an open problem by Laurent, we
show that two finitely branching arenas are isomorphic if and
only if they are geometrically the same, up to renaming of
moves (Laurent's forest isomorphism). We deduce from this an
equational theory characterising isomorphisms of types in a
finitary language L_2 with higher order references. We show
however that Laurent's conjecture does not hold on infinitely
branching arenas, yielding a nontrivial type isomorphism in
the extension of L_2 with natural numbers.
Analysis and Design of Evolutionary Algorithms
Thomas Jansen (Cork, Ireland) Evolutionary algorithms
are natureinspired general randomised search heuristics. They
are applied successfully for many different tasks, typically
when no good problemspecific algorithm is available. The
analysis of evolutionary algorithms aims at understanding the
fundamental working principles in a precise way, exhibiting
limitations, and guiding the way to improvements. We consider
as an example mutation and the influence of the mutation
probability on the optimisation time considering the class of
strictly monotone pseudoBoolean functions. These functions
are a proper superset of the class of linear pseudoBoolean
functions and a proper superset of the class of unimodal
pseudoBoolean functions. For linear functions over n bits it
is known that each mutation probability of size c/n leads to
efficient optimisation. For unimodal functions it is known
that no mutation probability can achieve that. We demonstrate
that strictly monotone functions are in between in the sense
that if c a sufficiently small constant the optimisation is
efficient but becomes very inefficient if c is a larger
constant. We discuss consequences for the choice of the
mutation probability.
The Duality of State and Observation
Prakash Panangaden (McGill, Canada) In this talk we consider the problem of
representing and reasoning about systems, especially
probabilistic systems, with hidden state. We consider
transition systems where the state is not completely visible
to an outside observer. Instead, there are observables that
partly identify the state. We show that one can interchange
the notions of state and observation and obtain what we call a
dual system. The double dual gives a minimal representation
of the behaviour of the original system. We extend this to
nondeterministic systems and to probabilistic transition
systems and finally to partially observable Markov decision
processes (POMDPs). In the case of finite automata restricted
to one observable, we obtain Brzozowski's algorithm for
minimizing finitestate language acceptors. I will explain
the coalgebraic reason why this works at the end. This
project began with joint work with colleagues from McGill
especially Doina Precup and Chris Hunt. The recent
coalgebraic understanding is joint work with Clemens Kupke
and Nick Bezhanishvili.
PAR Method and PAR Platform for Developing Reliable Software and Its New Development
Jinyun Xue (Jiangxi Normal University (JXNU), China) It is a challenging task of computer scientists
for increasing the reliability of software and efficiency of
developing software. For answering the challenge, we are
developing the PAR method and its supporting platform, called
PAR platfor, that is a longterm research project supported
by a series of research foundations of China. PAR method and
PAR platform consists of PAR programming methodology,
specification and algorithm describing language Radl, abstract
programming language Apla, a set of rules for specification
transformation and a set of automatic transformation tools of
algorithm and program. PAR provides powerful generic
structures that support convenient generic programming and the
methodology that supports formal derivation of executable
algorithmic programs from their formal specification. PAR can
be used to develop correct application program that access to
database and to develop software components with high
reliability.In this talk, I will pay main attention on
outlining the components and main functions of PAR as well as
innovative techniques in developing PAR. After that, I will
present some new research goals that is to add some new
language mechanism to Radl and Apla. The goals are the center
tasks of two research projects that were proposed by
Prof. Jose Fiadeiro and me and supported by the Chinese
Ministry of Science and technology and the NSF of China.
Conor McBride (Strathclyde) Circular programs always make my head spin, and
sometimes my computer too. Lazy evaluation allows us to trade
in data which do not yet exist, in the hope that they can be
computed just in time. If an apparently circular program does
not, in fact, have cyclic data dependencies, it will work!
However, it is only too easy to write welltyped programs
which consume data before they are produced and spiral into a
black hole. This talk presents a typed approach to circular
programming, abstractly modelling relative time, ensuring that
the present does not depend on the future. Classic perplexing
examples, such as repMin, and even the breadthfirst
treelabelling algorithm of Jones and Gibbons are explicable
in this setting, with a minimum of fuss. There is more than a
hint of a connection with modal logic, which I should like to
learn more about if time and the audience permit.
On Metaprogramming and Game Semantics
Ulrich Schöpp (Munich) In game semantics
computation is modelled by question and answer dialogues.
While dialogues are most often studied as abstract
mathematical objects, there are also examples where it is
interesting to use such dialogues for actual computation.
Ghica implements dialogues by digital circuits and is thus
able to synthesise circuits from programs in a higher
programming language. Another example where computation with
dialogues is natural can be found in the context of
programming with data that is too large to fit into memory.
In work on game semantics it is standard to abstract the
concrete details of question/answer dialogues, not least
because these details can sometimes be complicated. In this
talk I will show how the implementation of dialogues can
similarly be aided by programming language constructs for
metaprogramming. With a view to intended applications like
the ones mentioned above, the emphasis lies on
metaprogramming for weak languages. I will also consider the
implementation of dialogues in languages with computational
effects such as state or nondeterminism.
Algebraic Data Language Theory (slides)
Clemens Ley (Oxford) In algebraic language theory, certain algebraic
objects, primarily monoids, are used to analyze the structure
of string and tree languages. A fundamental result states that
a language is regular iff it is accepted by a finite
monoid. Subclasses of regular languages, such as starfree
languages correspond to natural classes of finite
monoids. Most prominently, Schützenberger, McNaughton, and
Papert showed that a regular language is first order definable
iff it is starfree iff it is accepted by an aperiodic
monoid. The study of data languages  languages over an
infinite alphabet  is motivated by applications in
verification and XML processing. In this talk I will report
about a recent extension of algebraic techniques to the study
of data languages. A class of infinite monoids, finiteorbit
data monoids, has been proposed by Bojanczyk. We present a
logic, called rigidlyguarded monadic second order logic, that
defines exactly the languages accepted by finiteorbit data
monoids. A theorem akin to Schutzenberger's Theorem also
carries over to data languages: We show that a language is
definable in rigidlyguarded first order logic iff it is
accepted by an aperiodic data monoid.
A topostheoretic approach to Stonetype dualities (paper)
Olivia Caramello (Cambridge)
Bartek Klin (Cambridge/Warsaw) First
I will show how a simple categorical understanding of
deterministic automata in the spirit of Arbib and Manes, when
instantiated in the category of nominal sets as studied by
Gabbay and Pitts, yields a useful model of finite computation
on infinite alpabets, closely related to HDautomata of
Pistore and others, and enjoying better properties then Finite
Memory Automata of Francez and Kaminski. These are then
generalized to cater for alphabets with structure (such as an
order or a graph) that can be checked upon by automata. In the
process, the theory of nominal sets needs to be generalized to
arbitrary groups of permutations rather than symmetric
groups. A particularly well behaved class of alphabets arises
from the modeltheoretic study of Fraisse limits.
Types for access capabilities in multicore systems
Alan Mycroft (Cambridge) Private local memory and
shared memory in multicore systems causes headaches:
programs have concurrency errors (races); cache effects
expose the fiction of random access memory; and private
local memory requires explicit interprocessor data
transfers. We show how an intuitive type system can enforce
data isolation between tasks. This eliminates data
races and also allows a compiler to freely allocate tasks to
processors without changing program meaning and with
increased performance predictability.
Ontologydriven Service and Software Architecture
Claus Pahl (Dublin) Ontologies have recently been used
to support software development activities. Ontologies are
rooted in description logics and consequently support
formality and rigour in development of software, but
ontologies are also conceptual modelling frameworks close to
common software modelling notations such as UML. Based on
a framework for ontologydriven software development, we
investigate the potential, but also the limitations of using
ontologies for software modelling and reasoning. We
specifically look at software architecture design and
serviceoriented architectures, focussing on architecture
patterns, service composition and behaviour modelling. At the
core of the solution are extensions and adaptions of
description logics to encompass process behaviour and
processbased patterns as abstractions.
Programming Proofs and Proving Programs
Nick Benton (Microsoft Research) Developers turn coffee into programs, whilst
mathematicians turn it into proofs. Amazingly, proofs and
programs are not just made from the same stuff, but there's
a strong sense in which they actually *are* the same
stuff. The modern understanding of proofs, programs, and the
correspondence between them, is one of the most significant
intellectual developments of the 20th century. That
understanding is now embodied in a radically new kind of
language and software tool that could revolutionize both
mathematics and software development in the 21st century.
Jim Davies (Oxford) Semester 1, 2010/11Seminar programme
Seminar detailsAutomata and logics on structures with data (slides)
Ranko Lazic (Warwick) Even without continuous
phenomena, words and trees over finite alphabets are sometimes
insufficiently detailed models. A prominent example is
processing semistructured data, which may involve attribute
values from infinite domains. With such a motivation, several
formalisms for reasoning about words and trees with infinitary
data have recently been studied, using a variety of
techniques. The emerging landscape is interesting, but careful
navigation is required for avoiding undecidability and very
high complexity.
Adventures in XML Updates (slides)
James Cheney (Edinburgh) Over the last 10 years, members of the database,
programming language and Web communities have developed a
nice, purely functional (in parts) query language for
treestructured data called XQuery, including a formal
semantics that is a (nonnormative) W3C standard. Many people
are now intent on adding imperative features so that
treestructured data can also be updated. Doing so can easily
damage the existing advantages of XQuery. I’ll present some
work on a clean, but not very expressive language called FLUX
, and contrast it with the semantics of the W3C update
proposal currently under development, focusing on the issue of
typechecking. Time permitting I will also discuss more recent
work on static analysis and optimization for the W3C language.
Model Engineering for ModelDriven Engineering
Axel van Lamsweerde (Universite catholique de Louvain, Belgium) The effectiveness of MDE
relies on our ability to build highquality models. This task
is intrinsically difficult. We need to produce sufficiently
complete, adequate, consistent, and wellstructured models
from incomplete, imprecise, and sparse material originating
from multiple, often conflicting sources. The system we need
to consider in the early stages comprises software and
environment components including people and devices.
Such models should integrate the intentional, structural,
functional, and behavioral facets of the system being
developed. Rigorous techniques are needed for model
construction, analysis, and evolution. They should support
early and incremental reasoning about partial models for a
variety of purposes, including satisfaction arguments,
property checks, animations, the evaluation of alternative
options, the analysis of risks, threats and conflicts, and
traceability management. The tension between technical
precision and practical applicability calls for a suitable mix
of heuristic, deductive, and inductive forms of reasoning on a
suitable mix of declarative and operational models. Formal
techniques should be deployed only when and where needed, and
kept hidden wherever possible. The talk will provide a
retrospective account of our research efforts and practical
experience along this route, including recent progress in
model engineering for safetycritical medical
workfows. Problemoriented abstractions, analyzable models,
and constructive techniques are pervasive concerns.
Functional Programming Gets Physical: Pushing the Boundaries of NonCausal Modelling Languages
Henrik Nilsson (Nottingham) Equational models of physical phenomena and systems
is essentially noncausal: the equations simply state the relation
among the involved entities. However, solving such equations, for
example, predicting the behaviour of a system through simulation,
has traditionally required a manual reformulation into causal
form, allowing the "known" entities to be used for computing the
"unknowns". This causal reformulation can be very cumbersome,
especially for large models. This has led to the development of
modelling and simulation languages that directly support a
noncausal formulation, obviating the need for manual
causalisation. This also turns out to give additional important
methodological and modularity benefits. However, the current
industrialstrength noncausal modelling and simulation languages
have a number of limitations, notably when it comes to describing
hybrid systems: systems that exhibit both continuoustime and
discretetime characteristics. In this talk, I'll outline a novel
approach to noncausal modelling and simulation of hybrid systems,
called Functional Hybrid Modelling (FHM), aimed at mitigating some
of these limitations. As the name suggests, it draws from
functional programming; in particular, it can be seen as a
generalisation of Functional Reactive Programming (FRP), which
allows very general hybrid systems to be described, except only
causally.
FreshRegister Automata (slides)
Nikos Tzevelekos (Oxford) What is a basic automatatheoretic model of
computation with names and freshname generation? We
introduce FreshRegister Automata (FRA), a new class of
automata which operate on an infinite alphabet of names and
use a finite number of registers to store fresh names, and
to compare incoming names with previously stored ones. These
finite machines extend Kaminski and Francez’s FiniteMemory
Automata by being able to recognise globally fresh inputs,
that is, names fresh in the whole current run. We examine
the expressivity of FRA’s both from the aspect of accepted
languages and of bisimulation equivalence. We establish
primary properties and connections between automata of this
kind, and answer key decidability questions. As a
demonstrating example, we express the theory of the
picalculus in FRA’s and characterise bisimilarity by an
appropriate, and decidable in the finitary case, notion of
bisimilarity in these automata.
From Initial Algebras to Fibred Initial Algebras
Neil Ghani (Strathclyde) We all learned about
induction for proving properties of natural numbers at
school. But what about other data types such as lists  do
they have induction principles? And what exactly are
properties and can we use induction for different notions of
properties. Finally, if we work in categories other than the
category of Sets, do we still have induction principles? In this talk I'll show that, indeed, we can have induction
principles parameterised by the category we work in , the data
type we are interested in and the notion of property under
consideration. These results arise from a very beautiful
picture of induction if one will willing to consider the topic
within a fibrational setting.
Semantics of recursive behaviour
Jiri Velebil (Prague) In this overview talk I will mention three types
of terms (finite, rational and infinite) and show how they
arise naturally when considering recursive equational
specification. Moreover, their algebraic theories all enjoy
universal properties, distinguishing them as free theories
among theories of a certain type. The results mentioned
in this talk have been obtained in cooperation with Jiri
Adamek and Stefan Milius.
The visible and the invisible: interaction design for medical devices
Ann Blandford (UCL) Widely used
interactive medical devices such as infusion pumps pose
interaction difficulties. These include difficulties in
programming, interaction and sociotechnical design, all of
which may result in untoward incidents. These difficulties
have rarely been a focus for study: they are effectively
invisible. In this talk, I will discuss what is currently
known about the design and use of interactive medical devices
and outline ways of improving the designs to better support
the needs of clinicians and patients.
Time and Abstraction in Biological Membrane Models
Reiko Heckel (Leicester) When using models to
understand observed natural, social or technical processes (as
opposed to designing them), we are interested in abstraction
as the common direction of model development. Starting from a
detailed model or observation, some of the features are
ignored in order to simplify and reduce the model, for example
with a view to improving our capacities for analysis.
In Computer Science, a variety of methods and tools have been
developed to define modelling languages and support the
transformation and analysis of models. It is the aim of this
talk to show how such methods can be applied to Biological
Membrane Models, i.e., models of hierarchical cellular systems
with local interactions and mobility. Specifically, we
will use stochastic graph transformation systems to model
membrane systems, analyse quantitative properties and develop
a method of abstraction based on "forgetting" all instances of
types we want to abstract from. This yields an abstraction
function on states which extends to rules and transformations
in the system, thus preserving the behaviour. We will
also discuss how can extend this notion of abstraction to
stochastic systems, by defining a statistical measure of
distance based on correlations between frequencies of rule
applications. Such a measure can be used to assess the quality
of an abstraction through stochastic simulation of the two
systems. We illustrate our concepts by a generic model
for infection, recovery and death of cells, using features of
membrane systems in a graph representation.
Modular Specification of Programming Languages: Advances and Challenges (slides)
Peter D Mosses (Swansea) New programming languages and domainspecific
languages (DSLs) are continually being introduced, as are
new versions of existing languages. Each language needs to
be carefully specified, to determine the syntax and
semantics of its programs  independently of any particular
implementation or machine architecture. If one has to
start from scratch, it takes a huge effort to give a precise
specification of a major new language. However, new
languages typically include a large number of constructs
from previous languages, presenting a major opportunity for
reuse of specification components. We first consider
the modular structure of language specifications, and its
consequences for reuse. Then we review various frameworks
for specifying syntax and semantics, and assess how well
they meet the challenges of language specification based on
reusable components. REFERENCES
P. D. Mosses (2004). Modular structural operational
semantics. JLAP, 6061:195228. DOI:
10.1016/j.jlap.2004.03.008 P. D. Mosses
(2008). Componentbased description of programming
languages. In Visions of Computer Science,
pp. 275286. BCS. URL:
http://www.bcs.org/server.php?show=ConWebDoc.22912
P. D. Mosses and M. J. New (2009). Implicit propagation in
structural operational semantics. In Proc. SOS 2008, ENTCS
229(4):4966. DOI: 10.1016/j.entcs.2009.07.073
A. Johnstone, P. D. Mosses, and E. Scott (2010). An agile
approach to language modelling and development. Innovations
in Systems and Software Engineering 6(12):145153. DOI:
10.1007/s1133400901116
Optimising paired and pooled kidney exchanges
David Manlove (Glasgow) Recent changes in
legislation in the UK have allowed a patient who requires a
kidney transplant, and who has a willing but incompatible
donor, to be involved in a “pairwise kidney exchange” (i.e.,
to “swap” their donor) with another patientdonor pair in a
similar position. “Pooled donations'' extend this concept to
three or more couples in a cyclic manner. NHS Blood and
Transplant (NHSBT) run the National Matching Scheme for Paired
Donation (NMSPD), which finds pairwise and 3way exchanges
(the latter being pooled exchanges involving three couples) at
regular intervals. This matching scheme is based on optimising
firstly the number of transplants, and subject to this, the
total weight of the transplants, based on a scoring system
that incorporates a number of factors including sensitivity,
HLA compatibility, age and geographic location. In this talk
we describe three computational techniques that we have used
in order to construct optimal exchanges for matching runs of
the NMSPD between July 2008 and October 2010. The first two of
these involve efficient algorithms, based on weighted matching
in graphs, to find an optimal set of exchanges and are
implemented in C++. The third technique deals with an NPhard
optimisation problem, and uses integer linear programming,
using the COIN solver . We present a summary of the results
that we obtained for the matching runs, as applied to
anonymous data supplied by NHSBT. This is joint work with
Gregg O’Malley, Péter Biró and Kirstin MacDonald.
Related links: nhs, bbc, gla Some related papers: P. Biro, D.F. Manlove and R. Rizzi. Maximum weight cycle packing in directed graphs, with application to kidney exchange programs. Discrete Mathematics, Algorithms and Applications, 1 (4) : 499517, 2009. Postprint. D.J. Abraham, A. Blum and T. Sandholm. Clearing Algorithms for BarterExchange Markets: Enabling Nationwide Kidney Exchanges. In Proceedings of ACMEC 2007: the Eighth ACM Conference on Electronic Commerce, pp. 295304, 2007. A.E. Roth, T. Sönmez and M.U. Ünver. Kidney exchange. Quarterly Journal of Economics, 119 (2) : 457488, 2004.
Silvio Ghilardi (Milan) Satisfiability Modulo
Theories (SMT) is an emerging technology in the area of formal
verification. It extends classical satsolving algorithms by
combining them with specialised decision procedures.
We show how to exploit SMT solvers in declarative formulations
of classical backward reachability algorithms. We motivate the
notion of an arraybased system and introduce some decision
problems for quantified formulae arising from infinite state
model checking applications. We also show how this framework
is implemented in the model checker MCMT (based on the SMT
solver Yices). Finally we discuss some common benchmarks in
the area of distributed algorithms and report also recent
experiments concerning timed and fault tolerant systems. We
shall discuss the efficiency of strategies for invariant
synthesis and for partially interactive verification in our
experiments.
DigitalGoods Auctions with Purchase Probability
Kazuo Iwama (Kyoto University) Bid retraction in auction
is the most significant violation of the auction
rule. However, it is impossible to completely rule out this
possibility, especially in the case of digital goods auction
where there may be millions of winners. In this paper, we
introduce a new auction model for digital goods where winners
actually pay (buy goods) with certain probabilities. Namely if
bidder $i$ bids with value $b_i$ and the auction algorithm
offers price $p_i$, she actually buys the item with
probability $f(p_i/b_i)$ for some function $f$. The underlying
auction model is a standard one for digital goods, due to
Goldberg, Hartline and Wright, for which the wellknown
Sampling Cost Share (SCS) auction has a tight competitive
ratio of 4.0. As the above $f$, consider the function such
that the purchase probability is 1 if $p_i$ is at most $b_i/2$
(the bidder would be happy), decreasing linearly and becomes 0
if $p_i$ is $3b_i/2$ (the bidder is unhappy). Then note that
the purchase probability is 1/2 when $p_i$ is equal to $b_i$,
so only one half of the bidders on average actually pay while
all of them do so for the original model. Therefore a trivial
upper bound for the competitive ratio under the above linear
purchase probability is 8.0. The main purpose of this paper is
to prove that this trivial upper bound can be improved up to
5.334. We also examine the competitive ratio for more general
purchaseprobability functions. This is a joint work with
Mingmin Xie.


Author: Alexander Kurz (kurz mcs le ac uk), T: 0116 252 5356. 