# informatics

## Computer Science Seminars and Short Courses — 2006/07

A map of the campus is here (most of us are in the Mathematics and Computer Science building). Further maps and directions are available from this page.

• The room is likely to be BEN LT5, which is in the Bennet building and quite straightforward to find; however...
• If the room is "Ken Edwards LT3" be aware that the entrance is hidden on the left hand side when you walk towards the main entrance. Don't go to the main entrance: there is no indication there of where LT3 is...
• If the room is FJ1119, follow the signs to AVS - Graphics and Photography.

### Semester 2

#### Seminar details

Model-oriented Formal Methods: experience in semantics, tools and industry application.

John Fitzgerald (Centre for Software Reliability Newcastle University)
Friday Jan 26, 14:30 in Ben LT5 (Host: Jose Fiadeiro)

The term "lightweight formal methods" gained currency just over ten years ago following the publication of several articles calling on the formal methods community to develop methods and tools that provide at least some of the benefits of formalism, without requiring the wholesale application of highly specialised technology. The community working around the Vienna Development Method (VDM) rose to this challenge. In this talk, we draw on experience in developing the semantics and tool support for VDM, and in applying VDM technology in industry, to identify achievements and challenges in providing lightweight but effective formal methods.

This talk is based on a forthcoming paper written with Peter Gorm Larsen of the Engineering College, Aarhus, Denmark.

Subject-Oriented Modeling and the Identification of Risk in Enterprise

Bernie Cohen (City University London, Boxer Research Ltd)
Friday Feb 2, 14:30 in Ben LT5 (Host: Jose Fiadeiro)

The classical engineering modeling frameworks are appropriate for the modeling of 'objects', but not for subjects who, being embodied individuals, anticipate the satisfaction of their own demands. We model the object with a view to reifying the model as a system, but the only reification of the subject's model is the subject herself.

The modeler of an object asumes that the construction of the model does not change the object, but the modeler of the subject must be aware that the act of modeling is an intervention in the subject's being.

Similarly, the classical business modeling frameworks are appropriate for the modeling of enterprises that adopt 'positional' strategies, but not for those that adopt 'relational'strategies who, as subjects, take 'power to the edge', anticipating the satisfaction both of their own demands and of their clients'.

We model the positional enterprise with a view to reifying the business model in an information system but, as systems analysts have reported for years, the act of modeling often alters the client's business model.

We model the relational enterprise with a view to identifying, and thereby mitigating, the risks to which the enterprise is exposed by the variety of demand that its clients present and by their need for 'through life capability management'.

We present PAN, a modeling framework that is appropriate for eliciting and analysing the models of subjects and of relational enterprises.

We invite interest in pursuing research into the structure of PAN's meta-models and the philosophical, psychological and mathematical issues that they raise.

Computing with real real numbers, or, what is sin(10^40)?

Achim Jung (University of Birmingham)
Friday Feb 9, 14:30 in Ben LT5 (Host: Jose Fiadeiro)

A lot of our work as computer scientists is concerned with modelling the real world inside a computer system. The more accurate such a model is the more useful and reliable will the program be, but the limitations of computers force us to make compromises all the time between accuracy and effciency.

Computing with numbers (integers and reals) is a case in point; although the manipulation of numbers was the very reason why computers were invented in the first place (in the late 30s and early 40s), the problem of number representation is still not solved in today's main-stream languages.

In this talk I will explain what the issues are, starting briefly with the representation of integers, and then move on to the real numbers. A large part of the talk will be devoted to the shortcomings of floating point representation, and if there is time I will explain how one can represent and manipulate real numbers without loss of accuracy.

If you would like to get into the right mood for this lecture then use your pocket calculator, computer, or the internet to find out what the value of sin(10^40) is.

Descriptive and Computational Complexity

Anuj Dawar (University of Cambridge)
Friday Feb 16, 14:30 in Ben LT5 (Host: Jose Fiadeiro)

