Matteo Acclavio visiting Swansea

Next week's theory seminar will be given by Matteo Acclavio from the University of Sussex, who is visiting us for a few days. The topic will be a new logical framework for concurrent programs, abstract below.

Title: A new logical framework for concurrent programs

Abstract:
Designing logical frameworks to reason about the properties of concurrent programs while accurately capturing the essence of concurrency is a challenging task.
The main difficulties can be traced back to the syntactic constraints of the languages used for this purpose.

In this talk, I will present my ongoing line of research, which aims to provide a new computation-as-deduction paradigm for the study of concurrent programs.
In particular, I will show you a non-commutative logic where we can interpret proofs as computation trees for the pi-calculus, and use proof nets to provide canonical representations of these trees modulo interleaving concurrency.

This work is based on joint works with Giulia Manara and Fabrizio Montesi

Next week's Theory Seminar Series

Next week Troy will give a talk on Conceptualising Programming Language Semantics as a part of our seminar series.

Abstract:

Research on the semantics of programming language has tended towards formalisation. Following the successful deployment and myriad uses of formal syntax, many of those working on semantics assumed similar successes would be realised with formal semantics. 

The reality was different, and the resultant language specifications were large, complicated, technical artefacts. My previous historical research has studied those from a technical perspective. 

In this talk, I will explore the conceptual surroundings of the semantics, examining the use of metaphors, analogies, and illustrative language used to accompany or explain the formal documents.

It is early stage research and will focus primarily on picking examples from the history of semantics for deeper analysis in the future.

I will also present some philosophical frameworks I am considering for use in this analysis and begin to discuss how they might help us understand the topic.

This research will ultimately lead to a conference presentation and journal article next year, as well as forming a pilot study for a research grant proposal.

Galileo Sartor's talk

Today's theory seminar talk will be by Galileo Sartor on "Representing and reasoning with legal aspects of traffic rules for autonomous vehicles". 

Abstract:

In this talk, I will give an overview of a modular system for representing and reasoning with legal aspects of traffic rules for autonomous vehicles.
We focus on a subset of the United Kingdom's Highway Code (HC) related to junctions.
As human drivers and automated vehicles (AVs) will interact on the roads, especially in urban environments, we claim that an accessible, unitary, high-level computational model should exist and be applicable to both users.
Autonomous vehicles introduce a shift in liability that should not bring disadvantages or increased burden on human drivers.
The proposed system is built of three main components: a natural language interface, using Logical English, used to encode the rules; an internal representation of the rules in Prolog; and a simple multi-agent-based simulation environment, built in NetLogo. The three components interact: Logical English is internally translated in Prolog, and the resulting code (along with some support code) interfaces with NetLogo with a bridge.
Such a modular approach enables the different components to carry different ``burdens'' in the overall system; it also allows replacing modules.
With the NetLogo simulation, we can visualize the effect of the modeled rules as well as validate the system with a simple dynamic running scenario.
Designated agents monitor the behaviour of the vehicles for compliance and record potential violations where they occur. The information on potential violations is then utilized by validator agents, to determine whether the violation is punishable, differentiating between exceptions and cases.

Georg Moser visiting

Georg Moser, Prof of Computer Science at University of Innsbruck, is visiting again this week to continue our work on the Royal Society funded project MARRY: MARRYing the analyses of feasible algorithms and problems.

An introduction to effective fractal dimension by Benjamin Koch

Today's theory seminar will be given by Benjamin Koch, who will give as an introduction to effective fractal dimension. 

Abstract:

The purpose of this talk is to give an overview of effective fractal dimension, which is an application of computability theory to geometric measure theory. I will start with an overview of two of the most important notions of dimension in classical measure theory, the Hausdorff and packing dimensions. Following this will be the formulation of so-called effective dimensions for points in R^n via Kolmogorov complexity. The highlight of the study of effective dimension thus far has been the “point-to-set principle”, which connects the effective dimension of points in R^n to the classical dimension of the subsets in which they reside. I will discuss a handful of the results that have come from this connection, which include an alternate proof of the Kakeya conjecture in R^2, an improved lower bound on the Hausdorff dimension of Furstenburg sets (which generalize Kakeya sets in R^2), and a generalization of an upper bound on the Hausdorff dimension of intersections and products of subsets of R^n

Theory Seminar Series

The theory seminar tomorrow will be given by Eike on "Robust Decidability of Escape Problems for General Non-Linear Systems."

Abstract:
A wide range of problems from a diverse range of areas can be formulated as "escape problems": does a given point escape a set under the iteration of a function, or do all points in a given set escape the set under the function.

The decidability of these problems is almost exclusively studied under the assumption that points, functions, and sets are specified exactly by a finite amount of data (e.g. rational or algebraic parameters). In this setting, positive results are largely limited to linear systems, since already very simple non-linear systems can have undecidable escape problems.

