|
The list of invited speakers that have agreed to present a
talk includes:
- Muffy Calder (University of Glasgow)
- Ursula Martin (University of St. Andrews)
- Faron Moller (University of Wales, Swansea)
- Joachim Parrow (KTH Teleinformatik, Sweden)
- Mike Paterson (University of Warwick)
- Simon Peyton-Jones (Microsoft UK)
- Alexander Rabinovich (University of Edinburgh)
A Day in the Life of a Spin Doctor
The design of any concurrent system, particularly one with
synchronous and/or asynchronous communication, can be
very difficult. What kind of investigations should you
carry out to ensure that you have the got the system you intended,
that what you intended is reasonable, and that you will get an
answer within a reasonable period of time?
In this talk I will examine these questions within the context of
G. Holzmann's Promela language and the model-checker Spin.
Promela is a C-like language that supports synchronous and
asynchronous communication, concurrency, and dynamic
communication; Spin supports checking generic and
domain specific properties, the latter as linear temporal
logic. I wil survey some of the more interesting aspects of both
with special consideration to practical tips for making reasoning tractable.
Computational math: the new challenge for computational logic
Scientific computation based on continuous computational mathematics
is widely used for applications as diverse as high energy physics,
weather forecasting, environmental and financial modelling, and is
becoming important in systems design for engineering applications
like air-traffic control algorithms or synthesising code for control
systems. Complex models and simulations are among the most demanding
of computer power. The leading commercial software systems such as
Maple 6, MATLAB and NAG have around 2 million users, and scientists
and engineers have in-house code for many specialised applications.
Computational mathematics systems may be numeric or symbolic: both
can be subject to error and problems of scale, and lack a framework
for reasoning about the models they implement. Computational logic
systems allow such reasoning, and do the underlying mathematics
analytically, so we can rely on the answers they produce.
We give an overview of recent work at St Andrews and elsewhere in
applying computational logic to computational mathematics, and set
out some challenges:
- for its immediate application as an effective component of
mathematical
software such as Maple or for representing mathematical
knowledge as part
of endeavours like OpenMath/MathML
- for the use of computational logic techniques to support
applied math
and mathematical modeling, particularly in areas where the
highest
degree of assurance is required, such as avionics
- for developing a strategy for the representation, validation
and
communication of mathematics and science in a future where the
opportunities and challenges of digitally embodied knowledge
may
radically change scholarship and scientific discourse
Techniques for decidability and undecidability for bisimilarity
In this tutorial we describe general approaches to deciding
bisimilarity between vertices of (infinite) directed edge-labelled
graphs. The approaches are based on a systematic search following the
definition of bisimilarity. We outline (in decreasing levels of
detail) how the search is modified to solve the problem for finite
graphs, BPP graphs, BPA graphs, normed PA graphs, and normed PDA
graphs. We complete this by showing the technique used in the case of
graphs generated by one-counter machines. Finally, we demonstrate a
general reduction strategy for proving undecidability, which we apply
in the case of graphs generated by state-extended BPP (a restricted
form of labelled Petri nets).
Tutorial: An introduction to the pi-calculus
The pi-calculus is a process algebra where agents
communicate by sending communication ports, or capabililtes, to each other. In this
introduction I shall present some of the basic ideas and intutions and give
a small modelling example from mobile telephony
Recommended reading: intro.ps
Getting your message across, but nicely :
an introduction to contention resolution
When independent processes compete for a limited resource,
such as a communication channel, interesting combinatorial
and probabilistic questions are raised. Some old and
some new results on contention resolution protocols will
be described, though major open problems remaining.
Asynchronous Exceptions in Concurrent Haskell
There are some applications for which the ability to interrupt a computation cleanly is essential.
Timeouts and user interrupts are two common examples.
Recovering from such asynchronous exceptions is problematic, because
they may interrupt the computation at a bad moment. So problematic, in fact,
that most languages do not support asynchronous exceptions at all; instead
the application must poll an alert flag at regular intervals.
In my talk I will present a design for asynchronous exceptions in Concurrent
Haskell. Unusually, we have a complete operational semantics for the language,
including the asynchronous-exception part. My hope is that Colloquium
participants may be inspired to develop a usable theory for this semantics.
Temporal Logic over Branching Time: Expressiveness and Complexity
Many temporal logics were suggested as branching time specification formalisms
during the last 20 years. These logics were compared against each
other for their expressive power, model checking complexity and succinctness.
Yet, unlike the case for linear time logics, no canonical temporal logic
of branching time was agreed upon.
In this talk we offer an explanation for the multiplicity of temporal logics
over branching time and provide an objective quantified `yardstick' to measure these logics.
|
