This presentation will look at the steps we have taken towards practical verification of railway signalling interlocking logic using formal verification.
The theory is well demonstrated, and we have been working on some steps towards a system for use by railway signalling engineers.
Some of the issues we will consider:
How to convey understanding about formal verification - what is checked, what is not checked;
How to express safety properties;
How to capture railway geography;
How to provide a User Interface;
How to present the results;
How would formal verification fit within the overall process for interlocking data.
There is no way to implement all of intuitionistic real analysis or even formalize it.
Brouwer, the primary creator of intuitionistic mathematics, knew this and said that
a construction of the continuum is inconceivable. We will explain in this lecture why
that is so. This is not the case for the Bishop and Bridges account of constructive
analysis. Dr. Mark Bickford has implemented significant parts of constructive analysis
in Nuprl. It might be possible to implement the entire book. Bishop's comment on
Brouwer's view is priceless, and perhaps not well known. The lecture will use Bishop's
written remark as motivation and then discuss how we are implementing elements of
intuitionistic mathematics in Nuprl.
We consider a setting where players belong to two types
(men and women, vegetarians and carnivores, junior and senior researchers)
and need to split into groups, with each player having preferences
over the proportion of the two player types in his or her group.
We study the problem of finding a stable partition, for several
game-theoretic notions of stability; while some of the problems
we consider turn out to be polynomial-time solvable, others are NP-hard,
in which case we also explore their parameterized complexity.
In many countries, junior doctors are assigned to hospitals via a centralised
matching process. Algorithms take as input the preferences of doctors over
hospitals and vice versa, and the upper quotas of hospitals (these are the
numbers of doctors that each hospital has room for). The algorithms typically
produce stable matchings of doctors to hospitals, which guarantee that no
doctor and hospital would rather be assigned to one another than to remain with
their existing assignee/s (if any). The underlying computational problem has
been well studied in its classical form, and fast algorithms are known for
finding stable matchings.
In this talk we focus on extensions of the classical problem of assigning
junior doctors to hospitals that are motivated by practical applications, each
of which leads to an NP-hard problem. Variants that we consider include, for
example: (i) trading off size with stability, where we seek larger matchings
that minimise instability; (ii) allowing ties in the preference lists; (iii)
allowing couples to apply jointly to pairs of hospitals that are typically
geographically close; (iv) allowing hospitals to have lower quotas as well as
upper quotas. In each case we motivate and define the problem, survey existing
algorithmic results and outline some open cases.
I will talk about perfect information zero-sum games played on graphs, which
are ubiquitous in formal verification of reactive systems. For instance,
solving (i.e., determining the winner of) parity games is equivalent to model
checking for modal μ-calculus formulae, which in turn subsumes both LTL and CTL
specifications. Let’s ignore for now that the complexity of solving Parity
games remains unknown and instead be greedy and look into more expressive types
Moving from finite graphs to infinite ones and introducing randomization allows
to study interesting interplay between the structure of the graphs, the
complexities of winning strategies, and the decidability/complexity of game
It turns out that many interesting generalizations effectively reduce to
solving so-called energy games, in which one of the two players simply wants to
keep a discrete “energy” level nonnegative. In this talk I will recall
historical and recent results on such games played on infinite graphs and point
to open problems in the area.
A hole in a graph is a chordless cycle of length at least 4. A theta is a graph
formed by three internally vertex-disjoint paths of length at least 2 between
the same pair of distinct vertices. A wheel is a graph formed by a hole and a
node that has at least 3 neighbors in the hole. In joint work with Trotignon
and Radovanović we obtain a decomposition theorem for the class of graphs that
do not contain as an induced subgraph a theta nor a wheel, using clique cutsets
and 2-joins. In this talk we show how this decomposition theorem can be used to
solve the induced disjoints paths and related problems on this class.