In this talk I will introduce the study of descriptive complexity and compare it to the more classical notion of computational complexity. This will be motivated by the study of languages for generic queries in relational databases. I will review Fagin's well-known theorem giving a descriptive characterisation of NP - the class of problems decidable nondeterministically in polynomial time. I will also describe current progress on the long standing open problem of obtaining a descriptive characterisation of P.

Slides of the talk, background information: E. Grädel, Finite model theory and descriptive complexity, in Finite Model Theory and Its Applications, Springer-Verlag, 2007, and the recent paper which contains the result mentioned near the end of the talk: A. Atserias, A. Bulatov and A. Dawar Affine Systems of Equations and Counting Infinitary Logic, preprint NI07002-LAA, Isaac Newton Institute of Mathematical Sciences (2007).

Dynamics in Knowledge, Belief and Preference

Dick de Jongh (Amsterdam)
Friday Feb 23, 14:30 in Ben LT5 (Host: Alexander Kurz)

A new approach to preference in logic is developed. There is a basis of properties (issues, priorities, constraints) from which preference over objects is constructed. First, this preference relation is constructed directly (objective preference, betterness), afterwards belief is interposed in the construction (real, subjective preference). The latter opens the possibility of interpreting preference logic in epistemic-doxastic logic, the logic of knowledge and belief (of agents). The dynamic form of this logic, DEL (dynamic epistemic logic), developed by Gerbrandy, van Benthem, Baltag and others, can account for changes brought about by new information available to the agents. For belief statements this was done by introducing conditional belief, belief under certain assumptions. In our approach conditional preference takes its place naturally, and in this manner preference logic can take advantage of the attainments of DEL. The talk will require little or no prior knowledge. It is based on work with Fenrong Liu, Optimality, Belief and Preference, ILLC 2006.

Slides in pdf and ps

Complete Sequent Calculi for Induction and Infinite Descent

James Brotherston (Imperial College)
Friday March 2, 14:30 in Ben LT5 (Host: Fer-Jan de Vries)

I will give an overview of a paper recently submitted by myself and Alex Simpson, which is based upon (some of) my PhD work under his supervision at LFCS in Edinburgh.

We give completeness and cut-eliminability results for two different styles of reasoning with inductively defined predicates, each style being encapsulated by a corresponding sequent calculus proof system.

The first system supports traditional proof by induction, with induction rules formulated as sequent rules for introducing inductively defined predicates on the left of sequents. We show this system to be cut-free complete with respect to a natural class of Henkin models; the eliminability of cut follows as a corollary.

The second system uses infinite (non-well-founded) proofs to represent arguments by infinite descent. In this system, the left rules for inductively defined predicates are simple case-split rules, and an infinitary, global condition is imposed on proof trees to ensure soundness. We show this system to be cut-free complete with respect to standard models, and again infer the eliminability of cut.

The second infinitary system is unsuitable for formal reasoning. However, it has a natural restriction to proofs given by regular trees, i.e., to those proofs representable by finite graphs. This restricted "cyclic" system subsumes the first system for proof by induction. We conjecture that the two systems are in fact equivalent, i.e., that proof by induction is equivalent to regular proof by infinite descent.

Abstract Syntax: Substitution and Binders

John Power (Edinburgh)
Friday March 9, 14:30 in Ben LT5 (Host: Vincent Schmitt)

We summarise Fiore et al's paper on variable substitution and binding, then axiomatise it. Generalising their use of the category $\FF$ of finite sets to model untyped cartesian contexts, we let $S$ be an arbitrary pseudo-monad on $\Cat$ and consider $(S1)^{op}$: this generality includes linear contexts, affine contexts, and contexts for the Logic of Bunched Implications. Given a pseudo-distributive law of $S$ over the (partial) pseudo-monad $\mathit{T_{coc}}- = [(-)^{op},Set]$ for free cocompletions, one can define a canonical substitution monoidal structure on the category $[(S1)^{op},Set]$, generalising Fiore et al's substitution monoidal structure for cartesian contexts: this provides a natural substitution structure for the above examples. We give a concrete description of this substitution monoidal structure in full generality. We can then give an axiomatic definition of a binding signature, then state and prove an initial algebra semantics theorem for binding signatures in full generality, once again extending the definitions and theorem of Fiore et al. A delicate extension of the research includes the category $Pb(Inj^{op},\Set)$ studied by Gabbay and Pitts in their quite different analysis of binders, which we compare and contrast with that of Fiore et al.

