Lab Lunch Talks 2008

I will demonstrate an application for displaying Mandelbrot Curves and Julia Curves that responds in real time, implemented by an MSc student, Iain Parris. I'll review some of the theory, demonstrate a phenomenon I've not seen described elsewhere, and pose some questions.

We implement statically-typed multi-holed contexts in OCaml using an underlying algebraic datatype augmented with phantom types. Existing approaches require dynamic checks or more complex type systems. In order to support concatenation we use two type parameters to represent the number of holes in a context as the difference between two Peano numbers. In order to support plugging a context with contexts of different arity we introduce a datatype of lists of contexts of length n with a total of m holes. Further, we extend our representation to allow holes to be marked with additional type information. As an example, we use these marks to implement statically-typed multi-holed XHTML contexts. We take advantage of Garrigue's relaxed value restriction.

When the technology to build quantum computers finally becomes available, it is highly likely that it will only be accessible to a handful of centers around the world. Much like today's rental system of supercomputers, users will probably be granted access to the computers in a limited way. This begs the question: how will the users interface with the quantum computer? We present the first protocol which allows Alice to have Bob carry out a quantum computation for her such that Alice's inputs, outputs and computation remain perfectly private, and where Alice does not require any quantum computational power or memory. She only needs to be able to prepare single qubits from a finite set and send them to Bob, who has the balance of the required quantum computational resources. Our protocol is interactive and from Alice's point of view, can be implemented with physical systems that are already available and well-developed.

I shall give a report on the Workshop on XML, Logic, and Automata held in Grantown-on-Spey in July, just before the ICMS workshop on Logic and Algorithms here. I'll mention some of the memorable talks and give abridged versions of two less memorable talks (given by me: one introduced an analog of the Vardi-Wolper construction for reasoning about XML, and the other introduced the basics of whisky tasting).

A finite automaton over a unary alphabet can be thought of as recognizing a set of numbers. A standard undergraduate result is that this set is always representable as a union of arithmetic progressions. In particular, if we start with a deterministic automaton, then we can compute such a representation in linear time. [We use unary representation for numbers to strengthen the result.] A slightly less well-known result proven by Marek Chrobak in the late 80's is that, if we are given a nondeterministic automaton, then there *exists* an equivalent representation as a union of arithmetic progressions incurring only a quadratic blow-up. However, it is an open problem whether there exists a polynomial time that can compute such an equivalent representation given a nondeterministic automaton as input. Chrobak's original construction runs in exponential time and only very recently it has been improved to quasi-polynomial time. Mere curiosity aside, a polynomial-time algorithm for this problem will yield a substantial improvement in some model checking problem and NFA minimization problem for unary languages. In this talk, I intend to give Chrobak's original construction and, if time permits, Litow's recent improvement to quasi-polynomial time.

I am editor-in-chief of the journal Theoretical Computer Science. I will talk about what goes on behind the scenes at a journal and some of the issues in scientific publishing, including the currently fairly hot issue of open access. My journal is published by Elsevier, the world's largest commercial publisher of science journals, and my views are partly coloured by that fact, but in this talk I will not be speaking for Elsevier.

We present an application of partial evaluation to performance models expressed in the PEPA stochastic process algebra. We partially evaluate the state-space of a PEPA model in order to remove uses of the cooperation and hiding operators and compile an arbitrary sub-model into a single sequential component. This transformation is applied to PEPA models which are not in the correct form for the application of the fluid-flow analysis for PEPA. The result of the transformation is a PEPA model which is amenable to fluid-flow analysis but which is strongly equivalent to the input PEPA model and so, by an application of Hillston's theorem, performance results computed from one model are valid for the other. We apply the method to a Markovian model of a key distribution centre used to facilitate secure distribution of cryptographic session keys between remote principals communicating over an insecure network. [This is joint work with Allan Clark, Adam Duguid and Mirco Tribastone.]

I will talk about a current proposal by Bracha, Gafter, Gosling and von der Ahe for adding closures (a.k.a. lambda abstractions) to the Java programming language. One of the intriguing features of this proposal is the chosen semantics of "return" statements (for returning from method calls). However, according to the current proposal, it is possible to write programs that result in a runtime error because a "return" statement has nowhere to return to. It would be nicer if one could prevent this via some statically enforced restriction on programs. I will describe a possible solution to this problem, drawing on ideas that have arisen from work on my own programming language Eriskay.

What could the words in the title possibly have to do with each other? I'll say some things about this. I'll try to keep things mildly amusing and non-technical, since this is lab lunch. If people can stomach it, I can give a more technical talk (based on the same paper) later as a seminar. (Based on a joint paper with Andreas Lochbihler: "The computational complexity of evolutionarily stable strategies", Int. J. of Game Theory, 2008.)