When working with systems that involve real data, say, coming from scientific or engineering applications, the assumption that the system be known to infinite precision is arguably unrealistic. One should rather assume that the system is known only up to finite precision. In that case, the natural question becomes whether the system's behaviour -- escaping or not escaping -- is robust under all sufficiently small perturbations. On the one hand, this requires us in some sense to do more than to decide the problem for a single given point at a time. On the other hand, there appears to be little value in determining the status of problem instances that lie on a "decision boundary", i.e. instances that are not robust under small perturbation. The latter point is interesting in light of the aforementioned undecidability results in the discrete-data setting, which appear to rely on the existence of very difficult non-robust instances.

The aim of this talk is to demonstrate by means of a case study that computable analysis constitutes an excellent framework for the discussion of robust decidability questions, such as the above. I will study to escape problems for very general non-linear systems and show at least in one case that the problem becomes as close to decidable as one can hope it to be in this setting. The Point Escape Problem is to decide for a given continuous map f, a given closed set A, and a given point x in A whether x escapes A under iteration of f. The Set Escape Problem is to decide for a given continuous map f and a given compact set K whether all points of K escape K under iteration of f. I will give a complete algorithm for the Point Escape Problem and a potentially not complete algorithm for the Set Escape Problem.  I will show that both algorithms terminate generically, and discuss some concrete examples of termination problems.

Talk on Assuring non-functional requirements

This summer & autumn, our department is hosting Prof Magne Haveraaen (University Bergen, Norway)
 
As part of his involvement in ∆QSD group, he is organising a seminar talk:
 

“Assuring non-functional requirements”

Presented by Neil Davies (Bristol) and Peter Thompson (Predictable Network Solutions)

Friday, 4. 11, 14:00

CoFo 401

 
Abstract.
Great progress has been made in assuring the functional correctness of digital systems. Coverage analysis, property-based testing, mock environments and formal proof systems can be applied to give very high levels of confidence of correct system behaviour. (That they are all too often not applied is a problem in social science, not computer science!). Despite this, many prototypes that demonstrate attractive functionality in a laboratory or test setting fail to deliver when deployed in the real world, often because non-functional aspects such as response time, efficiency, reliability or safety are unsatisfactory. These are typically not properly addressed until the system is largely implemented, when it may eventually become apparent that early design decisions were ill-advised, and changing them is expensive or even impossible. 

Our ongoing goal, a journey that we began over 20 years ago, is to quantify ‘non-functional’ requirements in such a way that they can be treated on an equal footing with functional ones at all stages of the development and deployment process. This abstracts the inherent stochastic variability of the real-world as a data type used in reasoning about timeliness and resource consumption. Such system properties can be calculated at any stage of system development, from early design considerations to deployed systems. In many critical situations, delivering a response within a given time-bound is as much a requirement as the correctness of the answer, as is doing so within the available resources. This approach also informs the way that system performance can be measured for effective in-life management and maintenance throughout the full system life cycle.

This seminar will provide an overview of our journey so far, how we are reasoning about timeliness and “failure” using a formalism (with prototype tool support) called ‘∆QSD’. We will provide examples of how this can inform “design intuition”; capture reliability; and act as a socialisation tool with stakeholders in a complex development.
 
References
Haeri, S.H.; Thompson, P.; Davies, N.; Van Roy, P.; Hammond, K.; Chapman, J. Mind Your Outcomes: The ∆QSD Paradigm for Quality-Centric Systems Development and Its Application to a Blockchain Case Study. Computers 2022,11,45. https://doi.org/10.3390/computers11030045
Seyed Hossein Haeri, Peter W. Thompson, Peter Van Roy, Magne Haveraaen, Neil J. Davies, Mikhail Barash, Kevin Hammond, James Chapman: Algebraic Reasoning About Timeliness. 16th Interaction and Concurrency Experience (ICE 2023) EPTCS 383, 2023, pp. 35–54, doi:10.4204/EPTCS.383.3
 
Presenters
Dr Neil Davies, BSc, PhD, MBCS, CEng, CITP
Neil Davies is an expert in resolving the practical and theoretical challenges of large scale distributed and high-performance computing, particularly scalability effects in large distributed systems, their operational quality, and how to manage their degradation gracefully under saturation and adverse operational conditions. He is a computer scientist,
mathematician and hands-on software developer who builds rigorously engineered working systems and scalable demonstrators of new computing and networking concepts.
Throughout his 20-year career at the University of Bristol he was involved with early developments in networking, its protocols and their implementations. He collaborated with organisations such as NATS, Nuclear Electric, HSE, ST Microelectronics and CERN on issues relating to scalable performance and operational safety. He was also technical lead on several large EU Framework collaborations relating to high performance switching, and has mentored PhD candidates at CERN. 
 
Peter Thompson, BSc
Peter Thompson joined Predictable Network Solutions after several years as Chief Scientist of GoS Networks Limited (formerly U4EA Technologies). Previously he was co-founder and CEO of Degree2 Innovations, commercialising advanced research into network QoS undertaken with Neil Davies during the preceding four years at the Partnership in Advanced Computing Technology in Bristol, England, where he was a Senior Research Fellow. 
Before that he spent eleven years at STMicroelectronics, where one of his numerous patents for parallel computing and communications received a corporate World-wide Technical Achievement Award. For five years he was the Subject Editor for VLSI and Architectures of the journal Microprocessors and Microsystems, published by Elsevier.