Rank/select operations on large alphabets: a tool for text indexing

Srinivasa Rao (IT University Copenhagen)
Friday March 16, 14:30 in Ben LT5 (Host: Rajeev Raman)

Joint work with Alexander Golynski (University of Waterloo, Waterloo, ON, Canada) and J. Ian Munro (University of Waterloo, Waterloo, ON, Canada)

We consider a generalization of the problem of supporting rank and select queries on binary strings. Given a string of length n from an alphabet of size \sigma, we give the first representation that supports rank and access operations in O(\lg \lg \sigma) time, and select in O(1) time while using the optimal n \lg \sigma + o(n \lg \sigma) bits. The best known previous structure for this problem required O(\lg \sigma) time, for general values of \sigma. Our results immediately improve the search times of a variety of text indexing methods.

Indexed Data Types

Neil Ghani (University of Nottingham)
Friday March 30, 14:30 in Ben LT5 (Host: Alexander Kurz)

Abstract: Traditional data types such as the natural numbers can be described as inductive types. Lists are slightly more complicated in that for each type X, we have the type List X - we may say that lists thus form a family of inductve types indexed by types.

The last ten years have seen increasing interest in more sophisticated examples of types which are not families of inductive types, but rather inductive families of types. I will explain the intution behind this word play and consider the possibilities for indexing. Indexing by types leads to an impredicative system much like Haskell. The alternative is to index by terms which leads to a dependent type system as favoured by languages such as Agda and Epigram.

I will compare the two approaches and provide a shocking conclusion ...

Slides in pdf

Efficient P2P Overlay Systems using Multidestination Multicast Routing

Friday Mai 11, 14:30 in Ben LT5 (Host: Stephan Reiff-Marganiec)

Structured P2P systems come in two flavours: multi-hop and one-hop overlays. One-hop overlays offer significant latency reduction compared to multi-hop overlays, but at a cost of increased maintenance traffic and routing table size. However, many peer-to-peer overlay operations are inherently parallel and this parallelism can be exploited by using multi-destination multicast routing, resulting in significant message reduction in the underlying network.

This talk examines two techniques for routing table maintenance: active stabilisation using EDRA (Event Detection and Reporting Algorithm) and opportunistic updating using the EpiChord algorithm. Some errors in EDRA are identified, which lead to incorrect event detention and propagation, and appropriate solutions proposed.

Using simulation, message savings in the two algorithms are evaluated when multi-destination multicast routing is used in place of unicast messages. It is shown that the message overhead in one-hop overlays can be significantly reduced using this approach.

Finally a variable hop approach is introduced which combines the opportunistic and active maintenance mechanisms in a single overlay.

Action-state based Model Checking

Stefania Gnesi (ISTI-CNR, Pisa, Italy)
Monday June 18, Tuesday June 19 , 10:00 in KE LT3 (Host: Jose Fiadeiro)

These talks aim to present the possibilities offered by model checking tools for the verification of distributed, mobile, object-oriented systems, modelled as variants of Labelled Transition Systems. An action-state based logical framework for the analysis and verification of complex systems will be presented and related with classical state based logics using instead Kripke structures as semantic model. The defined logic combines the action paradigm, classically used for describing systems using labelled transitions systems together with the predicates that are true over states as captured using Kripke structures. Model checking algorithms and tools for this logical framework will be also discussed.

### Semester 1

#### Seminar details

Embodied computation

Susan Stepney (University of York)
Friday Oct 6, 14:30 in Ben LT5 (Host: Jose Fiadeiro)

