 |
cms |
||
ABOUT |
Computer Science Seminars and Short CoursesSemester 2, 2007/8Seminar programme
Seminar detailsApproximation Algorithms for Geometric Clustering in Arbitrary Dimensions Sandeep Sen (Indian Institute of Technology, Delhi)
We present a general randomized algorithm that can find
(1+ε)-approximations for a class of clustering
problems satisfying certain properties
(existence of a random sampling procedure and tightness)
in O(2(k/ε)O(1) dn) time. We show that k-means,
discrete k-means and k-medians clustering problems satisfy the above
properties, resulting in linear time (1+ε)-approximation
algorithms for these problems. These are the first
algorithms for these problems linear in the size of
the input (which is O(nd) for n points in d dimensions),
independent of dimensions in the exponent, assuming k and
ε to be fixed. (Joint work with Amit Kumar and Yogish Sabharwal.)
Geometric Embeddings of Unit Disk Graphs
Sriram Pemmaraju (University of Iowa) The quality of a 2-dimensional embedding of a graph
G=(V,E) into the
Euclidean plane is the ratio of the maximum distance between a pair
of neighboring vertices to the minimum distance between a pair of
non-neighboring vertices. This talk will focus on the problem of
producing a "good" quality embedding of a given unit disk graph
(UDG). Any UDG, by definition, has an embedding with quality
less than 1. We present a polynomial time algorithm that computes an
O(log2.5 n)-quality embedding of a given UDG. A key step of
this algorithm is the construction of a "growth-restricted
approximation" of the given UDG. Our problem is a version of the
well-known localization problem in wireless sensor networks, in which
network nodes are required to compute virtual 2-dimensional Euclidean
coordinates given little or (as in our case) no geometric information.
Oracles and Advice as Measurements
Jose Felix Costa (Technical University of Lisbon and University of Swansea) In this talk we will try to understand how oracles and advice
functions, which are mathematical abstractions in the theory of
computability and complexity, can be seen as physical measurements in
Classical Physics. First, we consider how physical measurements are a
natural external source of information to an algorithmic computation.
We argue that oracles and advice functions can help us to understand
how the structure of space and time has information content that can
be processed by Turing machines (after Cooper and Odifreddi
andCopeland and Proudfoot). We show that non-uniform complexity is an
adequate framework for classifying feasible computations by Turing
machines interacting with an oracle in Nature. By classifying the
information content of such an oracle using Kolmogorov complexity, we
obtain a hierarchical structure for advice classes.
(Joint
work with Edwin BEGGS, Bruno LOFF, and John TUCKER.)
Towards verifying compliance in agent-based Web service compositions
Monika Solanki (Imperial College London) We explore the problem of specification and
verification of compliance in agent based Web service compositions. We
use the formalism of temporal-epistemic logic suitably extended to
deal with compliance/violations of contracts. We illustrate these
concepts using a motivating example where the behaviours of
participating agents are governed by contracts. The composition is
specified in OWL-S and mapped to our chosen formalism. Finally we use
an existing symbolic model checker to verify the example specification
whose state space is approximately 2^{21} and discuss experimental
results.
A Foundation for Real Recursive Function Theory
Jose Felix Costa (Technical University of Lisbon and University of Swansea) The class of recursive functions over the
reals, denoted by
REC(R), was introduced by Cristopher Moore in his seminal paper
written in 1995. Since then many subsequent investigations brought new
results: the class REC(R) was put in relation with the class of
functions generated by the General Purpose Analog Computer of Claude
Shannon; classical
digital computation was embedded in several ways into the new model of
computation; restrictions of REC(R) where seen to represent different
classes of recursive functions, e.g., recursive, primitive recursive
and elementary functions, and structures such as the Ritchie and the
Grzergorczyk hierarchies. The class of real recursive functions was
then stratified in a natural way, and REC(R) and the analytic hierarchy
were recently recognized as two faces of the same mathematical
concept.
In this new seminar, we bring a strong foundational support to the
Real Recursive Function Theory, rooted in Mathematical Analysis, in a
way that the reader can easily recognize both its intrinsic
mathematical beauty and its extreme simplicity. The new paradigm is
now robust and smooth enough to be taught. To achieve such a result
some concepts had to change and some new results were added. (Joint
work with Bruno Loff and Jerzy Mycka.)
Paper
Axiomatising Modal Logics of Elementary Classes of Kripke Frames
Ian Hodkinson (Imperial College London) The modal logics of elementary classes of Kripke frames have been of some longstanding interest in modal logic. Sahlqvist (1973) gave a syntactic form of axiom that serves to axiomatise many but not all of them. His work has been extended, and other ways to capture some of these logics are known. I will survey some of this in the talk, and then go on to discuss one way to axiomatise the modal logic of an arbitrary elementary frame class. The method is to translate the first-order definition into the 'quasipositive' fragment of hybrid logic, using results of Goldblatt on 'pseudo-equational' first-order sentences. One then computes modal 'approximants' to each hybrid formula, which can be shown to axiomatise the original modal logic. This process is analogous to standard proofs of Sahlqvist's theorem.
From Finite to Infinite Stochastic Systems
Ernst-Erich Doberkat (TU Dortmund, Germany) A Unified Approach for Aspect-Oriented Modeling
Jon Whittle (Lancaster University) In software engineering, aspects are concerns
that cut across multiple modules. They can lead to the common problems
of concern tangling and scattering: concern tangling is where software
concerns are not represented independently of each other; concern
scattering is where a software concern is represented in multiple
remote places in a software artifact. Although aspect-oriented
programming is relatively well understood, aspect-oriented modeling
(i.e., the representation of aspects during requirements engineering,
architecture, design) is still rather immature. Although a wide
variety of approaches to aspect-oriented modeling have been suggested,
there is, as yet, no common consensus on how aspect-oriented models
should be captured, manipulated and reasoned about. This talk presents
MATA (Modeling Aspects Using a Transformation Approach), which is a
unified way of handling aspects for any well-defined modeling
language. The talk will argue why MATA is necessary and highlight some
of the key features of MATA. In particular, the talk will motivate the
decision to base MATA on graph transformations and will describe a
number of key applications of MATA to date.
The Temporal Logic of Rewriting
Jose Meseguer (University of Illinois at Urbana-Champaign) This paper presents the temporal logic of
rewriting TLR*. Syntactically, TLR* is a very simple extension of
CTL* which just adds action atoms, in the form of spatial action
patterns, to CTL*. Semantically and pragmatically, however, when used
together with rewriting logic as a ``tandem'' of system specification
and property specification logics, it has substantially more
expressive power than purely state-based logics like CTL*, or purely
action-based logics like A-CTL*. Furthermore, it avoids the
system/property mismatch problem experienced in state-based or
action-based logics, which makes many useful properties inexpressible
in those frameworks without unnatural changes to a system's
specification. The advantages in expresiveness of TLR* are gained
without losing the ability to use existing tools and algorithms to
model check its properties: a faithful translation of models and
formulas is given that allows verifying TLR* properties with CTL*
model checkers.
Session Types and Multiparty Communication Protocols
Nobuko Yoshida (Imperial College London) A session takes place between two parties;
after establishing a connection, each party interleaves
local computations with communications (sending or
receiving) with the other party. Session types
characterise such behaviour in terms of the types of
values communicated and the shape of protocols. They have
been developed for the pi-calculus, Ambients,
multi-threaded functional languages, Web Description
languages, F#, CORBA interfaces and concurrent and
distributed Java.
This talk first gives an overview of the past and current
studies of session types.
Then we talk an extension of the session types to
multiparty, asynchronous interactions, which often arise
in practical communication-centred applications. The
theory introduces a new notion of types in which
interactions involving multiple peers are directly
abstracted as a global scenario. A global type plays the
role of "a shared agreement" among communication peers,
and is used as a basis of efficient type checking through
its projection onto individual peers. The fundamental
properties of the session type discipline such as
communication safety, progress and session fidelity are
established for general n-party asynchronous
interactions.
Paper
Joint Work with Kohei Honda and Marco Carbone (to appear
in POPL'08)
Leader Election in Anonymous Networks
Wan Fokkink (Vrije Universiteit Amsterdam) In an anonymous networks, in which nodes do not have unique identities, no terminating algorithm for leader election exists.
Probabilities can be
used to break the symmetry in anonymous networks. I present probabilistic
leader election algorithms for anonymous rings, based on an earlier
algorithm from Itai and Rodeh. We used the probabilistic model checker
PRISM to verify, for small ring sizes up to size four, that eventually a
unique leader is elected with probability one. I also discuss how leader
election for anonymous networks plays a role in FireWire (which is an
alternative for USB).
Related references:
Alon Itai, Michael Rodeh: Symmetry breaking in distributed networks Inf.
Comput. 88(1): 60-87 (1990)
Wan Fokkink, Jun Pang: Variations on Itai-Rodeh Leader Election for
Anonymous Rings and their Analysis in PRISM. J. UCS 12(8): 981-1006 (2006)
Marielle Stoelinga: Fun with FireWire: A Comparative Study of
Formal Verification Methods Applied to the IEEE 1394 Root Contention
Protocol. Formal Asp. Comput. 14(3): 328-337 (2003)
The Minimum Cost Flow Problem, Applications and Algorithms
Tomasz Radzik (King's College London) The minimum cost flow problem is a fundamental network flow problem which has been extensively studied since 1960's. It generalises the maximum network flow problem by requiring that the computed maximum flow should have the minimum possible cost, and provides foundations for more complex network flow problems, including the multicommodity flow problem. We discuss some applications of the minimum cost flow problem and review the basic properties of this problem. We also outline the main algorithmic approaches, including the capacity scaling and the cost scaling methods, which lead to polynomial time algorithms.
Steve Battle (HP Labs Bristol) This talk is about the art of ontology
creation, looking at a number of case-studies from HP and
the different methodologies used. These range from the
re-use of existing models, through use-case driven
approaches, to collaborative development.
Change Detection via Spectral Analysis in Dynamic Enterprise Networks
Diane Donovan (University of Queensland, Australia)
In the present global environment, enterprise communication networks
are continually expanding, both in terms of size and
complexity. Consequently, an important aspect of network management is
the development of efficient tools that ensure robust network
performance, and monitor changes in both network topology and
complexity. We are specifically interested in detecting changes which
are the result of abnormal events or trends.
By representing networks as combinatorial graphs we gain access to a
rich mathematical environment that facilitates a rigorous study the
dynamical aspects of these structures.
In this talk we will compare different distance measures which have
been developed to detect changes in network traffic. In particular, we
will define a metric based on vertex clustering through spectral
analysis of the Laplace matrix.
Damon Wischik (University College London) Internet connection speeds grow steadily
faster -- so why does the user experience not seem to
improve? Retrieving web pages becomes ever slower, as web
sites are stuffed with more and more features. Windows
Explorer can be excruciatingly slow when it is used over a
VPN. I believe that the main culprit is TCP, and the
unthinking way in which programmers use it as a messaging
protocol for distributed systems. I will argue that we
need a new transport protocol for short messages, and a
new calculus of network complexity for distributed
algorithms. As case studies I will look at http, at
hop-by-hop versus end-to-end reliable delivery, and at
leader election.
A logic for bimolecular interactions in compartmentalized systems
Radu Mardare (Microsoft Research, Centre for Computational and Systems Biology, Trento, Italy) The talk introduces the molecular calculus, a
logic for specifying biological systems with compartments,
that takes into account compartmentalization imposed by
biological membranes including movements of molecules across
membranes as well as the formation of molecules throw
complexation and de-complexation. The dynamic structure of
membranes is also considered, in the sense that new
compartments can be created and existing membranes
dissolved.
The formalism combines, in a unified framework, features
from two successful computational paradigms - membrane
systems and process algebras.
(Joint work with M.Cavaliere and G. Rozenberg)
Information and Logic: A Bitopological Perspective
Andrew Moshier (Chapman University, Orange, California, USA)
The classical duality theorems of Stone (for Boolean algebras), Priestley
(for distributive lattices) and Esakia (for Heyting algebras) relate
propositional logic to topology. In a quite different application, domain
theory from Scott onward has related information to topology. On the
domain theoretic view, information is characterized by being ordered
in such a way that information can accumulate. The topology arises
by taking the accumulation of information as a limit. As the field has
developed, many researchers have exploited techniques of Stone duality
in the service of domain theory. In particular, the frame of open sets
of a topological space is typically regarded as a logic in itself:
open sets are the extents of propositions and are closed under finite
conjunction and arbitrary disjunction. Thus in a domain, these propositions
constitute information about data. The result is that logic (finitary
combination of propositions) is conflated with information (infinitary
accumulation of data).
In this talk, we discuss a way to split the logic=information conflation
using bitopological spaces in place of topological spaces. On the algebraic
side, we develop the category of "skew frames" based on Kleene's analysis
of propositional logic in the presence of divergent behavior. We also discuss
how this proposal relates to some work in AI and logic programming using
bi-lattices, and consider some examples of classical topological concepts that
carry over neatly to the bitopological setting, and sketch a duality theorem
for Heyting algebras represented in bitopological spaces. We conclude with
a dicussion of logic and information in a more general setting.
Semester 1Seminar programme
Seminar detailsNew results in topological completeness of modal and superintuitionistic logics
Guram Bezhanishvili (Las Cruces, New Mexico, USA) We give an up-do-date overview of topological
completeness of modal and superintuitionistic logics. We
provide a modern account of the famous Tarski result that
IPC is the logic of each dense-in-itself metrizable space
and its modal analogue, due to McKinsey and Tarski. We also
discuss new topological completeness results for such
important modal systems as S4, S4.1, S4.2, S4.Grz, and
their superintuitionistic fragments.
The Java Memory Model: Operationally, Denotationally, Axiomatically
Pietro Cenciarelli (Universita degli Studi di Roma, La Sapienza) A semantics to a small fragment of Java
capturing the new memory model (JMM) described in the
Language Specification is given by combining operational,
denotational and axiomatic techniques in a novel semantic
framework. The operational steps (specified in the form of
SOS) construct denotational models (configuration
structures) and are constrained by the axioms of a
configuration theory. The semantics is proven correct with
respect to the Language Specification and shown to capture
many common examples in the JMM literature. (Joint work
with Alexander Knapp and Eleonora Sibilio)
Luca Cardelli (Microsoft Research, Cambridge) We investigate an artificial biochemistry that
operates according to the laws of well-mixed solutions,
where each molecule is represented by an interacting
automaton. We provide translations between the process
algebra or such automata and systems of chemical
reactions. We show that the translations preserve
discrete-state (stochastic/CME) and continuous-state
(concentration/ODE) semantics, and that the process
algebra representations are in general more compact by an
n-square factor. Compactness and compositionality of
representation are essential in describing the large
models that arise in Systems Biology.
Structured Communication-Centred Programming for Web Services
Marco Carbone (Queen Mary and Westfield College, London) This paper relates two different paradigms of
descriptions of communication behaviour, one focussing on
global message flows and another on end-point behaviours,
using formal calculi based on session types. The global
calculus, which originates from a web service description
language (W3C WS-CDL), describes an interaction scenario
from a vantage viewpoint; the end-point calculus, an
applied typed
pi-calculus, precisely identifies a local
behaviour of each participant. We explore a theory of
end-point projection, by which we can map a global
description to its end-point counterpart preserving types
and dynamics. Three principles of well-structured
description and the type structures play a fundamental role
in the theory.
Nondeterminism: many questions and (maybe) some answers
Paul Levy (University of Birmingham) Denotational semantics of nondeterminism is an
old subject, but many fundamental problems remain, such as
modelling bisimulation and fairness. This talk is a survey
of the state of the art in these problems.
On the one hand, we see counterexamples that pinpoint the
difficulties. On the other, I will indicate some lines of
investigation that appear promising, using recent
technology such as game semantics and operational
reasoning methods.
Ready Simulation for Concurrency: It's Logical!
Gerald Luettgen (University of York) This talk presents a concurrency-theoretic
framework that allows one to truly mix operational and logic
styles of specification. Heterogeneous methodologies
supporting multi-paradigm specifications have strong
practical motivations, and design notations such as the UML
already provide superficial support for them.
Our framework adds a conjunction operator to the standard
setting of labelled transition systems with CSP-style
parallel composition. We show that the well-known
behavioural relation of ready simulation is fully abstract
with respect to failures inclusion. Ready simulation also
satisfies standard logic properties, and thus lends itself
to studying mixed operational and logic languages.
Model checking faulty communication systems
James Worrell (University of Oxford)
In this talk we consider systems that communicate through
unbounded buffers that are subject to insertion errors. We
consider the complexity of model checking simple liveness,
safety and response properties expressed in CTL. We find
that while certain liveness properties can be model
checked in primitive-recursive time, checking safety
properties is non-primitive recursive.
Fabrice Saffre (BT)
We deal with the problem of deploying complementary
service components in a network of arbitrary initial
topology. We argue that, in the special case where all
components need to be present in the immediate
neighbourhood of every host, the problem amounts to a
restricted form of graph colouring, which we refer to as
"full graph colouring". We also show evidence that, in the
absence of central control or global information about
system state, a stable configuration satisfying the
requirements of full graph colouring can be approximated
through distributed heuristics, though careful calibration
of the parameters governing local decision is
required. Implications for the design of autonomic network
services are discussed.
Haplotype Inference with Propositional Logic
Joao Marques-Silva (University of Southampton)
Mutation in DNA is the principal cause for differences among
human beings, and Single Nucleotide Polymorphisms (SNPs) are
the most common mutations. A fundamental task in the
identification of SNPs is to complete a map of haplotypes in
the human population. Associated with this effort, a key
computational problem is the inference of haplotype data
from genotype data. This talk surveys recent work on using
Propositional Logic models for solving the problem of
haplotype inference by pure parsimony (HIPP). Besides the
application in bioinformatics, HIPP is a computationally
hard problem, being APX-hard. Our results show that
SAT-based haplotype inference approaches are most often
orders of magnitude faster than existing alternative
approaches.
Modelling Business Processes by Graph Transformation: Towards Artefact-driven Design
Reiko Heckel (University of Leicester)
Current practice in requirements engineering is based on
models favouring a control flow-oriented specification of
processes, e.g., using activity diagrams, complemented by a
static domain model, given by a class or ER diagram. This
approach suffers from several weaknesses. The lack of
formal integration of data and process models means that it
is impossible to check formally the consistency of these
views. Absence of data flow information makes it hard to
identify implicit dependencies between actions within
different processes. Arising from a scenario-based
methodology, a tendency towards linear processes leads to
inefficient design solutions. The method of
artefact-driven design addresses these problems by
focussing on the intended products of business processes,
describing their transformation in terms of preconditions
and effects, and deriving control flow by data flow
analysis, if required. This is particularly effective if
several artifacts In this presentation, we propose a
visual notation and formal interpretation for
artefact-oriented models based on graph transformation,
which allows to make precise the notions of conflict and
dependency between requirements expressed by different
stakeholders.Models can be statically analyzed, and
conflicts or dependencies detected by the analysis can be
communicated to the modeller by annotating the model. An
implementation of the static analysis within a graph
transformation tool is discussed.
Elena Gaura (Coventry University) The talk will be aimed at an audience little
versed in the area of Wireless Sensor Networks (WSN)and will
have as a starting point the state of the art in WSN from a
technology adoption perspective. System design principles
together with selected applications will be brought forward.
The research challenges remaining to be overcome if large
scale WSNs are to become a reality are described. Particular
emphasis will be set on the 4 themes/WSN design exercises
curently pursued within the Cogent Computing Applied
Research Centre at Coventry University: - designing for
information visualization; - designing for robustness and
long life; -designing for information extraction; -
designing for practical applications.
Hendrik Richter (HTWK Leipzig) The concept of fitness landscapes originates
from evolutionary biology and is an important tool in
theoretical studies in evolutionary optimization. Such a
fitness landscape assigns fitness values to the points of a
search space in which an optimal solution is to be found. A
general spatio-temporal fitness landscape may describe
changes of the fitness values continuously in both space and
time and could be modelled by a Partial Differential
Equation (PDE). The idea to employ Coupled Map Lattices
(CML) as fitness landscape comes from the intention to use a
discretization of space and time in order to facilitate
efficient computing of the fitness landscape. Hence,
CML can be interpreted as spatio-temporal fitness landscapes
which may pose a dynamic optimization problem. In this talk,
I present an analysis of such dynamic fitness landscapes in
terms of the landscape measures modality, ruggedness,
information content and epistasis. These measures account
for different aspects of problem hardness. I use an
evolutionary algorithm to solve the dynamic optimization
problem and study the relationship between performance
criteria of the algorithm and the landscape measures. In
this way problem hardness can be related to expectable
performance.
Generalized Sketches - Theoreticians vs. Practitioners
Uwe Wolter (University of Bergen, Norway)
Around 14 years ago Micheal Makkai came to the need to
generalize the notion of Ehresmann's sketches during his
work on an abstract categorical formulation of Completeness
Theorems in logic. In parallel Zinovy Diskin and colleagues
developed Generalized Sketches as a more appropriate
mathematical foundation of diagrammatic specification
techniques used in Software Engineering.
In the talk we present the original definition of
Generalized Sketches and their models including some
practical examples. These definitions, designed by
theoreticians, are based on "indexed concepts". It turns
out, however, that Software Engineers prefer "fibred
concepts". The concept of (meta) model in object-oriented
design, for example, is essentially a "fibred concept". We
will give the "fibred versions" of the corresponding
Generalized Sketch definitions and we discuss the relation
between the "indexed" and the "fibred world". We close the
talk pointing out some open questions and current research
topics related to Generalized Sketches.
Short CoursesProgramme
Details
Nicola Gambino (Barcelona)
(joint work with Hyland) Many important forms of data-types, such as
the set of natural numbers or the set of binary trees, can be
described abstractly as inital algebras for a special class of
endofunctors on the category of sets, which we shall refer to as
polynomial functors. Polynomial functors enjoy many good properties.
In particular, they support the development of a "calculus" very much
analogous to the ordinary polynomial calculus. The aim of the seminar
is to give an overview of the general theory of polynomial functors
and of their calculus.
Generalised species of structures
Nicola Gambino (Barcelona)
(joint work with Fiore, Hyland, and Winskel) Cartesian closed
categories are models for the simply-typed lambda calculus in which
the eta-rule and beta-rule are modelled as equalities. Moving from
cartesian closed categories to cartesian closed bicategories allows us
to model the eta-rule and beta-rule as isomorphisms rather than
equalities. The aim of the seminar is to describe the notion of a
cartesian closed bicategory and to explain one example thereof, based
on a generalisation of Joyal's notion of a species of structures.
2008/9, Semester 1Seminar programme
Seminar details
Alessandra Russo (Imperial College London)
Alistair McEwan (University of Leicester, Department of Engineering)
Simon Gay (University of Glasgow)
Artur Czumaj (University of Warwick) |
|
Author: Alexander Kurz (kurz mcs le ac uk), T: 0116 252 5356. |
|