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.
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)
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.
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.
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.
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.
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.
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.
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.
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.
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.
Extremal graphs (12 March, 2013)
Speaker: Patrick Prosser and Alice Miller
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.
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.
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.
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.
On being the CSA for Scottish Government (04 June, 2013)
Speaker: Muffy Calder
An overview of what I do in "the other job".
FATA Seminar (22 October, 2013)
FATA Seminar (29 October, 2013)
Speaker: Patrick Prosser
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 (05 November, 2013)
Speaker: Muffy Calder
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 (12 November, 2013)
Speaker: Dimitrios Kouzapas
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 - Cliques, Bicliques, Clubs and Colours (19 November, 2013)
Speaker: Ciaran McCreesh
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 - Two-sided Matching with Partial Information (26 November, 2013)
Speaker: Baharak Rastegari
"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 - What do we mean by persistence in stochastic models? (10 December, 2013)
Speaker: Rebecca Mancy
In this talk I will present some of the research I'm currently working on relating to disease persistence in structured populations (e.g. those that have spatial structure or multiple host species). I will briefly introduce the model that prompted this work and the analytic theory associated with it that gives a measure of persistence capacity and a persistence threshold for deterministic models. I will then describe the computational study that I am currently working on to establish the extent to which this threshold is informative about behaviour in a stochastic version of the model.
In the second part of the talk, I will introduce several definitions of persistence from the literature and others that I have briefly considered, explaining why I believe that these don't fully capture what it is that we want to know about the system. Finally, I will introduce (early thoughts on) a new measure of stochastic persistence that I am working on, highlighting aspects of implementation that might provide interesting problems in algorithm development.
FATA Seminar - Christmas Quiz (17 December, 2013)
2 months in California: from bigraphs to autonomous vehicles (+ a bit of sunshine) (21 January, 2014)
Speaker: Michele Sevegnani
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.
Session Types Revisited (28 January, 2014)
Speaker: Ornela Dardha
Session types are a formalism to model structured communication- based programming. A session type describes communication by specifying the type and direction of data exchanged between two parties. When session types and session primitives are added to the syntax of standard π-calculus types and terms, they give rise to ad- ditional separate syntactic categories. As a consequence, when new type features are added, there is duplication of efforts in the theory: the proofs of properties must be checked both on ordinary types and on session types. We show that session types are encodable in ordinary π types, relying on linear and variant types. Besides being an expressivity result, the encoding (i) removes the above redun- dancies in the syntax, and (ii) the properties of session types are derived as straightforward corollaries, exploiting the correspond- ing properties of ordinary π types. The robustness of the encoding is tested on a few extensions of session types, including subtyping, polymorphism and higher-order communications.
FATA Seminar - Stability in networks (04 February, 2014)
Speaker: Ágnes Cseh
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.
FATA Seminar - An Exact Branch and Bound Algorithm with Symmetry Breaking for the Maximum Balanced Induced Biclique Problem (11 February, 2014)
Speaker: Ciaran McCreesh
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 - Sudoku as an Assessed Exercise in Constraint Programming: an analysis of student programming ability (18 February, 2014)
Speaker: Patrick Prosser
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 - Backbones for equality (25 February, 2014)
Speaker: Mike Codish
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 - Verification of Concurrent Quantum Protocols by Equivalence Checking (04 March, 2014)
Speaker: Simon Gay
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 - Verifying Differential Privacy by Program Logic (11 March, 2014)
Speaker: Marco Gaboardi
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 - Profile-based optimal matchings in the Student/Project Allocation (18 March, 2014)
Speaker: Augustine Kwanashie
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.