Biological processes are made from physical material, they are situated in and interact with a physical environment, and they are constrained by physical laws such as conservation of matter and energy. Software systems, on the other hand, are informational, exist in the virtual world of the computer, and labour under no such constraints. How does this difference matter? Can the advantages of embodiment be achieved in virtual environments? What are design principles for embodied computational systems? Slides

Algorithms for Wireless Ad-Hoc Networks

Thomas Erlebach (University of Leicester)
Friday Oct 13, 14:30 in Ben LT5 (Host: Jose Fiadeiro)

In recent years there has been an increasing interest in wireless ad-hoc networks. Contrary to wired networks and cellular networks, there is no fixed infrastructure and the network is formed spontaneously by the participating nodes. Questions such as efficient topology control and routing lead to interesting algorithmic problems. We will give an introduction to this topic and then discuss some algorithms for unit disk graphs, a popular simplified model for wireless ad-hoc networks.

Hyper-computation with Newtonian machines

John Tucker (University of Wales Swansea)
Friday Oct 20, 14:30 in Ben LT5 (Host: Jose Fiadeiro)

Pelorus - getting to where you want to be

Vic Stenning (Anshar Ltd)
Friday Oct 27, 14:30 in Ben LT5 (Host: Jose Fiadeiro)

Pelorus is a tool for formulating and delivering change within a business, whether at the level of overall strategy, a single programme or a specific project. It helps to address and 'dissolve' many of the problems of change and, by so doing, increases the probability of meeting objectives and delivering the desired outcomes. Key themes include the active participation of all stakeholders, collective responsibility, dialogue, alignment, continuous learning, dynamic adjustment, and convergence.

EDAs and Markov Networks

John Mc Call (Robert Gordon University, Aberdeen)
Friday Nov 3, 15:30 in Ben LT5 (Host: Shengxiang Yang)

Estimation of Distribution Algorithms (EDA) are derived from Genetic Algorithms. In an EDA, a probabilistic model is constructed from a population of solutions. The model is then sampled repeatedly to generate a successor population of solutions, thus replacing the traditional use of genetic operators to breed children from selected solutions. EDAs apply selective pressure by "estimating the distribution" of good solutions. A common approach is to select good solutions from the population and then construct a joint probability distribution of solution variables. The jpd is represented using a Bayesian Network and an armoury of techniques now exists to build a Bayesian Network from a population of solutions. Sampling the jpd then generates the next population. In this talk, I will describe how Markov Networks can be used to estimate the jpd. The approach has benefits in improving evolution but at some computational expense in building the model. I will demonstrate the costs and benefits of a Markov Network EDA by comparing with other EDAs on a range of problems.

Parameterised Proof Complexity: Complexity Gap for Tree-like Resolution (joint work with B. Martin and S. Szeider)

Stefan Dantchev (University of Durham)
Friday Nov 10, 14:30 in Ben LT5 (Host: Michael Hoffmann)

I will announce the strange engagement of two areas of Computational Complexity that have so far known very little about each other, Propositional Proof Complexity and Parameterised Complexity. The "big" motivation that brought them together is a general programme for separating FPT and W[2], inspired by and very similar to the NP vs co-NP programme of Cook and Reckhow. I will then prove a specific result in the newly created area of Parameterised Proof Complexity, the so-called Complexity Gap for Parameterised Tree-like Resolution. The gap for (classical) Tree-like Resolution has been know for quite a while; it is a dichotomy theorem that characterises and separates the propositional tautologies expressible in First-Order Logic that are easy for Tree-like Resolution from the ones that are hard. Our theorem refines the hard case by splitting it into two sub-cases, the easier of which is a fixed-parameter tractable. The separating criterion refers to the existence of a finite dominating set in a certain infinite hyper-graph.

The query equivalence problem for XML path languages

Balder ten Cate (University of Amsterdam)
Friday Nov 17, 14:30 in Ben LT5 (Host: Alexander Kurz)

