Formal Analysis, Theory and Algorithms (FATA)
Formal Analysis, Theory and Algorithms (FATA)
Overview
The FATA section is led by Professor Simon Gay. It develops and applies mathematics and logic to the design and analysis of algorithms and complex computational systems. We are especially interested in bringing the clarity and insight of formal theories to hard application problems of real practical significance. There are three main topics:
- Algorithms and Complexity
- Programming Language Foundations
- Formal Modelling and Analysis
Detailed topics include:
- algorithms for matching problems
- combinatorial search and optimization
- computational biology
- constraint programming
- graph algorithms
- modelling and analysis of complex and reactive systems
- phase transition phenomena in combinatorial problems
- probabilistic model checking
- process algebras
- programming language semantics and type systems
- quantum computation
- string algorithms
- telecommunications software and protocol analysis
- bigraphs
Many projects are collaborative, as the group aims to apply formal ideas to problems of genuine interest outside the formal community itself. Collaboration involves, for example, life scientists and communication system designers, companies in the telecommunications, software and pharmaceutical sectors, as well as government organisations.
Section members
Group photo, May 2017. Left to right: Prof. Simon Gay, Dr Alice Miller, Dr Ornela Dardha, Prof. Muffy Calder, Dr David Manlove, Ms Laura Voinea, Ms Sofiat Olamiji Olaosebikan, Dr Gethin Norman, Mr Craig Reilly, Dr Michele Sevegnani.
Group photo, September 2017. From left to right: Dr Michel Steuwer, Dr Patrick Prosser, Prof. Simon Gay, Prof. Muffy Calder, Dr Gethin Norman, Dr Alice Miller, Dr Ciaran McCreesh, Dr Oana Andrei, Mr Craig Reilly, Dr Ornela Dardha, Dr Roly Perera, Mr Florian Weber, Ms Frances Cooper, Mr Paulius Dilkas, Dr Kitty Meeks, Dr David Manlove, Ms Sofiat Olamiji Olaosebikan.
Academic Staff:
- Prof Muffy Calder (Professor of Formal Methods, Vice Principal & Head of College of Science and Engineering)
- Dr Ornela Dardha (Lecturer)
- Prof Simon Gay (Professor of Computing Science) - Section Leader
- Prof David Manlove (Professor of Algorithms and Complexity)
- Dr Kitty Meeks (Royal Society of Edinburgh Research Fellow)
- Dr Alice Miller (Senior Lecturer)
- Dr Gethin Norman (Senior Lecturer, Deputy Head of School)
- Dr Patrick Prosser (Senior Lecturer)
- Dr Michele Sevegnani (Lecturer)
Honorary Research Fellow:
Research Staff:
Research Students:
- Mr Benjamin Bumpus
- Ms Frances Cooper
- Mr William Kavanagh
- Mr Michael McKay
- Ms Sofiat Olamiji Olaosebikan
- Mr Craig Reilly
- Ms Jessica Ryan (FATA seminar convenor)
- Mr James Trimble
- Ms Laura Voinea
Associate Members:
Projects
Current:
- IP-MATCH: Integer Programming for Large and Complex Matching Problems (2017 - 2020) - Dr David Manlove (PI)
- Modelling and Optimisation with Graphs (2017 - 2020) - Dr Patrick Prosser (PI), Dr Ciaran McCreesh (Researcher Co-I)
- Science of Sensor Systems Software (2016 - 2020) - Prof Muffy Calder (PI)
- Exploiting Parallelism through Type Transformations for Hybrid Manycore Systems (2013 - 2018) - Prof Simon Gay (Co-I)
- From Data Types to Session Types: A Basis for Concurrency and Distribution (2013 - 2018) - Prof Simon Gay (PI)
Past:
- A Population Approach to Ubicomp System Design (2011-2017) - Prof Muffy Calder (co-I)
- Efficient Algorithms for Mechanism Design Without Monetary Transfer (2013-2016) - Dr David Manlove (PI)
- COST Action IC1201: Behavioural Types for Reliable Large-Scale Software Systems (2012-2016) - Prof Simon Gay (Chair)
- EPSRC Institutional Sponsorship Fund project: "New algorithms for paired and altruistic kidney donation" (October 2015 - March 2016) - Dr David Manlove (PI)
- EPSRC Impact Acceleration Account - Algorithms for Paired and Altruistic Kidney Exchange (01/01/2015-30/09/2015) - Dr David Manlove
- Kidney Exchange Data Analysis Toolkit (2011) - Dr David Manlove
- NHS Blood and Transplant project: "Optimising options and strategies for living donor kidney transplantation for incompatible donor-recipient pairs" (2012-2013) - Dr David Manlove (co-I)
- VPS: Verifying Interoperability Requirements in Pervasive Systems (2008-2012) - Prof Muffy Calder (co-I)
- Homework: Shaping Future User Domestic Infrastructure (2008-2012) - Prof Muffy Calder
- Stochastic process algebra modelling of ROS regulation in oxidative stress (2007-2011) - Prof Muffy Calder
- Molecular Nose (2007-2011) - Prof Muffy Calder
- ARTE: Advanced Symmetry Reduction Tools for Explicit State Model Checking - Dr Alice Miller
- Software for the National Matching Scheme for Paired Donation - Dr David Manlove
- QNET: Semantics of Quantum Computation - Dr Simon Gay
- MATCH UP: Matching Under Preferences - Algorithms and Complexity (2007-2010) - Dr David Manlove
- SIGNAL: Stochastic Process Algebra for Signalling Pathways (2007-2010) - Prof Muffy Calder
- QICS: QISC: Foundational Structures in Quantum Information and Computation - Dr Simon Gay
- Engineering Foundations of Web Services: Theories and Tool Support - Dr Simon Gay
- Algorithmics of Stable Matching Problems with Indifference - Dr David Manlove
- Quantum Computation: Foundations, Security, Cryptography and Group Theory - Dr Simon Gay
- Behavioural Types for Object-Oriented Languages - Dr Simon Gay
Compumatch
COMPUMATCH
...for finding collaborators in computing.
One of the things that makes theoretical computer science at the University of Glasgow special is our passion for applying our abstract knowledge to address real-world problems. Do you think your research could benefit from a collaborator in theoretical computer science? Our areas of expertise include optimisation, modelling, data analysis, and many more – and if we can’t help you ourselves, we’ll do our best to point you in the direction of somebody who can.
There are two ways to start your search for a computing collaborator:
1. Come along to our next drop-in session for a chat. These are advertised in the events list.
2. Complete our Compumatch enquiry form and send it to compumatch@dcs.gla.ac.uk.
A few success stories from our past interdisciplinary collaborations
Living-donor kidney exchange |
|||
By BruceBlaus [CC BY-SA 4.0 (https://creativecommons.org/licenses/by-sa/4.0)], from Wikimedia Commons |
People suffering from advanced stages of kidney disease have only two treatment options: dialysis or transplant. Transplantation is by far the better choice for both quality of life and life expectancy, but finding a donor who is both willing and medically compatible is hard. Enter the algorithm. By teaming up with computer scientists, surgeons have been able to perform over a hundred extra transplants per year in the UK through pooled kidney donations - a system which helps mitigate the medically compatible requirement through the use of clever algorithms to find compatible exchanges between donors and patients. |
||
Air navigation services assets management |
|||
When an asset fails in a critical air navigation service, how urgent is a repair? If we repair within 1 hour, 2 hours, or n hours, how does this affect the likelihood of service failure? Can a formal model support assessing the impact, prioritisation, and scheduling of repairs in the event of component failures, and forecasting of maintenance costs? These are some of the questions posed to us by a large organisation; we developed a stochastic framework to answer them. |
By Andrew Choy from Santa Clara, California (Flickr) [CC BY-SA 2.0 (https://creativecommons.org/licenses/by-sa/2.0)], via Wikimedia Commons |
||
Restricting the size of a livestock epidemic |
|||
Major livestock disease outbreaks such as the 2001 Foot and Mouth epidemic are hugely economically damaging, and a lot of research has been undertaken with the goal of ensuring that we never see a disease outbreak on this scale again. In this context, we designed an efficient algorithm to answer the following question: if we could – hypothetically – prevent disease being transmitted on a certain number of trade routes in Scotland, by how much could we reduce the worst-case epidemic size? |
Seminar series
FATA seminars are usually held on Tuesdays from 1pm to 2pm, see the Events tab for more details. If you would like to visit us to give a talk, please contact the FATA seminar convenor, Jessica Ryan.
Events this week
There are currently no events scheduled this week
Upcoming events
COMPUMATCH drop-in session
Group: Formal Analysis, Theory and Algorithms (FATA)
Speaker: COMPUMATCH
Date: 25 January, 2019
Time: 12:30 - 14:00
Location: Sir Alwyn Williams Building, 422 Seminar Room
All members of the university interested in forming research collaborations with colleagues in theoretical computer science are warmly invited to come and discuss their research problems. A light buffet lunch will be provided.
Weighted Congestion Games: Price of Stability, Price of Anarchy and Computation of Approximate Equilibria
Group: Formal Analysis, Theory and Algorithms (FATA)
Speaker: Yiannis Giannakopoulos, Department of Mathematics, TU Munich
Date: 12 February, 2019
Time: 13:00 - 14:00
Location: Sir Alwyn Williams Building, 422 Seminar Room
The central theme in this talk is the study of the behaviour of autonomous agents in congestion games; important special cases of such games include traffic routing in networks and scheduling.
We give exponential lower bounds on the Price of Stability (PoS) of weighted congestion games with polynomial cost functions. In particular, for any positive integer d we construct rather simple games with cost functions of degree at most d which have a PoS of at least \Omega(\Phi_d)^{d+1}, where \Phi_d is the unique positive root of equation x^{d+1}=(x+1)^d. This essentially closes the huge gap between \Theta(d) and \Phi_d^{d+1} and asymptotically matches the Price of Anarchy (PoA) upper bound. We further show that the PoS remains exponential even for singleton games and approximate equilibria. All our lower bounds extend to network congestion games, and hold for mixed and correlated equilibria as well. On the positive side, we give a general upper bound on the PoS of \rho-approximate Nash equilibria, which is sensitive to the range W of the player weights and the approximation parameter \rho. We do this by explicitly constructing a novel approximate potential function, based on Faulhaber's formula, that generalizes Rosenthal's potential in a continuous, analytic way.
Furthermore, we will briefly discuss how this new potential can be used to derive a polynomial-time deterministic algorithm for computing d^{d+o(d)}-approximate equilibria. This is an exponential improvement of the approximation factor with respect to the previously best algorithm. An appealing additional feature of our algorithm is that it uses only best-improvement steps in the actual game, as opposed to earlier approaches that first had to transform the game itself. A critical component of the analysis of the algorithm, which is of independent interest, is the derivation of a new bound for PoA of \rho-approximate equilibria. More specifically, we show that this PoA is *exactly* equal to \Phi_{d,\rho}^{d+1}, where \Phi_{d,\rho} is the unique positive solution of the equation \rho (x+1)^d=x^{d+1}.
This talk is based on joint work with
(1) George Christodoulou, Martin Gairing and Paul Spirakis (Liverpool)
(2) Georgy Noarov (Princeton) and Andreas S. Schulz (TU Munich)
and the actual papers can be found at the following links:
(1) https://arxiv.org/abs/1802.09952
(2) https://arxiv.org/abs/1810.12806
Past events
Paths between colourings of sparse graphs(12 December, 2018)
Speaker: Carl Feghali
The reconfiguration graph R_k(G) of the k-colourings of a graph G has as vertex set the k-colourings of G and two vertices of R_k(G) are joined by an edge if the corresponding colourings differ on the colour of exactly one vertex. Given a k-degenerate graph G, a conjecture of Cereceda from 2008 states that R_{k+2}(G) has diameter O(|V(G)|^2). I will give a short proof of an existing theorem that addresses the conjecture for graphs with bounded maximum average degree. I will also discuss some progress on the conjecture for planar graphs.
Super-stability in the Student-Project Allocation Problem with Ties(04 December, 2018)
Speaker: Sofiat Olaosebikan
In this presentation, I will talk about the Student-Project Allocation problem where students have preferences over projects, lecturers have preferences over students, and preferences may involve ties (SPA-ST). I will briefly introduce the concept of a blocking pair in this context, and the various definitions of stability that arise. The most robust type of stable matching in this context is super-stability. Thus, I will describe our polynomial-time algorithm to find a super-stable matching or report that no such matching exists, given an instance of SPA-ST. Finally, I will present results obtained from an empirical evaluation of the polynomial-time algorithm based on randomly-generated SPA-ST instances. Our main finding based on this experiment is that, whilst super-stable matchings can be elusive, the probability of such a matching existing is significantly higher if ties are restricted to the lecturers' preference lists.
An improved algorithm for a class of linear programming problems(20 November, 2018)
Speaker: Paul Cockshott
In the period from the late 1930s to the mid 1950s the Russian mathematician Kantorovich developed what came to be known in the West as Linear Programming. Slightly later a similar algorithm, the Simplex one, was independently developed Danzig.
Whilst Danzig’s version is well known in the west, implementations of Kantorovich’s own version are not available.
In this talk I will first describe an implementation I have made of Kantorovich’s original algorithm generalised to handle one year economic plans driven by input output tables. The latter were developed by another Russian theorist Leontief, and have now become a standard tool of economic analysis.
I will then go on to show how the open source LP-solve package can be used, with an appropriate pre-processor, to construct multi-year national economic plans.
I will describe work by one of my former PhD students who showed that the information content of IO tables grows as NLog N and, using simulated economies with this complexity rule, demonstrate that the national planning problem with LP-solve is polynomial of order N^3.
Finally I will describe an algorithm I have developed, that falls into the general class of interior point optimisers, that has very much lower complexity < N^2 demonstrate how much faster even a single threaded Java implementation of this is when compared to the optimised LP-solve version.
COMPUMATCH drop-in session(16 November, 2018)
Speaker: COMPUMATCH
All members of the university interested in forming research collaborations with colleagues in theoretical computer science are warmly invited to come and discuss their research problems. A light buffet lunch will be provided.
Testing logically defined properties on graphs of bounded degree(13 November, 2018)
Speaker: Isolde Adler
Property testing (for a property P) asks for a given graph, whether it has property P, or is "far" from having that property. A "testing algorithm" is a probabilistic algorithm that answers this question with high probability correctly, by only looking at small parts of the input. Testing algorithms are thought of as "extremely efficient", making them relevant in the context of large data sets.
We show that in the bounded degree model, every property definable in monadic second-order logic is testable with a constant number of queries in polylogarithmic running time on graphs of bounded tree-width.
Work in progress solving equations over free groups(06 November, 2018)
Speaker: Markus Pfeiffer
I will discuss some work in progress using constraint solving techniques to the solve equations over free groups.
Population structure and evolution: a survey of the graph Moran process(23 October, 2018)
Speaker: John Lapinskas
When a new mutation is introduced into a population of organisms, it will either die out completely (extinction) or become prevalent (genetic fixation). The driving force behind evolution is that a mutation which confers a small advantage is quite likely to fixate, even in a very large population, whereas a mutation which confers a small disadvantage is exponentially unlikely to fixate. In 2004, Lieberman, Hauert and Nowak proposed the graph Moran process to examine the effects of population structure. Individuals are modelled as vertices on a graph, and only adjacent individuals can interact with each other. In this talk, I will survey a number a recent advances in our understanding of the model, including an almost-tight upper bound on expected absorption time and an answer to the question: can graph structure suppress evolution almost entirely, so that beneficial, neutral or harmful mutations all fixate with roughly the same probability? (Spoiler: It depends!)
The talk is intended to be as accessible as possible for people in different fields - it will assume only elementary graph theory and discrete probability, and no biology whatsoever.
Nondeterministic Bigraphs and Their Use in Modelling Movement(16 October, 2018)
Speaker: Paulius Dilkas
COMPUMATCH launch session(12 October, 2018)
Speaker: COMPUMATCH
The first drop-in session for the newly launched COMPUMATCH scheme. All members of the university interested in forming research collaborations with colleagues in theoretical computer science are warmly invited to come and discuss their research problems. A light buffet lunch will be provided.
FATA Intro 2: Constraint Programming and Model Checking(09 October, 2018)
Speaker: Ciaran McCreesh & Gethin Norman
Ciaran and Gethin will give us short introductions on two core research topics of the FATA Research Section: Constraint Programming and Model Checking.
FATA Intro 1: Programming Languages & Algorithms(02 October, 2018)
Speaker: Kitty Meeks & Ornela Dardha
Kitty and Ornela will give us short introductions on two core research topics of the FATA Research Section: Algorithms and Programming Languages.
Multi-objective mixed integer programming: An exact algorithm(04 September, 2018)
Speaker: William Pettersson
Many heuristic or approximate methods have been used to find all non-dominated objective vectors to a multi-objective mixed integer program (MOMIP), but no generic exact algorithms yet exist. The first exact algorithm for the bi-objective case was only given in 2016. We present here an exact MOMIP algorithm that generalises to an arbitrary number of objective functions, the first such algorithm. Working with an arbitrary number of objective functions, say k, is particularly difficult as the set of non-dominated objective vectors consists of not necessarily convex polytopes of arbitrary dimension (up to k). Our new algorithm consists of three phases: (1) a collection phase, in which the algorithm finds all polytopes which contain some part of the solution, (2) a convexity phase, which takes all such polytopes and creates a set of non-intersecting convex polytopes which cover the same set, and (3) a dominance phase, which then compares such polytopes to determine where (in the objective space) some polytopes may be either partially or totally dominated.
These three phases are presented so as to encourage further work to improve the performance of the algorithm, and a Python implementation currently in use for computational experiments will soon be made available for use by other researchers.
Efficient assignments in generalized roommates problems/On the no-show paradox in quota methods of apportionment(24 August, 2018)
Speaker: Tamás Fleiner and Katarína Cechlárová
On the no-show paradox in quota methods of apportionment - Katarína Cechlárová
The no-show paradox is a disturbing property of some apportionment methods: all parties receive the same number of votes, except for one party that achieves more votes than before and yet this party gets less parliamentary seats.To determine the number of seats in a parliament after elections, two main classes of methods are used: the divisor methods and the quota methods. It is known that the divisor methods are monotone and so do not suffer from the no-show paradox either. We formulate a condition that eliminates the no-show paradox from a quota method and for other quota methods quantify the occurrence of this paradox.
Efficient assignments in generalized roommates problems - Tamás Fleiner
We consider Pareto-efficient assignments of players with preferences on each other to rooms. In his interesting result, Morrill demonstrates how can one borrow ideas from Edmonds' algorithm to find a pareto-improvement of a given assignment in case of twin rooms and strict preferences. In this talk, we consider generalizations where rooms may accommodate more than two agents and preferences might not be strict. It turns out that some of these extensions are not tractable while for certain other ones there is a polynomial time algorithm. The key to some of the presented results is a connection between Pareto-efficient assignments and maximum-weight matchings in graphs. Some of the results are joint with Petra Harján.
AI-augmented algorithms -- how I learned to stop worrying and love choice(23 July, 2018)
Speaker: Lars Kotthoff
Often, there is more than one way to solve a problem. It could be a different
parameter setting, a different piece of software, or an entirely different
approach. Choosing the best way is usually a difficult task, even for experts.
AI and machine learning allow to leverage performance differences of
algorithms (for a wide definition of "algorithm") on different problems and
choose the best algorithm for a given problem automatically. In AI itself,
these techniques have redefined the state of the art in several areas and led
to innovative approaches to solving challenging problems.
In this talk, I will give examples of how AI can help to solve challenging
computational problems, what techniques have been applied, and how you can do
the same. I will argue that AI has fundamental implications for software
development, engineering, and computer science in general -- stop making
decisions when coding, having more algorithmic choices is better!
Normalisers in permutation groups as automorphisms of linear codes(05 June, 2018)
Speaker: Mun See Chang
At the present time, there is no known general polynomial time algorithm for finding the normaliser N_G(H) of subgroup H in a finite permutation group G. The best solution so far is to use backtrack search to look for the normalising elements. However, the current algorithm does not perform well in certain kinds of groups. This includes the groups that have all orbits of size at most 2. By considering the problem as computing automorphisms of linear codes, the performance of the algorithm has been greatly improved. In this talk I will demonstrate some tests used in this algorithm to reduce the search size.
On the Enumeration of Minimal Hitting Sets in Lexicographical Order(30 May, 2018)
Speaker: Martin Schirneck
It is a long-standing open problem whether there exists an output-polynomial algorithm enumerating all minimal hitting sets of a hypergraph. A stronger requirement is to ask for an algorithm that outputs them in lexicographical order. There is no incremental-polynomial algorithm for this task in general, unless P = NP. However, we present a method with delay O(|H|^(k*+2) |V|^2), where k* is the rank of the transversal hypergraph. On classes of hypergraphs for which k* is bounded the delay is polynomial. Additionally, we identify the extension problem of minimal hitting sets as one of only a few natural problems being complete for the parameterized class W[3]. We give an algorithm that is optimal under ETH.
A polynomial-time approximation algorithm for all-terminal network reliability(22 May, 2018)
Speaker: Heng Guo
All-terminal network reliability is the probability that, in a undirected graph, assuming each edge fails independently, the remaining graph is still connected. We will present a fully polynomial-time randomised approximation scheme (FPRAS) for this problem. Our main contribution is to confirm a conjecture by Gorodezky and Pak (Random Struct. Algorithms, 2014), that the expected running time of the "cluster-popping" algorithm in bi-directed graphs is bounded by a polynomial in the size of the input.
Joint work with Mark Jerrum (QMUL).
Applying Formal Methods in Healthcare(15 May, 2018)
Speaker: Juliana Bowles
Abstract:
This talk shows different logic-based approaches to detect and resolve conflicts in the treatment of multiple chronic conditions, and model and compare treatment options for chronic conditions.
We developed an automated approach focusing on the composition of (static or behavioural) design models via constraint solvers. This approach is directly applicable to many different domains, and can be used for the detection of conflicts in clinical pathways. Clinical pathways are care plans which detail essential steps in the care of patients with a specific clinical problem, usually a chronic disease. A pathway includes recommendations of medications prescribed at different stages of the care plan. For patients with three or more chronic diseases (known as multimorbidities) the multiple pathways have to be applied together. One common problem for such patients is the possible adverse interaction between medications given for different diseases. In this context, we have used an optimising SMT solver (Z3) to quickly find the set of medications with the minimal number and severity of conflicts which is assumed to be the safest. In our approach we can vary the measures of interest to obtain different outcomes and generate the best
option, second best, etc. We use a combination of SMT solvers and theorem provers for checking correctness.
Conversely, automata can be used to capture the stages and treatment options for a chronic disease, where traces in the model highlight different treatments plans that patients can follow. Adding further information to such models allow us to explore extensions and combinations of different variants of timed automata and associated tools in different ways. We can combine patient information and comorbidities with the disease automaton through composition. We have explored the use of model checking as an analysis technique to provide further insights into the effectiveness/completeness of treatment plans for a given patient.
Bio:
Juliana Bowles (née Küster-Filipe) is a senior lecturer at the School of Computer Science, University of St Andrews, Scotland. She has research interests in formal methods and dependability, logics and models for true-concurrency, and foundations of modelling languages. She is currently applying her foundational work to the healthcare domain, and
has an EPSRC-funded project on "Automated Conflict Resolution in Clinical Pathways".
Bowles received her PhD (Dr.rer.nat) from the Technical University of Braunschweig, Germany, in 2000.
The language of stratified sets, Quine's NF, rewriting, and higher-order logic(08 May, 2018)
Speaker: Murdoch Gabbay
http://www.gabbay.org.uk/papers.html#lanssc
The language of Stratified Sets is confluent and strongly normalising
Graph Colouring for Special Graph Classes(01 May, 2018)
Speaker: Daniel Paulusma
Joint work with Serge Gaspers and Shenwei Huang
The Colouring problem is to decide if the vertices of a graph can be coloured with at most k colours for a given integer k, such that no two adjacent vertices are coloured alike. The complexity of Colouring is fully understood for graph classes characterized by one forbidden induced subgraph H, but there are still major complexity gaps if the number of colours k is fixed or if two induced subgraphs H_1 and H_2 are forbidden. We survey known results in both directions and discuss a number of new results for the second direction. Let H_1 be the s-vertex cycle C_s and H_2 be the t-vertex path P_t. We consider the complexity of Colouring for (C_s,P_t)-free graphs. In particular we show that Colouring is polynomial-time solvable for (C_4,P_6)-free graphs and NP-complete for (C_4,P_9)-free graphs. In our talk we focus on the graph colouring techniques behind the polynomial-time result (which have a wider applicability).
Level 5 Student Presentations(19 April, 2018)
Speaker: Duncan Adamson and Duncan Milne
There will be two 25-minute talks from current Level 5 students on their MSci research projects. Details are as follows:
Maximum least-unstable matchings using Integer Programming
Duncan Adamson
In the stable marriage problem with incomplete lists we have a set of men and women who each express preference over each other. Much work for this problem has been concerned with finding a stable matching, however in many cases we would rather find a matching including the maximum number of agents. In this case we want to find a matching of maximum cardinality that is the "least-unstable", either having as few blocking pairs or blocking agents as possible for a matching of that cardinality, unfortunately the problem of finding such a matching is NP-Hard. In this talk we will present our IP model for finding solutions to this problem, as well as our theoretical results for this problem. We will also present empirical results based on random instances of this problem evaluated with our IP model.
Mouse Maze with Integer and Constraint Programming techniques
Duncan Milne
Mouse Maze is a game about a mouse named Squeaky who is attempting to escape an n by n grid containing obstacles placed by users, where n is any integer greater than 2. The goal of Mouse Maze is to find a maze that confounds Squeaky for as long as possible. Squeaky follows a deterministic rule which has been proven to always lead him to escape from the maze, meaning an upper bound on the number of turns Squeaky can be confounded for must exist. Finding optimal mazes on larger grids is challenging because of the enormous number of possible obstacle configurations users can create. This talk discusses the viability of integer programming and constraint programming approaches to this problem. Brute force techniques are also discussed and compared to the integer and constraint programming approaches.
Level 5 Student Presentations(18 April, 2018)
Speaker: David Frohlingsdorf and Gary Curran
There will be two 25-minute talks from current Level 5 students on their MSci research projects. Details are as follows:
The Capacitated Vehicle Routing Problem with Time Windows
David Frohlingsdorf
The Capacitated Vehicle Routing Problem with Time Windows is a very important logistic problem because our economy is becoming increasingly globally connected in particular in the wake and rise of online trading. Nowadays customers can order goods at any time from anywhere in the world and the order must be delivered to the customer within days. This trend puts significant strains on supply chains. Logistic businesses need to keep transportation costs low in order to stay competitive. Businesses use computer models and programs to effectively route their delivery vehicles to customers. Various approaches have been proposed and used to solve this problem. Our work focuses on Constraint Programming models because of their high flexibility and readability. Constraint Programming models can be adapted and changed with relative ease on a day to day basis allowing businesses to react quickly to exceptional circumstances.
SAT Encodings of Stable Matching Problems
Gary Curran
The Hospitals / Residents problem involves a set of junior doctors and a set of hospitals with each junior doctor expressing preference over the hospitals they can be assigned to and, likewise, each hospital expresses preference over the junior doctors. When considering this problem, one often seeks a stable matching, meaning that there is no incentive for a pair not in the matching to break away from the given assignment. If preference lists are allowed to express indifference between agents, stable matchings can have different sizes and the task of finding the maximum weakly stable matching is NP-hard. This talk will describe a SAT encoding to find the maximum weakly stable matching of the Hospitals / Residents problem where ties are allowed, and the results given from empirical evaluation on randomly generated instances will be presented.
Leveraging Formal Methods for addressing challenges in building Wireless Sensor Networks(17 April, 2018)
Speaker: Milan Kabáč
This talk provides an overview of diverse challenges designers of sensor systems have to face in terms of energy availability and harsh environmental conditions, etc. to prevent potentially harmful consequences on the WSN. We argue that the application of formal modelling and verification techniques to the domain of WSN can improve the design of these systems, identify issues at runtime and provide means to predict potentially harmful situations in the near future. To this end we present an approach based on a formalism called Bigraphs that provides both a straightforward graphical representation of the system and a computational model that integrates with established techniques in formal methods. The approach leverages various formal logics dedicated to the verification of WSN. We demonstrate how our approach can be used to address the identified challenges and highlight opportunities for applying Formal Methods to the domain of WSN.
Concurrent Semantics of Controlled Graph Rewriting(26 March, 2018)
Speaker: Géza Kulcsar
Graph transformation systems (GTS) are often defined as sets of rules that can be applied repeatedly and non-deterministically to model the evolution of a system. Several semantics proposed for GTSs are relevant in this case, providing means for analysing the system's behaviour in terms of dependencies, conflicts and potential parallelism among the relevant events.
Compositional Verification of Self-Adaptive Cyber-Physical Systems(20 March, 2018)
Speaker: Liliana Pasquale
Cyber-Physical Systems (CPS) must often self-adapt to respond to changes in their operating environment. However, scale of CPS makes it computationally intractable to use traditional formal techniques to verify how they can self-adapt. This talk proposes a modelling language to represent self-adaptive CPS that supports compositionality. Using topological relationships of CPS, such as containment and connectivity, the language allows decomposing CPS into loosely coupled components. These can affect satisfaction of certain system requirements and may be therefore responsible to self-adapt in order to satisfy these requirements. The proposed language allows a system designer to explore and verify alternative self-adaptive behaviours enacted by different CPS components at different granularities. These self-adaptive behaviours can be formally verified independently from the rest of the system, thus enabling computationally tractable verification. The modelling language combines the concurrency abstractions of Communicating Sequential Processes (CSP) with specialised contracts that can express locality and self-adaptation. Properties of interest are proved formally using FDR. The feasibility of the approach is demonstrated using an example of a smart art gallery.
Applying Formal Methods in Healthcare(15 March, 2018)
Speaker: Juliana Bowles
Abstract:
This talk shows different logic-based approaches to detect and resolve conflicts in the treatment of multiple chronic conditions, and model and compare treatment options for chronic conditions.
We developed an automated approach focusing on the composition of (static or behavioural) design models via constraint solvers. This approach is directly applicable to many different domains, and can be used for the detection of conflicts in clinical pathways. Clinical pathways are care plans which detail essential steps in the care of patients with a specific clinical problem, usually a chronic disease. A pathway includes recommendations of medications prescribed at different stages of the care plan. For patients with three or more chronic diseases (known as multimorbidities) the multiple pathways have to be applied together. One common problem for such patients is the possible adverse interaction between medications given for different diseases. In this context, we have used an optimising SMT solver (Z3) to quickly find the set of medications with the minimal number and severity of conflicts which is assumed to be the safest. In our approach we can vary the measures of interest to obtain different outcomes and generate the best option, second best, etc. We use a combination of SMT solvers and theorem provers for checking correctness. Conversely, automata can be used to capture the stages and treatment options for a chronic disease, where traces in the model highlight different treatments plans that patients can follow. Adding further information to such models allow us to explore extensions and combinations of different variants of timed automata and associated tools in different ways. We can combine patient information and comorbidities with the disease automaton through composition. We have explored the use of model checking as an analysis technique to provide further insights into the effectiveness/completeness of treatment plans for a given patient.
Bio:
Juliana Bowles (née Küster-Filipe) is a senior lecturer at the School of Computer Science, University of St Andrews, Scotland. She has research interests in formal methods and dependability, logics and models for true-concurrency, and foundations of modelling languages. She is currently applying her foundational work to the healthcare domain, and has an EPSRC-funded project on "Automated Conflict Resolution in Clinical Pathways".
Bowles received her PhD (Dr.rer.nat) from the Technical University of Braunschweig, Germany, in 2000.
Student-Project Allocation(06 March, 2018)
Speaker: Sofiat Olaosebikan and Frances Cooper
Frances:
In universities all over the world, students must be assigned to dissertation projects as part of their degree programmes. In many cases students are required to rank a subset of the available projects in order of preference, and likewise, lecturers rank in order of preference those students who have applied for their projects. A centralised allocation is then conducted which gives a matching of students to projects. A key consideration is that the matching should be stable, which ensures that no student and lecturer who are not matched together have an incentive to form an assignment with one another after the matching has been announced. In this talk we consider the case where preference lists need not be strictly ordered, and may contain ties. In this scenario stable matchings can be of different sizes and it is known that the problem of finding a maximum-sized stable matching is NP-hard. We present an approximation algorithm for this problem that has a performance guarantee of 3/2.
Sofiat:
The Student-Project Allocation problem with preferences over Projects (SPA-P) involves sets of students, projects and lecturers, where the students and lecturers each have preferences over the projects. In this context, we typically seek a stable matching of students to projects (and lecturers). However, these stable matchings can have different sizes, and the problem of finding a maximum stable matching (MAX-SPA-P) is NP-hard. There are two known approximation algorithms for MAX-SPA-P, with performance guarantees of 2 and 3/2. In this talk, I’ll describe an IP formulation to enable MAX-SPA-P to be solved optimally. Finally, I’ll present results arising from an empirical analysis that compares the approximation algorithms and the IP formulation, with respect to the size of the stable matchings constructed, on instances that are both randomly-generated and derived from real datasets.
Subgraph Isomorphism in Practice(20 February, 2018)
Speaker: Ciaran McCreesh
The subgraph isomorphism problem is to find a little "pattern" graph inside a larger "target" graph. Despite being NP-complete, practical algorithms can often solve instances with graphs involving many thousands of vertices. I'll give an overview of the state of the art in subgraph isomorphism solving, with a particular focus on search strategies. I'll then explain some recent work we've carried out on moving away from simple backtracking search and on introducing small amounts of randomness. This can be hugely beneficial for satisfiable instances, and thanks to the "two watched literals" scheme (which is the awesomest data structure in all of computer science), we can even make this change without affecting performance on unsatisfiable instances. Finally, I'll talk about how we verify empirically that these techniques actually give an improvement, since they have no effect on worst-case theoretical complexity.
Modelling of spatial stochastic systems and analysis of their spatio-temporal properties (13 February, 2018)
Speaker: Ludovica Luisa Vissat
In my talk I will give an overview of my PhD research work. We have initially developed a novel process algebra, specifically tailored for modelling ecological systems, and more generally for spatial stochastic systems. These systems can be seen as a collection of agents that can interact and are spatially located. To analyse properties of the dynamics of these stochastic systems, we worked with spatio-temporal logics and statistical model checking. We introduced the novel Three-Valued Spatio-Temporal Logic (TSTL), which extends the available analysis, looking at the spatio-temporal evolution of the satisfaction probabilities of given logical formulas, estimated through statistical model checking. We have also defined an automatic procedure that verifies if TSTL results are given with sufficient precision. I will present different case studies during the talk, to show various applications of our modelling language and spatio-temporal analysis.
Parameterised complexity in 3-manifold topology(30 January, 2018)
Speaker: William Pettersson
A topologist is, according to the joke, a mathematician who does not see the difference between a coffee cup and a donut. Aside from as a conversation starter, topology is also useful in molecular biology (protein folding), astronomy (coronal loops and the shape of the universe), physics (group field theories and string theory) and also has applications in further fields of mathematics such as geometric group theory, algebra and knot theory.
In this talk I will give some background into the world of combinatorial topology, and also detail how topologists came to eventually use parameterised complexity to help solve some of their problems.
Performance Portable Parallel Code Generation with Lift(23 January, 2018)
Speaker: Michel Steuwer
The Lift project aims at generating high-performance code for parallel processors from portable high-level programs. Starting from a single high-level program an optimisation process based on formal rewrite rules transforms the portable program into highly-specialised low-level code delivering high-performance.
Algorithms for Maximum Common Subgraph(16 January, 2018)
Speaker: James Trimble and Paulius Dilkas
This talk has two parts.
In the first part, James will introduce ``McSplit'', a branch and bound algorithm for the maximum common subgraph and maximum common connected subgraph problems. Our method in some ways resembles a traditional constraint programming approach, but uses a novel compact domain store and supporting inference algorithms which dramatically reduce the memory and computation requirements during search.
In the second part, Paulius will introduce algorithm selection for maximum common subgraph, using machine learning to choose between the McSplit, McSplit-down, k-down, and clique algorithms on an instance-by-instance basis. He will present new results showing how the performance changes depending on the number of labels that appear on vertices and edges.
Probabilistic model checking for UAV controller generation(05 December, 2017)
Speaker: Alice Miller
I will describe how the PRISM model checker was used to generate controllers for an Unmanned Ariel Vehicle (UAV), specifically to determine search strategies for a UAV trying to find objects within a grid, for a range of scenarios. Parameters and probabilities for our models were informed by simulation models developed in the School of Engineering's Micro Air Systems Technologies (MAST) Laboratory. Our generated controllers can now be used within the simulation models (and ultimately in UAV software).
This is joint work with colleagues from the School of Computing Science (Gethin Norman, Ruth Hoffmann and Ruben Giaquinta) and the School of Engineering (Murray Ireland).
Objects as communicating automata(21 November, 2017)
Speaker: Roly Perera
Abstract:
Behind the interfaces of most objects lurk state machines, constraining the services they offer and consume at various points in their lifecycles. Many familiar program errors result from using objects at one point in their lifecycle as if they were at another. I will describe ongoing work, inspired by session types, which models objects as communicating automata, making their states and transitions explicit.
Joint work with Julian Lange, J. Garrett Morris and Simon J. Gay.
Formal models for target counting(14 November, 2017)
Speaker: Michele Sevegnani
The target counting problem is the computational task of estimating the total number of observable targets within a region using local counts performed by a set of networked sensors capable of counting but not identifying targets within their sensing range. The complexity of this problem lies in the fact that multiple sensors may be observing the same target if it is located within the intersection of their overlapping sensing ranges. This may lead to wrong estimates as duplicate observations, together with the inability to distinguish different targets, introduce over-counting. In this talk, I will present models based on bigraphs of two different algorithms that have been developed to mitigate this issue. This is ongoing work in collaboration with Sven Linker at the University of Liverpool.
An introduction to the Constraint Modelling language MiniZinc(07 November, 2017)
Speaker: Patrick Prosser
MiniZinc is a free open-source constraint modelling language and is all the rage with the young, thrusting Constraint Programmer. I'll give an introductory talk and demo of MiniZinc, solving two problems: the (now famous) Crystal Maze and the (fantastic ) Abarth 595 paint shop! Be there ... or be somewhere else.
Data-driven, probabilistic models for software usage(24 October, 2017)
Speaker: Muffy Calder
In the Populations project, we have been interested in how people actually use interactive software applications (apps), so that we might redesign that app, or design future apps, to better support styles of use. We had access to the user logs of instrumented apps, for tens of thousands of users, over several years. A key question for Oana and I has been how to derive models from those user traces, which would allow us to hypothesise about and analyse user styles. In previous talks, we have focussed on our use of temporal logics for expressing hypotheses and doing the analysis. In this short, informal talk I will focus solely on the question “which models”? We found there were no suitable, established models -- so we had to define our own. I will outline three different probabilistic, Markovian, admixture models, and the different kinds of questions (hypotheses) we can ask of each one.
FATA Intro 1: Programming Languages & Algorithms(10 October, 2017)
Speaker: Simon Gay & David Manlove
Simon and David will give us short introductions on two core research topics of the FATA Research Section: Programming Languages and Algorithms.
FATA Seminar - A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming(30 May, 2017)
Speaker: Ornela Dardha
Multiparty Session Types (MPST) is a typing discipline for message-passing distributed processes that can ensure properties such as absence of communication errors and deadlocks, and protocol conformance. Can MPST provide a theoretical foundation for concurrent and distributed programming in “mainstream” languages? We address this problem by (1) developing the first encoding of a full-fledged multiparty session pi-calculus into linear pi-calculus, and (2) using the encoding as the foundation of a practical toolchain for safe multiparty programming in Scala.
Our encoding is type-preserving and operationally sound and complete. Crucially, it keeps the distributed choreographic nature of MPST, illuminating that the safety properties of multiparty sessions can be precisely represented with a decomposition into binary linear channels. Previous works have only studied the relation between (limited) multiparty and binary sessions via centralised orchestration means. We exploit these results to implement an automated generation of Scala APIs for multiparty sessions, abstracting existing libraries for binary communication channels. This allows multiparty systems to be safely implemented over binary message transports, as commonly found in practice. Our implementation is the first to support distributed multiparty delegation: our encoding yields it for free, via existing mechanisms for binary delegation.
SICSA sponsored seminar: Scottish Theorem Proving(19 May, 2017)
Speaker: SICSA Event
Everyone with an interest in theorem proving and related forms of formal verification is warmly invited to the Scottish Theorem Proving seminar at the School of Computing Science, University of Glasgow. This year we celebrate 20 years of Scottish Theorem Proving seminars (over 40 events). Therefore it is a great opportunity for the School of Computing Science to host the first seminar of 2017 to join the on-going celebration of the 60th anniversary of Computing in Glasgow.
Theorem proving research is notably strong in Scottish universities, with active groups and researchers in at least six departments. The Scottish Theorem Proving Seminar series provide a common venue for communication and sharing of ideas by all these researchers. At least once a year, one of the departments hosts an informal seminar for the whole Scottish theorem proving community. As well as theorem proving, other related fields are also represented, e.g. model checking and other forms of formal verification. This is a friendly venue for PhD students and RAs to discuss their work in progress and get feedback.
Registration: Attendance is free, but participants are asked to register by 18th of May on Eventbrite. Lunch, tea, coffee and celebratory cake will be provided.
Programme:
- 13:15 - 14:00 Lunch
- 14:00 - 14:40 Tom Melham (University of Oxford), Effective Validation of Low-Level Firmware — (invited talk)
- 14:40 - 15:20 Yue Li (Heriot-Watt University), Productive Corecursion in Logic Programming
- 15:20 - 15:40 Coffee break
- 15:40 - 16:20 Chris Warburton (University of Dundee), Quantitative Benchmarks for Theory Exploration
- 16:20 - 17:00 Oana Andrei (University of Glasgow), Machine Learning and Probabilistic Model Checking for Interactive Systems
Chairs: Oana Andrei and Alice Miller
More details can be found at: http://www.dcs.gla.ac.uk/~oandrei/STP17/
FATA Seminar - Student talks(18 April, 2017)
Speaker: Alexandra Stan, Iva Babukova, Kyle Simpson
The second hour will take place in room F121
FATA Seminar - Hyper-Verification: Challenges from Cyber-Physical Systems(04 April, 2017)
Speaker: Luminita Manuela Bujorianu
Abstract: Cyber-physical systems represent an evolving paradigm promoting a holistic view on engineered systems. The holistic view makes the formal verification look like a restrictive or specialised approach. In this way, a research challenge appears: How to leverage formal verification to cope with the holistic character of cyber-physical systems?
The holistic aspects include: emergent behaviours, complex faults (like hybrid discrete continuous), severe uncertainty, rich interactions, interdependence of critical components, potential disasters due to climate change.
In this talk, we will discuss about hyper-verification of cyber-physical systems and sketch the fundamentals of a suitable formal framework to investigate it.
Bio: Manuela L Bujorianu (PhD in computer science, BSc in Mathematics) is a Research Fellow with Maritime Safety Research Centre, Department of Naval Architecture, Ocean and Marine Engineering, University of Strathclyde. Before she was affiliated with several universities: Leicester, Warwick, Manchester, Twente, Cambridge and Stirling.
Manuela’s research is at the border between computer science, applied mathematics, and systems engineering bridged by probability theory and statistics. The major focus is on modelling and analysis of complex systems. The considered application areas are: cyber-physical systems (maritime safety, air traffic management, intelligent transportation systems), complex systems (financial /social systems, swarms, complex networks), probabilistic risk assessment, resilience of critical infrastructures. A unique feature of Manuela publication record is that she published at the top conferences and journals in control engineering, computer science, and mathematics. She has single authored a monograph at Springer Verlag.
FATA Seminar - Specifying Protocol Message Formats(21 March, 2017)
Speaker: Florian Weber
The protocol description language Scribble, based on session types, is used as the input format for several tools that generate code to support the correct implementation of protocol roles. Scribble describes messages abstractly independently of their underlying transport mechanism. This means that working with legacy protocols and their existing textual message formats requires parsing and formatting code to bridge the gap between abstract Scribble messages and concrete protocol messages. We introduce a small language for defining the mapping between abstract and concrete messages. We also describe a tool that automatically generates the corresponding parsers and formatters from this language. This tool has been integrated with an existing Scribble to Java transpiler. We show that the combination of Scribble and a message mapping specification is an effective way of formally specifying internet protocols, by describing implementations of clients for POP3, SMTP and IMAP.
FATA Seminar - Behavioural types to make object-oriented programs go right(28 February, 2017)
Speaker: António Ravara
Abstract: Stateful objects typically have a non-uniform behaviour, as the availability of their methods depend on their internal state. For instance, in an object that implements file access the method to read a file should not be invoked before calling the method to open that file. Similarly, in an iterator object, calls to the next method should be preceded by calls to the hasNext method.
Behavioural types are particularly well-suited to object-oriented programming, as they make it possible to statically guarantee that method calls happen when an object has an internal state that is safe for the method's execution. Following the typestates approach, one may declare for each possible state of the object the set of methods that can be safely executed in that state.
Several languages already associate with a class a dynamic description of objects' behaviour declaring the admissible sequences of method calls. These descriptions, herein called usages, can be used to ensure at compile time that, in a given program, all the sequences of method calls to each object follow the order declared by its usage. To ensure usages to be followed, objects are linear to prevent interferences unexpectedly changing their state.
However, the typing systems referred to above have two shortcomings. First, type checking is typically inefficient, as a method's body is checked each time that method appears in a usage. Second, said typing systems limit themselves to just verifying that method calls follow the usage, and do not necessarily prevent the typed program from ``going wrong'' (e.g., getting stuck or producing a null pointer exception).
Our work addresses these weaknesses:
1) We attain a stronger type-safety result, by including de-referencing a null reference in the definition of errors and by including in type-checking a form of null pointer analysis. Thus, type-safety in our setting means no run-time errors and complete execution of objects' usages.
2) We attain more efficient type-checking by analysing methods' bodies only once. Instead of checking the code following the usage, we introduce client usages, behavioural descriptions of how a methods' code changes the state of objects in fields (and variables/parameters), type the method bodies following that information and check the consistency of the usages independently.
Client usages have another advantage: they can, not only be inferred from the code, but also be used to produce pre- and post-conditions to methods that then allow to infer usages.
We are developing this work in stages. First, we define a type system only with usages and prove type-safety (our enhanced version). Subsequently, we extend the type system with client usages and get a more efficient type-checking. Afterwards we infer the client usages from the code, and finally, we infer pre- and post-conditions from client usages. Our aim is to provide an approach that takes a program in a Java-like language and automatically infers class usages that describe safe orders of method calls, but also type-checks (client) code against usages (either inferred or user-defined) so as to guarantee that the whole program does not go wrong.
Short bio: Assistant Professor at DI FCT UNL PT, on Sabbatical leave during 2016/17 visiting SCS Glasgow.
Main research problem addressed is how to ensure that inherently concurrent, highly distributed, software systems behave correctly. The focus is on the development of techniques, program constructions, and tools that help creating safe and well-behaved systems, provably providing correctness guarantees. The toolbox used includes static analysis of source code, capturing defects before deployment, with decidable, low complexity, property-driven, proof systems, using behavioural descriptions of programs.
FATA Seminar - Discovery and recognition of emerging activities via directional statistical models and active learning(21 February, 2017)
Speaker: Lei Fang
Abstract:
Human activity recognition plays a significant role in enabling pervasive applications as it abstracts low-level noisy sensor data into high-level human activities, which applications can respond to. In this paper, we identify a new research question in activity recognition -- discovering and learning unknown activities that have not been pre-defined or observed. As pervasive systems intend to be deployed in a real-world environment for a long period of time, it is infeasible, to expect users will only perform a set of pre-defined activities. Users might perform the same activities in a different manner, or perform a new type of activity. Failing to detect or update the activity model to incorporate new patterns or activities will outdate the model and result in unsatisfactory service delivery. To address this question, we propose a solution to not only discover and learn new activities over time, but also support incremental updating the activity model by employing directional statistical model (hierarchical mixtures of von Mises-Fisher Distributions) and active learning strategies.
Short bio:
Lei Fang is a Research Fellow at the School of Computer Science, University of St Andrews. His research interests include sensor networks, sensor data processing, statistical modelling, human activity recognition, etc. Currently, he is a postdoc working on the EPSRC Science of Sensor Systems Software (S4) project. He got his Ph.D. from the University of St Andrews in 2015.
FATA Seminar - The complexity of finding and counting sum-free subsets(07 February, 2017)
Speaker: Kitty Meeks
A set A of natural numbers is said to be sum-free if it does not contain distinct x, y and z such that x + y = z. Sum-free sets have been studied extensively in additive combinatorics (Paul Erdős was particularly interested in these sets) but algorithmic questions relating to sum-free sets have thus far received very little attention. We consider the problem, given a set A, of determining whether A contains a sum-free subset of size at least k. We show that this problem is NP-complete in general, but is tractable with respect to certain parameterizations; in the cases where the decision problem is tractable, we also consider the complexity of counting all sum-free subsets of size exactly k.
This is joint work (in progress) with Andrew Treglown (University of Birmingham).
FATA Seminar - Spatial Reasoning about Traffic Safety(31 January, 2017)
Speaker: Sven Linker
Abstract:
Due to the increasing use of automated car controllers, mathematical correct formalisms are needed to describe these controllers and verify their safety. Typical approaches refer to the dynamical behaviour of cars via differential equations. In this way, spatial aspects of cars, like the current position and the space needed for safe braking in case of emergencies, are only available indirectly. However, for the verification of safety properties, e.g., collision freedom, these properties are of inherent importance.
In this talk, I present an approach with the intention to simplify safety proofs by abstracting away from the concrete dynamics of cars. Within proofs, explicit assumptions about the behaviour of cars have to be used. These assumptions, e.g. that cars are able to calculate their braking distance, can then be instantiated with more detailed approaches.
The contributions of this work are divided into three parts. I present an abstract model of traffic on multi-lane highways which hides the dynamics and only considers a local neighbourhood of each car. Subsequently, I define and briefly explain a modal logic based on this model to specify and verify safety properties of highway traffic.
Finally, I present the application of this logic in form of a case study exploring minimal constraints for controllers ensuring safety on motorways.
Bio:
Sven Linker received his PhD with the topic "Proofs for Traffic Safety - Combining Diagrams and Logic" in 2015 from the Carl von Ossietzky University of Oldenburg, Germany. From 2015 to 2016 he was part of the project "The Readability of Proofs in Diagrammatic Logic" at the University of Brighton, UK. Since 2016, he works at the University of Liverpool in the project "Science of Sensor Systems Software".
His main research areas are the application of logics to verification and specification of computer systems, especially modal logics and their proof systems, as well as formal diagrammatic systems.
FATA Seminar - Hyper-Heuristics with Graph Transformations(17 January, 2017)
Speaker: Christopher Stone
Hyper-Heuristics is a search method for selecting and generating heuristics to solve combinatorial optimisation problems taking advantage of the abundance of heuristics developed to tackle a wide range of problem classes. Unfortunately heuristics, and the solutions they operate on, tend to have their own specific representation both in terms of underlying data structure and in the taxonomy used to describe their approach. This talk will present an approach based on graphs and graph transformations able to model multiple problem classes using the same data structure. This will include a discussion on the trade-offs of this approach and an overview of the latest empirical results.
Bio: Christopher L. Stone received his MEng degree in Software Engineering from Edinburgh Napier University. He is currently a PhD student under the supervision of Emma Hart and Ben Peachter at the same university. His main research interests are related to computational intelligence with a focus on representation of NP-Hard problems (Routing, packing and scheduling), generation of heuristics and graph transformations.
FATA Seminar - Between Subgraph Isomorphism and Maximum Common Subgraph(13 December, 2016)
Speaker: Craig Reilly
When a small pattern graph does not occur inside a larger target graph, we can ask how to find “as much of the pattern as possible” inside the target graph. In general, this is known as the maximum common subgraph problem, which is much more computationally challenging in practice than subgraph isomorphism. We introduce a restricted alternative, where we ask if all but k vertices from the pattern can be found in the target graph. This allows for the development of slightly weakened forms of certain invariants from subgraph isomorphism which are based upon degree and number of paths. We show that when k is small, weakening the invariants still retains much of their effectiveness. We are then able to solve this problem on the standard problem instances used to benchmark subgraph isomorphism algorithms, despite these instances being too large for current maximum common subgraph algorithms to handle. Finally, by iteratively increasing k, we obtain an algorithm which is also competitive for the maximum common subgraph problem.
FATA Seminar - Probabilistic and Stochastic Hybrid Automata and their Abstractions(06 December, 2016)
Speaker: Ruth Hoffman
With the wide applicability of probabilistic and stochastic hybrid systems in the real world, it is now more important than ever to be able to verify these systems for safety and reliability. Hybrid systems can be found anywhere, from thermostats to processes passing messages. We will discuss the different types of hybrid systems and their discrete abstractions. The probabilistic hybrid systems we will be focusing on are autonomous unmanned aerial vehicles. The abstracted structures allow for existing quantitative and model checking tools to verify and analyse the system.
FATA Seminar - More Semantics More Robust: Improving Android Malware Classifiers(29 November, 2016)
Speaker: Wei Chen
Abstract: Automatic malware classifiers often perform badly on the detection of new malware, i.e., their robustness is poor. We study the machine-learning-based mobile malware classifiers and reveal one reason: the input features used by these classifiers can't capture general behavioural patterns of malware instances. We extract the best-performing syntax- based features like permissions and API calls, and some semantics-based features like happen-befores and unwanted behaviours, and train classifiers using popular supervised and semi-supervised learning methods. By comparing their classification performance on industrial datasets collected across several years, we demonstrate that using semantics- based features can dramatically improve robustness of malware classifiers.
Bio: Dr Wei Chen is a Research Associate in School of Informatics at University of Edinburgh. He received his PhD from University of Nottingham on Type Theory supervised by Prof. Roland C. Backhouse. In 2012 Wei worked with Prof. Martin Hofmann on type-based verification in Munich. He started his current RA with Prof. David Aspinall since 2013, focusing on learning policies for mobile security. Wei's main research interests are in formal methods, in particular, type theory, combinatorial games, and Buechi automata with their applications in program analysis and verification. He is currently working on combining formal methods and machine learning to help with mobile security.
FATA Seminar - On parameterized algorithms for polynomial-time solvable problems(22 November, 2016)
Speaker: André Nichterlein
Parameterized complexity analysis is a flourishing field dealing with the exact solvability of "intractable" problems. Appropriately parameterizing polynomial-time solvable problems helps reducing unattractive polynomial running times. In particular, this "FPT in P" approach sheds new light on what makes a problem far from being solvable in linear time, in the same way as classical FPT algorithms help in illuminating what makes an NP-hard problem far from being solvable in polynomial time. Surprisingly, this very interesting research direction has been too little explored so far; the known results are rather scattered and do not systematically refer to or exploit the toolbox of parameterized algorithm design.
In this talk, I will introduce the field of "FPT in P". To this end, I will outline known results, explain some of the corresponding techniques, and highlight similarities and differences to the classical design of parameterized algorithms for NP-hard problems.
FATA Seminar - Max Weight Clique(15 November, 2016)
Speaker: Patrick Prosser
In the maximum clique problem, we are given a simple graph (with vertices and edges), and we are to find a largest set of vertices such that all pairs of vertices in that set are adjacent. In the maximum weight clique problem (mwc), vertices have weight, and we are to find a set of pair-wise adjacent vertices such that the sum of the weights of those vertices is as big as can be. In my talk I will present an exact algorithm for this problem, present some real-world problems (one that is very close to home) that are in fact instances of mwc. I'll review the current state of empirical studies of mwc and suggest future directions of study.
FATA Seminar - Binary session types for psi-calculi(08 November, 2016)
Speaker: Hans Hüttel
The framework of psi-calculi introduced by Bengtson et al. makes it possible to give a general account of variants of the pi-calculus. We use this framework to describe a generic session type system for variants of the pi-calculus. In this generic system, standard properties, including fidelity, hold at the level of the framework and are then guaranteed to hold when the generic system is instantiated.
We show that our system can capture existing systems including the session type system due to Gay and Hole, a type system for progress due to Vieira and Vasconcelos and a refinement type system due to Baltazar et al. The standard fidelity property is proved at the level of the generic system, and automatically hold when the system is instantiated.
FATA Seminar - "Almost stable" matchings in the Hospitals / Residents problem with Couples(01 November, 2016)
Speaker: David Manlove
The Hospitals / Residents problem with Couples (HRC) models the allocation of intending junior doctors to hospitals, where couples are allowed to submit joint preference lists over pairs of (typically geographically close) hospitals. In this context we seek a stable matching of doctors to hospitals, but for some instances, such a matching may not exist. We thus consider MIN BP HRC, the problem of finding a matching that is "as stable as possible" (i.e., admits the minimum number of blocking pairs). We present some new complexity results for this problem - in general it is NP-hard and difficult to approximate. We then present the first Integer Programming (IP) and Constraint Programming (CP) models for MIN BP HRC. Finally, we discuss an empirical evaluation of these models applied to randomly-generated instances of the problem. We find that on average, the CP model is about 1.15 times faster than the IP model, and when presolving is applied to the CP model, it is on average 8.14 times faster. We further observe that the number of blocking pairs admitted by a solution is very small, i.e., usually at most 1, and never more than 2, for the (28,000) instances considered.
FATA Seminar - Modularity of Random Graphs(25 October, 2016)
Speaker: Fiona Skerman
An important problem in network analysis is to identify highly connected components or `communities'. Most popular clustering algorithms work by approximately optimising modularity. Given a graph G, the modularity of a partition of the vertex set measures the extent to which edge density is higher within parts than between parts; and the maximum modularity q*(G) of G is the maximum of the modularity over all partitions of V(G) and takes a value in the interval [0,1) where larger values indicates a more clustered graph.
Knowledge of the maximum modularity of random graphs helps determine the significance of a division into communities/vertex partition of a real network. We investigate the maximum modularity of Erdos-Renyi random graphs and find there are three different phases of the likely maximum modularity. This is joint work with Prof. Colin McDiarmid.
Bio: Fiona is a postdoc at Bristol University after a doctorate with Colin McDiarmid in Oxford. She has a particular interest in identifying community structure in networks and also more broadly in phase transitions, random graphs, network coding and positional games.
FATA Seminar - What we did in the summer(18 October, 2016)
Speaker: All FATA members
FATA Seminar - Course Allocation with Prerequisites(07 June, 2016)
Speaker: David Manlove
FATA Seminar - The Challenge of Typed Expressiveness in Concurrency(31 May, 2016)
Speaker: Jorge A. Perez
By classifying behaviors (rather than data values), behavioral types abstract structured protocols and enforce disciplined message- passing programs. Many different behavioral type theories have been proposed: they offer a rich landscape of models in which types delineate
concurrency and communication. Unfortunately, studies on formal relations between these theories are incipient. In this talk I will argue that clarifying the relative expressiveness of these type systems is a pressing challenge for formal techniques in distributed systems. I will briefly overview works that
address this issue and discuss promising research avenues. (This talk is based on a short position paper to be presented at FORTE'16.)
FATA Seminar - Preference Elicitation in Matching Markets via Interviews: A Study of Offline Benchmarks(24 May, 2016)
Speaker: Baharak Rastegari
FATA Seminar - The Tinder Stable Marriage Problem(17 May, 2016)
Speaker: Josue Ortega
I study the many-to-many matching problem induced by the popular dating app Tinder. I provide empirical evidence suggesting that its matching procedure is unstable, and show, in a simplified setting, that its assignments can be setwise and even pairwise blocked. Tinder's mechanism can be improved by a known two-step procedure which guarantees setwise stability whenever achievable, i.e. when agents' preferences are strongly substitutable, a restriction compatible with men preferences in online dating. I establish a link between strong substitutability and the maximin property that connects two areas of the literature that remained unrelated, and that can be merged to obtain a useful result: deciding who proposes first generates a tradeoff between the optimality versus the simplicity and privacy of the matching.
FATA Seminar - Autonomous Agent Behaviour Modelled in PRISM(10 May, 2016)
Speaker: Ruth Hoffmann
With the rising popularity of autonomous systems and their increased deployment within the public domain, ensuring the safety of these systems is crucial.
Although testing is a necessary part in the process of deploying such systems, simulation and formal verification are key tools, especially at the early stages of design. Simulation allows us to view the continuous dynamics and monitor behaviour of a system. On the other hand, formal verification of autonomous systems allows for a cheap, fast, and extensive way to check for safety and correct functionality of autonomous systems, that is not possible using simulations alone.
In this talk I will demonstrate a simulation and the corresponding probabilistic model of an unmanned aerial vehicle (UAV) in an exemplary autonomous scenario and present results of the discrete models. Further, I discuss a possible formal framework to abstract autonomous systems using simulations to inform probabilistic models.
FATA Seminar - Using Session Types for Pop3: A case study(03 May, 2016)
Speaker: Florian Weber
Session types are used to describe communication protocols. We use a case study to show the applicability of session types in the real world and how we bridge the gap between the
abstract message format used in a session type protocol and the concrete message format used by a naturally occurring server. The case study uses POP3, a standard protocol used to retrieve messages from an email server, as an example, presenting an introduction on how to describe standard internet protocols as session types. We use the protocol description language Scribble, which is based on multiparty session types, to express POP3 in the form of a global protocol from which the local protocols for the client and the server are derived. We use a tool called StMungo to translate the Scribble local protocol into a typestate specification, which defines the order in which the communication methods are called, written in Java. We use Mungo, a Java typestate checking tool and compiler, to show that the implementation follows the typestate specification. Mungo checks the correctness of the sequence of method calls. The case study highlights several points of interest for future work on Scribble and the translation process. Furthermore it provides insight into the relationship between Scribble and the real world protocol implementations, suggesting the use of session types for protocol documentation.
FATA Seminar - Session Types: Achievements and Challenges(26 April, 2016)
Speaker: Simon Gay
Session types are type-theoretic specifications of communication protocols, introduced by Kohei Honda and collaborators in the mid-1990s. They define the type and sequence of messages exchanged via a communication medium, and allow type-checking techniques to be used
to verify protocol implementations. Whereas data types codify the static structure of information in a computer program, session types codify the dynamic structure of communication in a software
system. The classic slogan "algorithms + data structures = programs" can be generalised to "programs + communication structures = systems", and the full range of type-checking = technology can be generalised too.
In the simplest form, a session type specifies a straightforward sequence of messages. The type !int.?bool.end describes how to run a protocol on an endpoint of a communication channel: first send an integer, then receive a boolean, then terminate. The other endpoint has the dual type ?int.!bool.end. More complex protocols include choice and repetition. For example, the recursive type S defined by S = &< start}: ?int.!bool.S, stop: end > describes a protocol that offers a choice between start and stop, each with its own continuation protocol. The basic idea for protocol verification is to match the structure of a session type with the use of communication operations in a program.
The twenty years since the introduction of session types have seen a dramatic growth in research activity. There is now a substantial community, and most programming language conferences regularly include papers on session types.
The seminar will introduce session types, survey the main themes and achievements of the field, and suggest directions for future work that are likely to be of interest to researchers from the wider area of programming language design and type theory.
FATA Seminar - On the Relative Expressiveness of Higher-Order Session Processes(19 April, 2016)
Speaker: Dimitrios Kouzapas
FATA Seminar - BIG DATA subgraph query processing: a light filter with smart verification(15 March, 2016)
Speaker: Patrick Prosser
In subgraph isomorphism we have a target graph T and a pattern graph P and the question is “does T contain P?”. This problem is NP-Complete. One of the problems in BIG DATA is, given a graph database (i.e. a collection of target graphs) does a given query (a pattern graph) exist in the database. Therefore, there are many target graphs and many patterns graphs. Current state of the art produces an index for each target and pattern graph, where an index captures a summary of the features in a graph. Prior to performing a subgraph isomorphism test between a pattern P and target T the indices are used to determine if P is trivially not in T. If this test succeeds then T is not a candidate, and if the test fails then a call to a backtracking search algorithm is made for verification. This is the “filter-verification paradigm”. The BIG DATA approach is to spend considerable effort creating sophisticated indices to avoid having to resort to backtracking search i.e. attempt to answer the decision problem with polynomial effort. This only pays off when the majority of decision problems are unsatisfiable, and therefore problems must exist in the easy unsat region for filtering to work. But what happens if we take a different approach? What happens if we put little effort into creating indices and more effort into crafting smarter subgraph isomorphism algorithms? In this talk I will report on work in progress (with Iva Babukova, Ciaran McCreesh and Christine Solnon) in our new approach “a light filter with smart verification”.
FATA Seminar - Kidney exchange simulation and IP models(08 March, 2016)
Speaker: JamesTrimble
Kidney exchange schemes have been employed successfully in many countries (including the UK since 2007) to increase the number of kidney transplants from living donors. It is an NP-hard cycle-packing problem to determine the largest possible set of transplants for a given pool of donors and patients.
This talk will present two pieces of work we carried out recently - the first to develop a more scalable approach to optimising the kidney-exchange problem, and the second to help in policy development.
1. New compact integer-programming models for kidney exchange. I will briefly describe the new models we have developed, which frequently outperform the existing state of the art, and present some LP relaxation tightness results. (Joint work with David Manlove, John Dickerson, Benjamin Plaut and Tuomas Sandholm)
2. A simulation project which we carried out for NHS Blood and Transplant to estimate the effects of several policy options. (Joint work with David Manlove)
FATA Seminar - When can an efficient decision algorithm be used to find and count witnesses?(01 March, 2016)
Speaker: Kitty Meeks
Suppose we have a universe of n elements, and we are interested in subsets of size k that have certain properties; an example would be cycles of length k in a graph on n vertices. We may simply want to know whether a subset with the property exists ("Does the graph contain a cycle of length k?"), but in many applications we will want more information: this might involve *finding* such a subset (rather than just saying one exists), *counting* how many such subsets there are, or *enumerating* a list of all subsets with the desired property.
For a number of problems of this kind, the fastest known exact algorithm for the decision problem is non-constructive: the algorithm returns either "yes" or "no" without finding a subset with the desired property (if one exists). This motivates the study of what further information we can learn about our instance using only this fast, non-constructive decision algorithm.
We will model the decision algorithm as a black-box subroutine, or an oracle which answers queries of the form, "Does the subset X of the universe contain at least one witness?" This is the approach previously adopted by Bjorklund, Kaski, and Kowalik (MFCS 2014), who addressed the problem of using a decision oracle to find a single witness. In this talk, I will discuss some of the situations in which we can go further, using the decision oracle to find or count (almost) all witnesses.
FATA Seminar - Beyond Graphs -- Canonical Images in Permutation Groups(23 February, 2016)
Speaker: Christopher Jefferson
The famous Graph Isomorphism problems asks, given two graphs A and B, if there is a bijection between the vertices of A and B which preserves edges. This problem is important both theoretically, and practically.
Given a large set of graphs, which we wish to separate into isomorphic classes, it is common to take a 'Canonical Image' of each graph (there is an isomorphism between two graphs if and only if they have the same canonical image). This is much more efficient than calculating an isomorphism between each pair of graphs.
The current algorithms for generating canonical images are limited in two ways -- they only operate on graphs, and they allow any permutation of the graph. This talk will show how we can use a similar technique to find canonical images and isomorphisms of a wide range of objects and actions, in any permutation group G.
FATA Seminar - Overview of the new Science of Sensor System Software programme grant (16 February, 2016)
Speaker: Muffy Calder
FATA Seminar - Symmetry breaking for Ramsey colouring(19 January, 2016)
Speaker: Alice Miller
FATA Seminar - Three Problems for Constraint Programmers(08 December, 2015)
Speaker: Patrick Prosser
FATA Seminar - Automated Verification of Quantum Circuits(24 November, 2015)
Speaker: Sarah Sharp
When directly simulated on a classical computer, quantum computations can result in an exponential slowdown, so how can we verify quantum protocols without a quantum computer to hand? In this talk I will go over a few different ways in which formal methods can be used to validate quantum protocols and what, if any, speedups can be achieved in the process.
I will start by presenting ways in which equivalence checking can be used for quantum circuits, which can be done by testing if one circuit representation is equal to another, and how to model the build up of the operations on a set of qubits comparing both mapstate and QUIDD representations and their related operations to attempt to further minimise the runtime.
The previous work by Ebrahim et al. has established a model-checking technique to enable checking the equivalence of protocols described by a specific input language using the stabilizer formalism. By restricting my initial examples to the Clifford group operators, I will demonstrate how the checking of equivalence between pairs of generated circuits can be done using both stabilizer arrays and mapstate representations, looking at the pros and cons of both techniques as well as future approaches.
FATA Seminar - Behavioural prototypes(17 November, 2015)
Speaker: Roland Perera
I'll demo a simple language of concurrent objects which explores the design space between type systems and continuous testing. In our language, finite-state programs are checked automatically for multiparty compatibility. This property of communicating automata, taken from the session types literature but here applied to terms rather than types, guarantees that no state-related errors arise during execution: no object gets stuck because it was sent the wrong message, and every message is processed.
The usual object-oriented notion of subtyping is also interpreted at the level of terms rather than types. An abstraction takes the form of a prototypical implementation against which another program can be automatically tested for behavioural conformance. Any program can act as
an abstraction, and conversely every abstraction is a concrete program that can be executed.
FATA Seminar - Stable Marriage and Roommates problems with restricted edges(10 November, 2015)
Speaker: David Manlove
In the Stable Marriage and Roommates problems, a set of agents is given, each of them having a strictly ordered preference list over some or all of the other agents. A matching is a set of disjoint pairs of mutually acceptable agents. If any two agents mutually prefer each other to their partner, then they block the matching, otherwise, the matching is said to be stable. We investigate the complexity of finding a solution satisfying additional constraints on restricted pairs of agents. Restricted pairs can be either forced or forbidden. A stable solution must contain all of the forced pairs, while it must contain none of the forbidden pairs. In this talk we describe a range of algorithmic results for problems involving computing stable matchings in the presence of restricted edges. Whilst in some cases NP-hardness and strong inapproximability results prevail, certain other cases give rise to polynomial-time algorithms and constant-factor approximation algorithms. This is joint work with Agnes Cseh.
FATA Seminar - Mungo: Typechecking Protocols(03 November, 2015)
Speaker: Dimitrios Kouzapas
We are demonstrating Mungo, a tool developed for type-checking typestate for objects in Java.
Typestate is a notion that embeds a state on the type of an object, with each state allowing
only for certain methods to be called. The demonstration will focus on the relation of Mungo
and communication protocols that are based on global session types.
FATA Seminar - Enumeration of knots(27 October, 2015)
Speaker: Craig Reilly
Enumeration of knots is a key problem for mathematicians working in knot theory, a branch of topology. It has been since the time of Tait and Little in the late 19th century, who tabulated all prime knots up to 10 crossings. Most of the work in tabulating prime knots makes use of DT code representations of knots, however we instead make use of Gauss code representations . This choice of encoding has the advantage that it is relatively easy to understand, however it also presents problems which will be discussed. Our enumeration relies on constraint programming, and it appears that this meeting of CP and topology is novel. The symmetries of the problem are of particular interest and we will explore this during the talk. The material presented borrows heavily from my masters project.
FATA Seminar: When is finding a little graph inside a big graph hard?(20 October, 2015)
Speaker: Ciaran McCreesh
Subgraph isomorphism involves finding a little "pattern" graph inside a larger "target" graph. The problem is NP-complete, but it has lots of important applications. Practical algorithms for the problem can now handle some patterns with up to a thousand vertices, and targets with up to ten thousand vertices---but they cannot handle all such graphs, and we need to make sure we aren't making overly bold claims based upon favourable results from particular benchmark sets.
We've been looking at how to generate really hard random instances for the problem. This isn't as simple as, for example, random maximum clique, because we have lots of parameters we can vary independently. This short talk is mostly about figuring out how we should present the data: we're going to put up some pretty charts with lots of colours, and ask whether you find them helpful in understanding what's going on.
FATA Seminar: Complexity of the n-Queens Completion Problem(13 October, 2015)
Speaker: Ian Gent
The n-Queens problem is to place n chess queens on an n by n chessboard so that no two queens are on the same row, column or diagonal in either direction. This is one of the most famous puzzles there is, and is often - incorrectly - attributed to Gauss. It has very often been used as a benchmark for combinatorial search methods, and also very often criticised as a bad test cases [e.g. see *]. The reason for the criticism is that a solution can be computed in time O(n) for any n > 3.
We show that this criticism does not apply to the completion variant of the problem. That is, given m queens which do not attack each other on an n by n chessboard, can we add n-m queens to get a solution of the n queens problem? We show that this problem is NP-Complete and #P-Complete. We also report how difficult the n-Queens completion problem is on random problems, and thereby seek to rescue the n-Queens problem - in its completion version - as a valid benchmark problem. [This is joint work with Chris Jefferson and Peter Nightingale, St Andrews.]
* see http://www.optaplanner.org/blog/2014/05/12/CheatingOnTheNQueensBenchmark.html
FATA Seminar: On Dots in Boxes or Permutation Pattern Classes(06 October, 2015)
Speaker: Ruth Hoffmann
We will be looking at the notion of permutation pattern classes and the talk will give you a historical and current insight into the work done within permutation patterns and the applications thereof. Additionally, I will shortly talk about the work I have done during my PhD.
FATA Seminar: Probabilistic Formal Analysis of App Usage to Inform Redesign(29 September, 2015)
Speaker: Oana Andrei
Good design of mobile apps is challenging because users are seldom homogeneous or predictable in the ways they navigate around and use the functionality presented to them. Different populations of users will engage in different ways, and redesign may be desirable or even required to support populations’ different styles of use. In this talk I will present a process of app analysis intended to support understanding of use but also redesign. This process is based on inferring activity patterns (Markov models) from usage logs and employing probabilistic formal analysis to ask questions about the use of the app and characterise the inferred activity patterns. I will illustrate this work via a case study of a mobile app presenting analytic findings and finish with discussions on how the analysis results are feeding into redesign.
FATA Seminar: Strong inapproximability results for a class of optimisation problems(16 June, 2015)
Speaker: Iain McBride
The Hospitals / Residents problem with Couples (HRC) is a generalisation of the classical Hospitals / Residents problem (HR) that is important in practical applications because it models the case where couples submit joint preference lists over pairs of (typically geographically close) hospitals. It is known that an instance of HRC need not admit a stable matching. Deciding whether an instance of HRC admits a stable matching is NP-complete even under some very severe restrictions on the lengths of the participants' preference lists.
Since an instance of HRC need not admit a stable matching, it is natural to seek the 'most stable' matching possible, i.e., a matching that admits the minimum number of blocking pairs. We present a gap-introducing reduction that establishes a strong inapproximability result for the problem of finding a matching in an instance of HRC that admits the minimum number of blocking pairs. Further, we show how this result might be generalised to prove that the minimisation counterpart of a number of NP-complete decision problems based on matchings (and even more general NP-complete problems) may be shown to have the same strong inapproximability bound.
Boole's legacy for software(03 June, 2015)
Speaker: Professor Muffy Calder
Professor Muffy Calder will give a short, informal and personal overview of Boole’s legacy for software, in particular the ways in which human and physical processes are systematised and implemented through software systems. But do these systems behave as
Two hundred years ago this year George Boole was born. Boole was a largely self-taught mathematical genius and in 1854, as first Professor of Mathematics at Queen’s College, Cork, he founded the discipline of algebraic logic when he published The Laws of Thought An Investigation of the Laws of Thought on Which are Founded the Mathematical Theories of Logic and Probabilities. In it he proposed the first practical system of logic in algebraic form, now known as Boolean algebra, which was subsequently the foundation for the scientific and engineering work of Alan Turing, Claude Shannon, and many others, in the development of computation and the computer.
Muffy will give a short, informal and personal overview of Boole’s legacy for software, in particular the ways in which human and physical processes are systematised and implemented through software systems. But do these systems behave as we expect, do they behave as we want them to? Can logic help us answer the questions? The talk will explore how we use logics to reason about the software systems we have built, biological systems that have evolved, and some every day uses (and misuses).
FATA Seminar - Notes on the Bankruptcy Game(19 May, 2015)
Speaker: Tamas Fleiner
How to divide the estate among creditors in case of a bankruptcy? An entertaining story in connection with a result of Nobel laureate Aumann and Maschler from studying a long standing mystery about the Talmud with the help of Game Theory. The talk contains one or two proofs, we learn what we should say if we want to be big boys at jail and we also hear about a legal issue in connection with levirate marriage. Prerequisites are standard order and arithmetic operations. (This is joint work with Balazs Sziklai.)
FATA Seminar - A Tale of Two Workshops(12 May, 2015)
Speaker: Baharak Rastegari
David Manlove and I, with the help of a handful of volunteers, organized two international events recently: (i) COST Action IC1205 meeting on Matching and Fair Division, and (ii) 3rd International Workshop on Matching Under Preferences (MATCH-UP 2015). In this talk I'll tell you about an almost one year planning that went to these events, and all the fun and the troubles!
FATA Seminar - Symmetry in Constraint Programming(31 March, 2015)
Speaker: Karen Petrie
Symmetry in constraints has always been important but in recent years has become a major research area in its own right. A key problem in constraint programming has long been recognised: search can revisit equivalent states over and over again. In principle this problem has been solved, with a number of different techniques. Research remains very active for two reasons. First, there are many difficulties in the practical application of the techniques that are known for symmetry exclusion, and overcoming these remain important research problems. Second, the successes achieved in the area so far have encouraged researchers to find new ways to exploit symmetry.
This talk will give a whistle stop tour of symmetry elimination in constraint programming, before looking at what the open problems are which are ripe for research.
FATA Seminar - Progress as Compositional Lock-Freedom(24 March, 2015)
Speaker: Ornela Dardha
A session-based process satisfies the progress property if its sessions never get stuck when it is executed in an adequate context. Pre- vious work studied how to define progress by introducing the notion of catalysers, execution contexts generated from the type of a process. In this paper, we refine such definition to capture a more intuitive notion of context adequacy for checking progress. Interestingly, our new catal- ysers lead to a novel characterisation of progress in terms of the stan- dard notion of lock-freedom. Guided by this discovery, we also develop a conservative extension of catalysers that does not depend on types, gen- eralising the notion of progress to untyped session-based processes. We combine our results with existing techniques for lock-freedom, obtaining a new methodology for proving progress. Our methodology captures new processes wrt previous progress analysis based on session types.
FATA Seminar - Verification and Control of Partially Observable Probabilistic Real-Time Systems(10 March, 2015)
Speaker: Gethin Norman
In this talk I will outline automated techniques for the verification and control of probabilistic real-time systems that are only partially observable. To formally model such systems, we define an extension of probabilistic timed automata in which local states are partially visible to an observer or controller. Quantitative properties of interest, relate to the probability of an event’s occurrence or the expected value of some reward measure. I will propose techniques to either verify that such a property holds or to synthesise a controller for the model which makes it true. The approach is based on an integer discretisation of the model’s dense-time behaviour and a grid-based abstraction of the uncountable belief space induced by partial observability. The latter is necessarily approximate since the underlying problem is undecidable, however both lower and upper bounds on numerical results can be generated.
FATA Seminar - Scheduling sailing match races(03 March, 2015)
Speaker: Patrick Prosser
There is a form of sailing with skippers sailing one-vs-one in a round-robin, known as Match Racing. The early stages of the Americas Cup are done as round-robins. Recently, we have been performing research on how to improve the schedules and to make racing fairer. In this talk I will describe the problem and present the 13 rules described in the ISAF World Sailing Umpire’s Manual for constructing a legal schedule. A constraint model is then presented. We show that some of the published schedules are in fact illegal, violate ISAF rules. There are also some “missing” schedules, some that we believe are provably impossible given the rules. This is a presentation of “work in progress”.
FATA Seminar - Formal analysis of Edinburgh buses using GPS data(24 February, 2015)
Speaker: Daniel Reijsbergen
We present recent work on the development of stochastic performance models of a public transportation network using real-world data. The data is provided to us by the Lothian Buses company, which operates an extensive bus network in Edinburgh. In particular, we use datasets of GPS measurements with about 30-40 seconds between subsequent observations. Some quantities of interest that can be analysed using this data are the times needed to complete specific route segments, and the 'headway', the distance (in terms of journey completion)
between subsequent buses. Both can be modelled using established formalisms, namely Markov chains and time series respectively. We briefly discuss several applications, including a 'what-if' scenario involving the introduction of trams to the Edinburgh city centre, and the evaluation of the punctuality of frequent services in terms of criteria set by the Scottish government.
FATA Seminar - The Subgraph Isomorphism Problem: three new ideas(17 February, 2015)
Speaker: Ciaran McCreesh
In the subgraph isomorphism problem, we are given a pattern graph P, and a target graph T, and we wish to find "a copy of P inside T". I will introduce three new practical improvements to the simple algorithms presented by Patrick last year.
Firstly, I will discuss supplemental graphs. The key idea is that a subgraph isomorphism i from P to T is also a subgraph isomorphism F(i) from F(P) to F(T), for certain transformations F. This lets us generate redundant constraints: we can search for a mapping which is simultaneously a subgraph isomorphism between several carefully selected pairs of graphs.
Secondly, I will introduce an intermediate level of inference for an all-different constraint. Traditionally a matching-based approach is used, but this scales poorly to large target graphs and generally does not provide much additional filtering. We use a weaker counting-based approach, which is much faster and which usually gives the same amount of filtering.
Thirdly, I will revisit conflict-directed backjumping. I will show that there is no need to maintain conflict sets when working with cloned domains. I will also explain how the counting all-different algorithm can produce more fine-grained information on a conflict, allowing longer backjumps.
FATA Seminar - A semantic deconstruction of session types(03 February, 2015)
Speaker: Alceste Scalas
I will illustrate a semantic approach to the foundations of session types, by revisiting them in the abstract setting of labelled transition systems. The crucial insight is a simulation relation which generalises the usual syntax-directed notions of typing and subtyping, and encompasses both synchronous and asynchronous binary session types. This allows to extend the session types theory to some common programming patterns which are not typically considered in the session types literature.
FATA Seminar - Boole's Legacy for Software (27 January, 2015)
Speaker: Muffy Calder
This will be a practice talk for a public lecture (to a scientific audience) I will be giving in Cork to celebrate the 200th anniversary of Boole’s birth. (Boole was a Professor at UC Cork). I will give the polished lecture here in the School later this year, this will be an informal practice where I will look for feedback from FATA.
FATA Planning Meeting(20 January, 2015)
Speaker:
A (hopefully) short meeting to plan the talks for the rest of the year.
FATA Seminar: Type-Based Verification of Message-Passing Parallel Programs(13 January, 2015)
Speaker: Vasco Vasconcelos
We present a type-based approach to the verification of the communication structure of parallel programs. We model parallel imperative programs where a fixed number of processes, each equipped with its local memory, communicates via a rich diversity of primitives, including point-to-point messages, broadcast, reduce, and array scatter and gather. The theory includes a decidable dependent type system incorporating abstractions for the various communication operators, a form of primitive recursion, and collective choice. We further introduce a core programming language for imperative, message-passing, parallel programming, and show that the language enjoys progress. Joint work with Francisco Martins, Eduardo R.B. Marques, Hugo A. López, César Santos and Nobuko Yoshida.
FATA Seminar - Quiz(16 December, 2014)
Speaker: Rob Irving
FATA Seminar - Demand-indexed computation(09 December, 2014)
Speaker: Roland Perera
FATA Seminar - Russian Dolls Search (02 December, 2014)
Speaker: Ciaran McCreesh
Russian Doll Search is a general algorithmic technique for solving hard optimisation problems, which looks a bit like Branch and Bound combined with Dynamic Programming. I'll give an overview of how it works, and what it's been used for, and will then speculate about how we might parallelise it.
FATA Seminar - Choreographies in the wild (25 November, 2014)
Speaker: Massimo Bartoletti
Distributed applications can be constructed by composing services which interact by exchanging messages according to some global communication pattern, called choreography. Under the assumption that each service adheres to its role in the choreography, the overall application is
communication-correct.
However, in wild scenarios like the Web or cloud environments, services may be deployed by different participants, which may be mutually distrusting (and possibly malicious). In these cases, one can not assume (nor enforce) that services always adhere to their roles.
Many formal techniques focus on verifying the adherence between services and choreographic roles, under the assumption that no participant is malicious; in this case, strong communication-correctness results can be obtained, e.g. that the application is deadlock-free. However, in wild
scenarios such techniques can not be applied.
In this talk we present a paradigm for designing distributed applications in wild scenarios. Services use contracts to advertise their intended communication behaviour, and interact via sessions once a contractual agreement has been found. In this setting, the goal of a designer is to realise honest services, which respect their contracts in all execution contexts (also in those where other participants are malicious).
A key issue is that the honesty property is undecidable in general. In this talk we discuss veriﬁcation techniques for honesty, targeted at agents specified in the contract-oriented calculus CO2. In particular, we show how to safely over-approximate the honesty property by a model-checking technique which abstracts from the contexts a service may be engaged with.
FATA Seminar - Life out on the Savannah: formal models meet mixed-reality systems(18 November, 2014)
Speaker: Michele Sevegnani
We report on work with our HCI friends, Tom Rodden and Steve Benford, on modelling and analysis for Benford’s Savannah mixed reality “game”. We show how our novel bigraphical model of four perspectives of the system (computational, technical, human and physical), gives us new ways to analyse relationships between the perspectives and prove formally that there are cognitive dissonances in the system, as exemplified by user-trials.
No bigraph algebra required, we do everything with graphical forms (ie pictures)!
Formal modellers, HCI experts, computer scientists, all welcome!
FATA Seminar - Subgraph Isomorphism Problem: simple algorithms(11 November, 2014)
Speaker: Patrick Prosser
In the subgraph isomorphism problem (SIP), we are given two graphs, G and H where G is a the pattern graph and H the target. The problem is then to determine if there is a subgraph of H (the target graph) that is isomorphic to G (the pattern graph). Generally, the problem is NP-hard. I will present some simple SIP algorithms, all using BitSet encodings, and progressively modify a base algorithm to give more sophisticated algorithms that better exploit problem structure.
FATA Seminar - Linear numeral systems(04 November, 2014)
Speaker: Ian Mackie
We take a fresh look at an old problem of representing natural numbers in the lambda-calculus. Our interest is in finding representations where we can compute efficiently (and where possible, in constant time) the following functions: successor, predecessor, addition, subtraction and test for zero. Surprisingly, we find a solution in the linear lambda-calculus, where copying and erasing are not permitted.
FATA Seminar - Size versus truthfulness in the House Allocation problem(28 October, 2014)
Speaker: Baharak Rastegari
I will present our result from last year (presented in EC 2014) on designing truthful mechanisms for the House Allocation (HA) problem. HA is the problem of allocating a set of objects among a set of agents, where each agent has ordinal preferences (possibly involving ties) over a subset of the objects. We focus on truthful mechanisms without monetary transfers for finding large Pareto optimal matchings.
FATA Seminar - New Software Applications for Kidney Exchange(21 October, 2014)
Speaker: David Manlove
In this talk I will give some background to kidney exchange in the UK context, and present some recent results from quarterly matching runs. I will then give an overview of two new software applications for kidney exchange that emerged from summer MSc projects. The first of these, due to Tommy Muggleton, is a tool for visualising input datasets and optimal solutions for kidney exchange problem instances. The second, due to James Trimble, allows datasets to be generated that are a better reflection of the UK real data than a previous generator produced, and also permits characteristics of datasets to be analysed, and optimal solutions to be compared and contrasted with respect to different optimality criteria.
FATA Seminar - An introduction to knot theory(14 October, 2014)
Speaker: Brendan Owens
I will give a gentle introduction to mathematical knot theory, focusing on combinatorial aspects that may be of interest to computing scientists, and avoiding technical details. Topics include knot diagrams and Reidemeister moves, knots and graphs, tabulation of knots, and some discussion of ways of encoding knots. I will include a brief description of my ongoing search for alternating ribbon knots (joint with Frank Swenton).
FATA Summer Summary, or, how did you spend your summer?(07 October, 2014)
Speaker: FATA members
Complex networks and complex processes(27 May, 2014)
Speaker: Professor Simon Dobson
There is increasing interest in using complex networks to model phenomena, and especially in the construction of systems of networks that interact and respond to each other -- the so-called complex adaptive coupled networks. They seem to offer a level of abstraction that is appropriate for capturing the large-scale dynamics of real-world processes without becoming lost in the detail. This talk introduces such networks for a formal audience, describes some recent work in urban traffic modelling, and speculates on the combination of complex networks with sensor data to study environmental incidents such as flooding.
Reasoning about Optimal Stable Matchings under Partial Information(20 May, 2014)
Speaker: Baharak Rastegari
We study two-sided matching markets in which participants are initially endowed with partial preference orderings, lacking precise information about their true, strictly ordered list of preferences. We wish to reason about matchings that are stable with respect to agents' true preferences, and which are furthermore optimal for one given side of the market. We present three main results. First, one can decide in polynomial time whether there exists a matching that is stable and optimal under all strict preference orders that refine the given partial orders, and can construct this matching in polynomial time if it does exist. We show, however, that deciding whether a given pair of agents are matched in all or no such optimal stable matchings is co-NP-complete, even under quite severe restrictions on preferences. Finally, we describe a polynomial-time algorithm that decides, given a matching that is stable under the partial preference orderings, whether that matching is stable and optimal for one side of the market under some refinement of the partial orders.
Mining Behavior Models from User-Intensive Web Applications(13 May, 2014)
Speaker: Dr. Giordano Tamburrelli
Many modern user-intensive applications, such as Web applications, must satisfy the interaction requirements of thousands if not millions of users, which can be hardly fully understood at design time. Designing applications that meet user behaviors, by efficiently supporting the prevalent navigation patterns, and evolving with them requires new approaches that go beyond classic software engineering solutions.
In this talk we present a preliminary approach called BEAR that automates the acquisition of user-interaction requirements in an incremental and reflective way. More precisely, the approach builds upon inferring a set of probabilistic Markov models of the users’ navigational behaviors, dynamically extracted from the interaction history given in the form of a log file. BEAR builds on top of a well established formal tool, indeed it analyzes the inferred models to verify quantitative properties by means of probabilistic model checking. The talk discusses the capabilities of BEAR and illustrates the preliminary results obtained on a Web application currently in use.
Mining Behavior Models from User-Intensive Web Applications(06 May, 2014)
Speaker: Dr Giordano Tamburrelli
Many modern user-intensive applications, such as Web applications, must satisfy the interaction requirements of thousands if not millions of users, which can be hardly fully understood at design time. Designing applications that meet user behaviors, by efficiently supporting the prevalent navigation patterns, and evolving with them requires new approaches that go beyond classic software engineering solutions.
In this talk we present a preliminary approach called BEAR that automates the acquisition of user-interaction requirements in an incremental and reflective way. More precisely, the approach builds upon inferring a set of probabilistic Markov models of the users’ navigational behaviors, dynamically extracted from the interaction history given in the form of a log file. BEAR builds on top of a well established formal tool, indeed it analyzes the inferred models to verify quantitative properties by means of probabilistic model checking. The talk discusses the capabilities of BEAR and illustrates the preliminary results obtained on a Web application currently in use.
Do I need to fix a failed component now, or can I wait until tomorrow? (06 May, 2014)
Speaker: Prof Muffy Calder
Ideally in systems in which failures are monitored and sensed, an engineer would fix a failure immediately. But this might not be possible due to limited resources and/or physical distance to a device. So how does an engineer prioritise and make best use of their resources, while still ensuring the service is operating within acceptable levels of risk of failure?
We hypothesise predictive event-based modelling and reasoning with a stochastic temporal logic can inform decision making when failures occur. We show, with a real industrial case study (a safety critical comms system for NATS), that by relating the status of assets to service behaviour in a CTMC model, the risk of service failure now, and over various time frames, future failure rates, and interventions, can be quantified. We reason both in the context of how the system is designed to meet service requirements, and how it actually meets service requirements, when the models are calibrated with rates derived from historical, field data.
Canonical Labelling of Graphs(29 April, 2014)
Speaker: Dr Alice Miller
Many of us in FATA are concerned with symmetry in combinatorial objects, specifically in the use of isomorphism checking to eliminate copies of the same object during their generation, or to prevent redundant work during combinatorial search (for example, during model checking). I have been using the graph isomorphism package, nauty, for years, and eventually decided that I should find out how it works!
The most efficient method used for graph isomorphism checking is that of using a certificate, or cononical labelling . A canonical labelling is a function C that maps any graph to a natural number in such a way that C(G1)=C(G2) if and only if G1 and G2 are isomorphic. In this talk I discuss canonical labelling of trees, and of graphs in general. For the latter, I describe the popular algorithm using equitable partitions used by the most successful graph isomorphism programs such as nauty. The talk will include explanatory examples and pictures and no pseudocode!
FATA Seminar - Profile-based optimal matchings in the Student/Project Allocation(18 March, 2014)
Speaker: Augustine Kwanashie
Profile-based optimal matchings in the Student/Project Allocation
In the Student/Project Allocation problem (SPA) we seek to assign students
to group or individual projects offered by lecturers. Students are required
to provide a list of projects they find acceptable in order of preference.
Each student can be assigned to at most one project and there are
constraints on the maximum number of students that can be assigned to each
project and lecturer. A matching in this context is a set of
student-project pairs that satisfies these constraints.
We seek to find matchings that satisfy optimality criteria based on the
profile of a matching. This is a vector whose ith component indicates the
number of students obtaining their ith-choice project. Various profile-based
optimality criteria have been studied. For example, one matching M1 may be
preferred to another matching M2 if M1 has more students with first-choice
projects than M2.
In this talk we present an efficient algorithm for finding optimal matchings
to SPA problems based on various well known profile-based optimality
criteria. We model SPA as a network flow problem and describe a modified
augmenting path algorithm for finding a maximum flow which can then be
transformed to an optimal SPA matching. This approach allows for additional
constraints, such as project and lecturer lower quotas, to be handled
flexibly without modifying the original algorithm.
FATA Seminar - Verifying Differential Privacy by Program Logic(11 March, 2014)
Speaker: Marco Gaboardi
Verifying Differential Privacy by Program Logic
Differential Privacy is becoming a standard approach in data privacy: it offers ways to answer queries about sensitive information while providing strong, provable privacy guarantees, ensuring that the presence or absence of a single individual in the database has a negligible statistical effect on the query's result. Many specific queries have been shown to be differentially private, but manually checking that a given query is differentially private can be both tedious and rather subtle. Moreover, this process becomes unfeasible when large programs are considered.
In this talk I will introduce the basics of differential privacy and some of the fundamental mechanisms for building differentially private programs. Additionally, I will present a verification approach based on Hoare Logic useful to certify a broad range of probabilistic programs as differentially private.
FATA Seminar - Verification of Concurrent Quantum Protocols by Equivalence Checking(04 March, 2014)
Speaker: Simon Gay
Verification of Concurrent Quantum Protocols by Equivalence Checking
We present a tool which uses a concurrent language for describing quantum systems, and performs verification by checking equivalence between specification and implementation. In general, simulation of quantum systems using current computing technology is infeasible. We restrict ourselves to the stabilizer formalism, in which there are efficient simulation algorithms.
In particular, we consider concurrent quantum protocols that behave functionally in the sense of computing a deterministic input-output relation for all interleavings of the concurrent system.
Crucially, these input-output relations can be abstracted by superoperators, enabling us to take advantage of linearity. This allows us to analyse the behaviour of protocols with arbitrary input, by simulating their operation on a finite basis set consisting of stabilizer states.
Despite the limitations of the stabilizer formalism and also the range of protocols that can be analysed using this approach, we have applied our equivalence checking tool to specify and verify interesting and practical quantum protocols from teleportation to secret sharing.
Joint work with Ebrahim Ardeshir-Larijani and Rajagopal Nagarajan.
FATA Seminar - Backbones for equality(25 February, 2014)
Speaker: Mike Codish
Backbones for equality
Mike is visiting the school between 24th and 26th February, 2014. His research interests include the development and application of formal techniques to aid in the compilation and implementation of sequential and concurrent logic programs and to analyse, optimise and reason about such programs. In this talk Mike will give a general introduction to his work. Specifically, he will describe his structured approach to solving finite domain constraint problems through an encoding to SAT, and the BEE tool (Ben-Gurion Equi-propogation Encoder). He will introduce the notion of the backbone of a CNF formula, and describe his recent work, in which backbones are generalized to capture equations between literals.
FATA Seminar - Sudoku as an Assessed Exercise in Constraint Programming: an analysis of student programming ability (18 February, 2014)
Speaker: Patrick Prosser
Sudoku as an Assessed Exercise in Constraint Programming: an analysis of student programming ability
In the Constraint Programming course (Masters) the first exercise is to code up a solver for the Sudoku puzzle, investigating the effect of using 2 subtly different models and checking that problem instances do indeed have unique solutions. I will present snippets of java code from the 29 students who submitted work. Much of this presentation will be entertaining, but the underlying message is rather serious.
FATA Seminar - An Exact Branch and Bound Algorithm with Symmetry Breaking for the Maximum Balanced Induced Biclique Problem(11 February, 2014)
Speaker: Ciaran McCreesh
An Exact Branch and Bound Algorithm with Symmetry Breaking for the Maximum Balanced Induced Biclique Problem
Garey and Johnson's Hard Problem GT24 is to determine whether a given graph contains a balanced induced biclique of a particular size. We already have some good algorithms for the maximum clique problem---we adapt these, to introduce the first branch and bound algorithm for the maximum balanced induced biclique problem.
But why care about balanced induced bicliques? We are not aware of any applications (although other biclique variants do show up in data mining). Instead, we are interested because the problem has some nice properties from an algorithmic perspective: solutions are reasonably well-behaved, and it has the simplest possible non-trivial symmetry. We show how the the symmetry can be removed, using only two small lines of code. But how much easier does this make the problem? How do symmetries interact with branch and bound? What about parallel branch and bound? And what's going on with random graphs?
FATA Seminar - Stability in networks(04 February, 2014)
Speaker: Ágnes Cseh
Stability in networks
The well-known notion of stable matchings can be extended in several interesting ways, one of them operates with network flows. The stable flow problem lies on the border of Mathematics, Economics and Computer Science. We are given a directed network, where the vertices symbolize vendors, while the edges stand for the possible deals between them. We talk about stability if there is no pair of vendors who mutually want to change the current flow of goods. In this talk, we shorty summarize the results currently known about the problem. Besides showing algorithms to find such flows, we also sketch problems related to max flows, flows over time, restricted edges, multicommodity flows and uncoordinated markets.
Session Types Revisited(28 January, 2014)
Speaker: Ornela Dardha
Session Types Revisited
2 months in California: from bigraphs to autonomous vehicles (+ a bit of sunshine)(21 January, 2014)
Speaker: Michele Sevegnani
2 months in California: from bigraphs to autonomous vehicles (+ a bit of sunshine)
Professor Sengupta's group at UC Berkeley has been investigating the use of the BigActor Model as a formalism for modelling and controlling systems of autonomous vehicles such as Unmanned Air Vehicles (UAV) Autonomous Surface Vehicles (ASV) and Autonomous Underwater Vehicles (AUV). BigActors are distributed concurrent computational entities that interact with a dynamical structure of the world modelled as a bigraph. An example application of BigActors is the specification of environmental monitoring missions in which teams of autonomous vehicles collaborate for locating and tracking oil spills in the ocean.
The aim of my recent visit to UC Berkeley was to adapt and combine the modelling and verification approach developed at Glasgow for the the Homework run-time verification system with the BigActor Model in order to define a general framework for analysis of mobile robotic systems. In this talk, I will present the first step in this direction: an encoding of BigActors to bigraphs. This is work in progress. |
FATA Seminar - Christmas Quiz(17 December, 2013)
Speaker: Simon Gay
FATA Christma Quiz
FATA Seminar - What do we mean by persistence in stochastic models? (10 December, 2013)
Speaker: Rebecca Mancy
What do we mean by persistence in stochastic models?
FATA Seminar - Two-sided Matching with Partial Information (26 November, 2013)
Speaker: Baharak Rastegari
Two-sided Matching with Partial Information
"Two-sided matching markets model many practical settings, such as corporate hiring and university admission. In the traditional model, it is assumed that all agents have complete knowledge of their own preferences. As markets grow large, however, it becomes impractical for agents to precisely assess their rankings over all agents on the other side of the market. We propose a novel model of two-sided matching in which agents start with partial information about their preferences, but are able to refine this information via interviews. Our goal is to design a centralized interview policy that guarantees the outcome to be stable and optimal for one side of the market, while minimizing the number of interviews. We give evidence suggesting that the problem is hard in the general case, and show that it is polynomial-time solvable in a restricted, yet realistic, setting."
FATA Seminar - Cliques, Bicliques, Clubs and Colours(19 November, 2013)
Speaker: Ciaran McCreesh
Cliques, Bicliques, Clubs and Colours
A clique in a graph is a set of vertices, each of which is adjacent to every other vertex in this set. Finding a maximum clique is one of the fundamental NP-hard problems. We discuss how a branch and bound algorithm using greedy graph colouring can be used to solve this problem in practice. We then show how to adapt the algorithm to find maximum independent sets, maximum balanced bicliques, and maximum k-cliques (if a clique is a set of friends, a 2-clique is a set of people who are either friends or who have a mutual friend, and a k-clique is a set of people separated by distance at most k). We finish with a discussion about k-clubs, which are a stricter variation of k-cliques.
FATA Seminar(12 November, 2013)
Speaker: Dimitrios Kouzapas
Globally Governed Session Semantics
This paper proposes a new bisimulation theory based on multiparty session types where a choreography specification governs the behaviour of session typed processes and their observer. The bisimulation is defined with the observer cooperating with the observed process in order to form complete global session scenarios and usable for proving correctness of optimisations for globally coordinating threads and processes. The induced bisimulation is strictly more fine-grained than the standard session bisimulation. The difference between the governed and standard bisimulations only appears when more than two interleaved multiparty sessions exist. The compositionality of the governed bisimilarity is proved through the soundness and completeness with respect to the governed reduction-based congruence.
FATA Seminar(05 November, 2013)
Speaker: Muffy Calder
How to win users and influence developers with probabilistic user meta models.
A short talk outlining the definition and role of new probabilistic meta models of user activity patterns for a mass deployed app - how can reasoning about the meta models include future developments of an app? A lively fusion of formal modelling, model checking, HCI and statistics, courtesy of the Populations project.
FATA Seminar(29 October, 2013)
Speaker: Patrick Prosser
Constraint Programming and Stable Roommates
In the stable roommates problem we have n agents, where each agent ranks all other agents. The problem is then to match agents into pairs such that no two agents prefer each other to their matched partners. A remarkably simple constraint encoding is presented that uses O(n^2) binary constraints, and in which arc-consistency (the phase-1 table) is established in O(n^3) time. This leads us to a specialised n-ary constraint that uses O(n) additional space and establishes arc-consistency in O(n^2) time. An empirical study is presented and it is observed that the n-ary constraint model can read in, model and output all matchings for an instances with n = 1,000 in about 2 seconds on current hardware platforms. This leads us to a question: egalitarian SR is NP-hard, but where are the hard problems?
FATA Seminar(22 October, 2013)
Speaker: Various
Short talks for the summer research of the group and planning
On being the CSA for Scottish Government(04 June, 2013)
Speaker: Muffy Calder
An overview of what I do in "the other job".
On List Colouring and List Homomorphism of Permutation and Interval Graphs (28 May, 2013)
Speaker: Jessica Enright
List colouring is an NP-complete decision problem even if the total number of colours is three. It is hard even on planar bipartite graphs. I give a sketch of a polynomial-time algorithm for solving list colouring of permutation graphs with a bounded total number of colours. This generalises to a polynomial-time algorithm that solves the list-homomorphism problem to any fixed target graph for a large class of input graphs including all permutation and interval graphs.
The Hospitals/Residents problem with Free pairs(30 April, 2013)
Speaker: Augustine Kwanashie
In the classical Hospitals/Residents problem, a blocking pair exists with respect to a matching if both agents would be better off by coming together, rather than remaining with their partners in the matching (if any). However blocking pairs that exist in theory need not undermine a matching in practice. The absence of social ties between agents may cause a lack of awareness about the existence of blocking pairs in practice. We define the Hospitals/Residents problem with Free pairs (HRF) in which a subset of acceptable resident-hospital pairs are identified as free. This means that they can belong to a matching M but they can never block M. Free pairs essentially correspond to resident and hospitals that do not know one another. Relative to a relaxed stability definition for HRF, called local stability, we show that locally stable matchings can have different sizes and the problem of finding a maximum locally stable matching is NP-hard, though approximable within 3/2. Furthermore we give polynomial time algorithms for two special cases of the problem. This is joint work with David Manlove.
A hierarchy related to interval orders(16 April, 2013)
Speaker: Sergey Kitaev
A partially ordered set (poset) is an interval order if it is isomorphic to some set of intervals on the real line ordered by left-to-right precedence. Interval orders are important in mathematics, computer science, engineering and the social sciences. For example, complex manufacturing processes are often broken into a series of tasks, each with a specified starting and ending time. Some of the tasks are not time-overlapping, so at the completion of the first task, all resources associated with that task can be used for the following task. On the other hand, if two tasks have overlapping time periods, they compete for resources and thus can be viewed as conflicting tasks.
A poset is said to be (2+2)-free if no two disjoint 2-element chains have comparable elements. In 1970, Fishburn proved that (2+2)-free posets are precisely interval orders. Recently, Bousquet-Mélou, Claesson, Dukes, and Kitaev introduced ascent sequences, which not only allowed us to enumerate interval orders, but also to connect them to other combinatorial objects, namely to Stoimenow's matchings, to certain upper triangular matrices, and to certain pattern avoiding permutations (a very active area of research these days). A host of papers by various authors has followed this initial paper.
In this talk, I will review some of results from these papers and will discuss a hierarchy of objects related to interval orders.
Using formal stochastic models to guide decision making -- Should I fix this problem now or in 3 hours?(19 March, 2013)
Speaker: Michele Sevegnani
NATS is the UK's main air navigation service provider. Its control centre in Prestwick constantly monitors the status of its infrastructure via thousands of sensors situated in numerous radar and communication sites all over the UK's territory. The size and complexity of this system often makes it difficult to interpret the sensed data and impossible to predict the system's future behaviour.
In this talk, we present on-going work in which a stochastic model is used to guide decision making. In particular, we will show a prototype web-app based on the formal model that could allow the engineering team in the control room to perform stochastic model checking in a simple and intuitive way, without prior knowledge of formal methods. The analysis results can then be used to schedule, prioritise and optimise maintenance, without affecting safety.
Extremal graphs (12 March, 2013)
Speaker: Patrick Prosser and Alice Miller
Formal Models for Populations of User Activity Patterns and Varieties of Software Structures(05 March, 2013)
Speaker: Oana Andrei
The challenges raised by developing mobile applications come from the way these apps interweave with everyday life and are distributed globally via application centres or stores to a wide range of users. People use an app according to their needs and understanding, therefore one could observe variations in usage frequencies of features or time and duration of use. The same mobile app varies with app settings, mobile device settings, device model or operating system.
For this talk we present work in progress on a formal modelling approach suitable for representing and analysing the user activity patterns and the structural variability of a software system. It is based on a stochastic abstraction of the populations of software in use and the software uses, building upon results from statistical analysis of user activity patterns. One aim of our current research is to design for variability of uses and contexts that mobile software developers may not be able to fully predict. Based on the automatically logged feedback on in-app usage and configurations, inference methods and formal modelling and analysis connect and collaborate to provide information on relevant populations of similar user behaviour and software structure and to evaluate their performance and robustness. This way we can track behavioural changes in the population of users and suggest software improvements to fit new user behaviours and contexts and changes in the user behaviour. The software designers and developers will then (re)consider the design objectives and strategies, create more personalised modules to be incorporated in the software and identify new opportunities to improve the overall user experience. We use a real life case study based on an iOS game to illustrate the concepts.
This talk is based on a joint work with Muffy Calder, Mark Girolami and Matthew Higgs.
Model Checking Port-Based Network Access Control for Wireless Networks(26 February, 2013)
Speaker: Yu Lu
With the rapid development of Internet, the security of network protocols becomes the focus of research. The 802.1X standard is the IEEE standard for port-based network access control. The 802.1X standard delivers powerful authentication and data privacy as part of its robust, extensible security framework. It is this strong security, assured authentication, and dependable data protection that has made the 802.1X standard the core ingredient in today’s most successful network access control (NAC) solutions. As the central access authentication, the importance of IEEE 802.1X protocol's security properties is obvious. Formal methods is an crucial software and protocol analysis and verification tool. Formal methods includes model checking, logic inference, and theorem proving, etc.
We could use model checking to help analyse security protocols by exhaustively inspecting reachable composite system states in a finite state machine representation of the system. The IEEE 802.1X standard provides port-based network access control for hybrid networking technologies. We describe how the current IEEE 802.1X mechanism for 802.11 wireless networks can be modelled in the PROMELA modelling language and verified using the SPIN model checker. We aim to verify a set of essential security properties of the 802.1X, and also to find out whether the current combination of the IEEE 802.1X and 802.11 standards provide a sufficient level of security.
On Al Roth Nobel Prize-winning lecture(29 January, 2013)
Speaker: David Manlove
The 2012 Sveriges Riksbank Prize in Economic Sciences in Memory of Alfred Nobel (commonly known as the Nobel Prize in Economics) was awarded jointly to Professors Alvin E Roth and Lloyd S Shapley (see http://www.nobelprize.org/nobel_prizes/economics/laureates/2012/) "for the theory of stable allocations and the practice of market design".
Lloyd Shapley is the co-author of the famous Gale-Shapley algorithm (with David Gale, who sadly died in 2008). Al Roth has been instrumental in turning theory into practice through his involvement with centralised clearinghouses in many application domains, including junior doctor allocation and kidney exchange, in addition to contributing many important theoretical results himself.
The Nobel Prize announcement was made on 15 October, and the two laureates gave their award lectures on 8 December before receiving the awards on 10 December. We will watch Al Roth’s lecture, entitled “The Theory and Practice of Market Design” (43 mins). This is highly relevant to FATA research, as well as being very accessible to anyone who is interested in knowing “who gets what” when it comes to sharing around scarce resources.
The Hospitals Residents Problem with Couples(11 December, 2012)
Speaker: Iain McBride
The Hospitals Residents Problem (HR) is a familiar problem which seeks a stable bipartite matching amongst two sets: one containing residents and one containing hospitals. Each group expresses a strict linear preference over some subset of the members of the other set. The problem is well understood and an efficient algorithm due to Gale and Shapley exists which guarantees to find a stable matching in an instance of HR.
However, the problem becomes intractable when the residents are able to form linked pairs, or couples. This problem is known as the Hospitals Residents Problem with Couples (HRC). In this case Ronn has previously shown that the problem of deciding whether a stable matching exists in an instance of HRC is NP-complete. We show that this NP-completeness result holds for very restricted versions of HRC. Further, we provide an IP formulation for finding a stable matching in an instance of HRC, or reporting that the instance supports no stable matching, and provide early empirical results derived from this IP model.
A model checking approach for air traffic control requirement analysis (04 December, 2012)
Speaker: Michele Sevegnani
NATS provides air traffic navigation services to over 6,000 aircraft flying through UK controlled airspace every day. The huge challenge faced by the engineering team at the NATS control centre in Prestwick is to monitor constantly the status of the equipment required to provide safe and efficient en route services. This involves interpreting and unstructured data feed generated by thousands of diverse sensors such as communication link monitors but also intrusion sensors.
In this talk we will describe how stochastic modelling and checking can be employed to help in this task. Our models allow us to quantify the overall performance of the monitoring system and the quality of the service provided, to predict future behaviours, to react to external events and to plan future upgrades by identifying weaknesses of the system and optimise assets.
PEPA and the Diffusion Problem (20 November, 2012)
Speaker: Michael Jamieson
PEPA, a formalism for keeping track of events during interacting stochastic processes, has been advocated in this School for use in biological investigations. An example is the study of nitric oxide diffusing in a blood vessel. In this talk I will suggest that PEPA be regarded as complementary to another method, which I will describe, of accounting for this diffusion.
The Trials and Tribulations of Typestate Inference(13 November, 2012)
Speaker: Iain McGinniss
Typestate is the combination of traditional object-oriented type theory with finite state machines that represent allowable sequences of method calls. A textual definition of a typestate, as required in specifying the type of a function parameter, is verbose to the point of being impractical. Therefore it is desirable to be able to omit such definitions where they can be accurately inferred. In this talk, I shall discuss my attempts to formally define and prove a typestate inference algorithm for a simple calculus, TS1.
An Integer Programming Approach to the Hospitals/Residents Problem with Ties(06 November, 2012)
Speaker: Augustine Kwanashie
Matching problems generally involve the assignment of agents of one set to those of another. Often some or all of the agents have preferences over one another. An example of such a problem is the Hospitals/Residents problem with Ties (HRT) which models the problem of assigning graduating medical students to hospitals based on agents having preferences over one another, which can involve ties. Finding a maximum stable matching given an HRT instance is known to be NP-hard. We investigate integer programming techniques for producing optimal stable matchings that perform reasonably well in practice. Gains made in the size of these matchings can deliver considerable benefits in some real-life applications. We describe various techniques used to improve the performance of these integer programs and present some empirical results.
Pi-Cost and a brief introduction to DR-PI-OMEGA and DR-PI - Towards Formalizing the Cost of Computation in a Distributed Computer Network (16 October, 2012)
Speaker: Manish Gaur
The picalculus is a basic abstract language for describing communicating processes and has a very developed behavioural theory expressed as equivalence relation between process descriptors; A process P equivalent to a process Q signifies that although P and Q may be intentionally very different they offer essentially same behaviour to the users. The basic language and its related theory has been extended in myriad ways in order to incorporate many different aspect of concurrent behaviour. In this talk, we present a new variation on the picalculus, picost, in which the use of channels must be paid for. Processes operate relative to a cost environment; and communication can only happen if principals have provided sufficient funds for the channels associated with the communications. We define a bisimulation based behavioural preorder in which processes are related if, intuitively, they exhibit the same behaviour but one may be efficient than the other. We justify our choice of preorder by proving that it is characterised by three intuitive properties which behavioural preorders should satisfy in a framework in which the use of resources must be funded.
This development, apart from other applications, is useful in formalising a distributed network with routers acting as an active component in determining the quality of service of the network. We developed two formal languages for distributed networks where computations are described explicitly in the presence of routers. Our model may be considered as an extension of the asynchronous distributed pi-calculus (ADpi). We believe that such models help in prototyping the routing algorithms in context of large networks and reasoning about them while abstracting away the excessive details. Being general, the model may also be applied to demonstrate the role of routers in determining the quality of services of the network. Further in this talk, we intend to very briefly describe the frame work and results obtained about such descriptions.
Empirical Computer Science: how not to do it(09 October, 2012)
Speaker: Patrick Prosser
Empirical Computer Science is hard. To do it well you have to be ruthlessly honest and more than a little bit paranoid. I will present two examples of "How Not to do Empirical Computer Science". NOTE: "All persons, places, and events in this presentation are real. Certain speeches and thoughts are necessarily constructions by the presenter. No names have been changed to protect the innocent, since God Almighty protects the innocent as a matter of Heavenly routine." (quote plagiarized from Kurt Vonnegut's The Sirens of Titan)
Of bison and bigraphs: modelling interactions in physical/virtual spaces(15 May, 2012)
Speaker: Muffy Calder
Mixed reality systems present a wide range of challenges for formal modelling -- how can we model interactions in both physical and virtual spaces? We start to explore this question through a specific application: modelling Steve Benford's Savannah game using Bigraphical reactive systems. The Savannah game is a collaborative, location-based game in which groups of `lions' (i.e. children with devices) hunt together on a virtual savannah that is overlaid on a (physical) open playing field. This work is in the preliminary stages and so unusually for a formal methods talk, we will not give the details of *any* formal models! Instead we will focus on which aspects of the game we can formalise and reason about, and assumptions about the level of detail required for the physical space and for the virtual space.