It is now fairly common to be at a seminar where the speaker expresses surprise that the projected colours are not what he/she saw on the computer display. I will discuss the issues involved with getting consistent colour in the digital domain and explain why it would be surprising if the colours were right (for the systems as used). The talk will be based around the notion of a workflow, e.g., from scanner to display and to printer. I will illustrate briefly the use of some analysis tools which are useful in making compromises forced on us by significant differences in colour gamut of the various stages. This is a recreational talk and no previous knowledge will be assumed. It will last around 50 minutes.

This week (21–24/01), we are hosting the 6th Old World Conference on Phonology.

In case LFCS members wonder about any strange noises from G.07, I thought I'd give a crash survey of phonetics/phonology, concentrating on the wide range of possibilities used in language worldwide — based on the eponymous book, CD and web site by Ladefoged and Maddieson.

This is a recreational talk, and audience participation will be invited. In particular, if you expect to attend, and your native language is not English, German or Greek (which I will assume present), please let me know, so I can choose some of my demos to match the available live speakers.

The talk will include a (recorded!) example of what is almost certainly the world's most unpronounceable natural language.

How we brought high-speed Internet access to one of the remotest parts of Scotland, and why some theory is needed.

I'll talk about my recent trip to Bangalore for the Asian Symposium on Programming Languages and Systems on behalf of the Links project, summarize some of the talks I saw, and show some photos that I took in Bangalore and Mysore.

My last Lab Lunch talk was in February 2000 shortly before I retired, so I will say something about my connection with Edinburgh and LFCS, then a little what I have been doing and thinking about since.

Doing: Spending much of my time and energy practicing and studying in the Indo-Tibetan Buddhist tradition. Keeping up a little with computing. Reading too many books.

Thinking: About all sorts of things, but often centered round the understanding of mind from computing and linguistics on the one hand, and from the perspective of meditation experience on the other hand. In particular what is the basis of out human conceptual system and how is it organised? What is non-conceptual mind?

In this talk I will give a perspective on Semidefinite Programming (SDP). Most of you know Linear Programming (LP). SDP is more general: while in LP we optimize over a polyhedron, in SDP the domain is the cone of positive semidefinite matrices. This entails that SDP is more expressive. In fact, SDP has led to quite a few interesting algorithms for combinatorial problems, of which I hope to mention a few. A drawback, however, is that solving SDPs is computationally a "heavier" task than solving LPs. There has been some recent progress on the latter problem, which I hope to sketch briefly. A more detailed discussion will be the subject of next week's Algorithms and Complexity meeting!

It was only a matter of time, that is, before I managed to find a game-theoretic angle on what I'm most interested in these days, viz., bidirectional model transformations written in the OMG's standard QVT Relations language. It turns out that the way in which transformations in this language are structured — which had been a cause for some confusion — is easily explained in terms of a two-player game reminiscent of those used in concurrency. Once we have this explanation, we can use the classic difference between simulation equivalence and bisimulation equivalence to show that one of the things commonly assumed about QVT-R transformations is Just Not True. This may go some way towards explaining the relative lack of uptake of the language, and suggesting how to remedy it.

I will try to keep the talk lightweight and handwavy, but there is a draft paper for anyone who would like details.

SPARK is a subset of Ada used in high-integrity software applications. The company Praxis UK provides tools for generating VCs (verification conditions) from SPARK programs annotated with assertions such as preconditions and postconditions, and for proving these VCs, both by automatic and interactive means. For a while now I've been interested in how improve the automation of VC proof by making use of SMT (SAT modulo theories) solvers. For a recent poster on this subject, see:

I'll talk about the current status of this project, ongoing work, and some possible future directions.

At Lab Lunch next week, I'll talk about some recent experiments and analysis that David Aspinall and I have performed to determine whether challenge questions are either a secure or usable form of authentication. Questions such as "What is my mother's maiden name?" or "What was the name of my primary school?" are ubiquitously used, despite a surprising lack of understanding as to whether they are secure from attack, or if the answers are actually memorable to users. A key contribution of our work was the creation of a security model that would allow us to better understand the protection offered by such questions.

Further information about our work, including recent presentations and publications, can be found at http://homepages.inf.ed.ac.uk/mjust/KBA.html.

I also thought it would be fun if LFCS members were able to contribute their own ideas for questions to this talk. I've set-up a short survey to collect these questions at http://tinyurl.com/LFCSQuestions09. If you would like to participate (anonymously), please do so PRIOR TO NOON ON MONDAY, and I can refer to the questions during the talk.

Based on a simple axiomatization of concurrent behaviour I will present two ways of observing parallel computations and show that in each case they are dual to conflict and causality, respectively. Such dualities are used to define the semantics of a modal logic, which is called Separation Fixpoint Logic (SFL). Most importantly, I will show that natural syntactic fragments of SFL capture the observable behaviour of several concurrent systems since the equivalence they induce coincide with the standard bisimulation equivalences for concurrency. Moreover, by defining a characteristic bisimulation game for the equivalence induced by SFL, it is shown that this equivalence is decidable as well as strictly stronger than a history-preserving bisimulation (hpb) and strictly weaker than a hereditary history-preserving bisimulation (hhpb). Therefore, such a bisimulation is the strongest decidable equivalence with respect to discriminating power for concurrent systems with partial order models. This study considers branching-time models of concurrency based on transition systems and petri net structures.