XPath is a language for navigating XML documents. It is part of the W3C standard XML querying and processing languages XQuery and XSLT. From the perspective of logic, XPath can be understood as a variant of modal logic interpreted on finite trees. In this talk, I will discuss two "logical" aspects of XPath (as well as of some variants of the languages proposed in the literature):

- Expressivity and succinctness: Which paths through XML documents can be described in XPath, and how succinctly? One way to answer this is by comparing XPath to more well established and understood languages such as first-order logic.

- Static analysis: What is the complexity of testing whether two XPath expressions are equivalent (always give the same answer)? Can we find a complete set of equivalence-preserving rewrite rules (i.e., so that every two equivalent expressions can be rewritten to each other using these rules)?

Based on joint work with Maarten Marx, and with Carsten Lutz.

Reasoning about Code Pointers (Separation Logic for Higher-Order Store)

Bernhard Reus (University of Sussex)
Friday Nov 24, 14:30 in Ben LT5 (Host: Alexander Kurz)

Separation Logic is a sub-structural logic that supports local reasoning for imperative programs with dynamic memory. It was designed to elegantly describe sharing and aliasing properties of heap structures, thus facilitating the verification of programs with pointers. Various flavours of separation logic have been developed for heaps containing records of basic data types. However, languages like C or ML allow procedures to be stored on the heap. Such type of heap is commonly referred to as "higher-order store." This talk addresses the problem of lifting Separation Logic from first-order to higher-order store.

We will briefly introduce Separation Logic, explain what we mean by higher-order store, define a simple imperative language with dynamic memory and stored procedures and present a Hoare-like program logic for it. The challenge is then to prove the correctness of the fundamental rule of Separation Logic (the Frame Rule) and of a rule dealing with implicitly recursive stored procedures. Denotational Semantics will be used to do this. Modeling higher-order store as recursive domains enables us to use powerful (and well established) results from Domain Theory. There is a slight complication however: as the semantics needs to be independent of the choice of locations we need to resort to a Kripke-style functor model.

This is joint work with Jan Schwinghammer, Programming Systems Lab, Saarland University.

Frequency Allocation in Wireless Communication Networks

Joseph Chan (King's College London)
Friday Dec 1, 14:30 in Ben LT5 (Host: Stanley Fung)

A mobile phone network usually has geographical coverage area divided into cells. Phone calls are serviced by assigning frequencies to them. In order to avoid interference, a typical way is to assign different frequencies to two calls emanating from the same or neighbouring cells. The frequency allocation problem is thus to minimize the span of frequencies used to serve all calls, without creating interference. In this talk we study both the offline and online versions of the problem. We also consider the variations such as different coverage models for the networks and a more general interference constraint.

Distributive lattice-structured ontologies

Mai Gehrke (New Mexico State University, University of Oxford)
Friday Dec 8, 14:30 in Ben LT5 (Host: Alexander Kurz)

This is joint work with Fischer Nilsson and Bruun of the Technical University of Denmark. We describe an implementation of a language that accommodates both ontologies and relational databases. The structures arrived at are finite distributive lattices with attribution operations that preserve all joins and binary meets. The preservation of binary meets allows these functions to model the natural join operation in databases. A crucial feature we believe to be new is the concept of terminal solution identifying a minimal faithful ontology generated by the inhabited points of a data set. The main tools we use are Kripke frames/Birkhoff duality and adjoint operations. The work generalises work by Frank Oles of IBM.

Refactoring Information Systems

Michael Löwe (Hannover, Germany)
Friday Dec 15, 14:30 in Ben LT5 (Host: Reiko Heckel)

We present a formal framework for the refactoring of information systems, including the data model and the data itself. The framework is described using category theory and can handle addition, renaming and removal of model objects as well as folding and unfolding within complete and partial object compositions. A medium-sized example (introduction of a role pattern into a customer database) demonstrates the applicability of the approach. demonstrates the applicability of the approach.

 Author: Alexander Kurz (kurz mcs le ac uk), T: 0116 252 5356.© University of Leicester . Last modified: 13th September 2010, 07:59:25Informatics Web Maintainer. This document has been approved by the Head of Department.