A full paper on this work can be found at: http://homepages.inf.ed.ac.uk/s0785782/abs_fossacs09.html

(no abstract)

Quantales are abstract algebras with a complete partial order and an associative operation, motivated, in part, by the example of binary relations on a set.

A topos is a (Beth-Kripke) model for higher-order constructive (Heyting) logic.

We discuss the representation of quantales as algebras of binary relations on an object in a suitable topos.

Bio-PEPA is a stochastic process algebra that supports modelling of biochemical reaction networks which can then be analysed in a number of ways. In this talk I will explain the motivations for the design of Bio-PEPA including the benefits which can be gained from supporting a suite of analysis techniques, and describe the reagent- centric modelling style which it supports. In addition to the language definition and previous case studies, I will outline areas of on-going work. For more details see http://homepages.inf.ed.ac.uk/jeh/Bio-PEPA/biopepa.html .

(no abstract)

While general infinite-state Petri nets are a very expressive model for concurrency and synchronization, their reachability problem (and other questions like termination and boundedness) is still decidable.

We consider extensions of Petri nets with real-time features (i.e., clocks and time constraints) and prices (assigning action costs to transitions and storage costs to places). Intuitively, such generalized priced timed Petri nets are to standard Petri nets as classic priced timed automata are to finite automata. While general reachability is undecidable for these extended Petri net models, other questions (like control-state reachability, termination, zenoness, and some version of boundedness) remain decidable. Moreover, the minimal required cost for reaching a given control-state is computable.

Finally, the problems for priced timed Petri nets have interesting connections to problems for other classes of systems, such as transfer nets, Petri nets with one inhibitor arc, and unreliable (i.e., lossy) counter machines.

Bio-PEPA is a stochastic process algebra for modelling biological systems, which supports different types of analysis. We are currently investigating semantic equivalences. In searching for suitable equivalences, we can consider existing equivalences from the literature. Alternatively, we can decide what behaviours we want to consider the same and develop an equivalence to capture this. This talk focusses on the second approach. Bio-PEPA models can be discretised into levels which represent different abstractions of the same system and hence we view different discretisations as having the same behaviour. This is our starting point for an equivalence called compression bisimulation. I will motivate and define this equivalence and present some results.

Rahul Santhanam: Perfect Rationality as Infinite Patience

Patience...

Kyriakos Kalorkoti: Sufficiency conditions for Bokut' Normal Forms

I will discuss sufficient conditions for the existence and uniqueness of normal forms of sequences of HNN extensions defined by Bokut'. The conditions are amenable to be used in automatic theorem provers. I will discuss also how to obtain a Gr\"obner-Shirshov basis form the rewrite rules of Bokut' normal forms. Finally an application drawn from a paper of Aaanderaa and Cohen will be mentioned briefly as an illustration.

Elham Kashefi: Iranian 2009 Election!

(no abstract)

Conor McBride(University of Strathclyde): Arrows of Outrageous Fortune

Assisted by a small extension to Haskell's kind and type system, allowing types to become kinds and simple expressions to stand in types, and implemented in the form of a preprocessor (the Strathclyde Haskell Enhancement), I explore improvements in precision for both data and control structures. Specifically, I examine the "IMonad" abstraction which falls naturally from the notion of index-preserving maps on indexed sets:

type s :-> t = forall i. s i :-> t i

IMonads model indexed notions of computation with indexed notions of value, where the index represents the state of the system with which computations interact. Through the Curry-Howard lens, an indexed notion of value is a predicate on states, and an IMonad, phi say, is a predicate transformer. The Kleisli arrow types, s :-> phi t, resemble Hoare triples, requiring postcondition t to be reachable if precondition s is satisified. Crucially, to produce such an arrow, one must be ready for any state which satisfies the precondition. Correspondingly, IMonads model computation in changing circumstances. For example, it's easy to give types to file-open and file-read which ensure that we can only read from a file if we know it has opened successfully.

Many real-world systems are more suitably modeled as infinite transition systems. Common sources of infinity include unbounded number of processes, unbounded stacks or queues, unbounded real or discrete valued variables, and clocks of unbounded size. Many formalisms for infinite transition systems have been proposed including CCS, pushdown systems, Turing machines, timed systems, Petri nets, Minsky counter machines, and various notions of finite-state transducers. Since verifying infinite transition systems is in general undecidable, one has to either resort to semi-algorithms for general formalisms, or complete algorithms for more restrictive formalisms. In this talk, I will offer a new perspective to designing semi-algorithms for verifying liveness over a general formalism for infinite systems with sound theoretical foundations and practical applicability. The technique can also be instantiated to yield complete (and asymptotically optimal) algorithms for many well-known formalisms like pushdown systems and restrictions of Petri nets and counter machines.