The sixteenth meeting of the Wessex Theory Seminar took place at Imperial College London on August 29th 2012. It was a farewell workshop for Dirk Pattinson and Tadeusz Litak.

The talks were held in room 213 (Clore Lecture Theatre), Department of Computing, Imperial College London, 180 Queen's Gate, London SW7 2RH.

11:00 - 11:45 **Lutz Schroeder** (Friedrich-Alexander-Universität Erlangen-Nürnberg), Coalgebraic logic and self-reference

11:45 - 12:30 **Alexandra Silva** (Radboud University Nijmegen), Brzozowski's algorithm, (co)algebraically

12:30 - 13:45 lunch break

13:45 - 14:30 **James Brotherston** (University College London), Cyclic abduction of inductive termination preconditions

14:30 - 15:15 **Peter Hancock** (University of Strathclyde), On stuttering equivalence

15:15 - 16:00 **Frank Wolter** (University of Liverpool), Ontology-based data access and CSP: towards a link between modal logic and constraint satisfaction

16:00 - 16:30 coffee break

16:30 - 17:15 **Rasmus Mogelberg** (IT University of Copenhagen), The topos of trees as a model of guarded recursion

17:15 - 18:00 **Christian Urban** (Kings College London), The Myhill-Nerode Theorem in a Theorem Prover

Decidability of modal logics tends to break down quickly when features for self-reference are added,

such as the down-arrow binder of hybrid logic, or its single-variable version popularized by Marx as the I-me construct.

We have shown in earlier work that decidability (and in fact low complexity) of logics with I-me is regained if the number

of modal operators between between each use of me and its enclosing I is bounded by two. In the case of the description

logic ALCQ, the corresponding extension by depth-2 I-me turns out to be equivalent to the addition of a number of well-known

features: inverses, role hierarchies, safe boolean role combinations, and sROIQ's self-loop construct. Here, we report on

ongoing work aimed at a coalgebraic generalization of the algorithmic principles involved.

We give a new presentation of Brzozowski's algorithm to minimize

finite automata,

using elementary facts from universal algebra and coalgebra,

and building on earlier work by Arbib and Manes on the duality

between reachability and observability.

This leads to a simple proof of its correctness and opens the door to

further generalizations. Notably, we derive algorithms to minimize

Moore, non-deterministic and weighted automata.

Going all the way back to Alan Turing, people have asked the

question "does this program ever terminate?". In this talk, I want

to go further and ask "can we find a reasonable precondition under

which this program terminates?". When one considers

heap-manipulating programs, this problem - which is one of

**abduction**, or synthesis - typically involves inventing the

inductive definitions of data structures. For example, a program

that traverses a list will terminate given a heap structured as an

acyclic list as input. But given a cyclic list, it will fail to

terminate, and given something that is not a list at all, it will

typically encounter a memory fault and crash.

Here I demonstrate a new method, called **cyclic abduction**, for

automatically inferring the inductive definitions of termination

preconditions for heap-manipulating programs. That is, given a

program, this method returns the definition of an inductively

defined predicate in separation logic under which the program is

guaranteed to terminate (without crashing). Cyclic abduction

essentially works by searching for a **cyclic proof** of termination

of the program, abducing definitional clauses of the precondition

as necessary to advance the proof search process.

We have constructed abduction proofs for a range of small programs

both by hand, and automatically, using a custom cyclic theorem

prover. The abduced predicates may define segmented, cyclic,

nested, and/or mutually defined data structures.

This is joint work with Nikos Gorogiannis (also at UCL).

The notion of stuttering equivalence, or at least the name, is due to Leslie Lamport,

and plays an important role in his version of quantified linear-time temporal logic.

Some published definitions of this notion are plain broken. It turns out that a

possible (correct) definition has the form of a nested coinductive-inductive definition, a form

that Dirk may recognise.

In recent years, the use of ontologies (=logical theories) to access instance data has become

increasingly popular. The general idea is that an ontology provides a vocabulary or conceptual

model for the application domain, which can then be used as an interface for querying instance

data and to derive additional facts.

In this presentation, I will introduce ontology-based data access for ontologies given in modal logic

(aka description logic) and investigate the following non-uniform complexity problem: what is the data

complexity of query answering for a fixed ontology? I will present general conditions under which this

problem is in PTime and, respectively, coNP-hard. Then it is shown that query answering

in modal logic is equivalent to solving constraint satisfaction problems (CSPs) with finite templates.

This result provides a very close link between modal logic and CSPs - a very active research area

combining methods from logic, graph theory, algebra, and combinatorics.

This link has numerous consequences for modal logic. For example, a P/coNP dichotomy holds for

with query answering in modal logic if, and only if, Feder and Vardi¿s dichotomy conjecture for CSPs holds.

We show how the topos of trees, i.e., the category of presheaves over the ordered

natural numbers, models guarded recursive terms, predicates and types.

We have two motivations for this work: one is as a model of

computation with coinductive types such as streams, using guards to ensure

well-definedness of recursive definitions. The other is the construction of

models of programming languages with higher-order store, which involves

solving recursive domain equations. But since guarded recursion is commonplace

in computer science we expect many more applications.

In the talk I will give a computational intuition for the topos of trees and

show how the internal logic of this model can be used as an expressive

language combining dependent types and subset types with guarded recursion.

I will also sketch how to construct a model of higher-order store entirely inside

this language, using a combination of set-like constructions and guarded recursion.

Relations to step-indexing and metric space models of guarded recursion will be discussed.

There are numerous textbooks on regular languages. Many of them focus

on finite automata for proving properties. Unfortunately, automata are

not so straightforward to formalise in theorem provers. The reason is

that natural representations for automata are graphs, matrices or

functions, none of which are inductive datatypes. Regular expressions

can be defined straightforwardly as a datatype and a corresponding

reasoning infrastructure comes for free in theorem provers. I will show

in this paper that a central result from formal language theory - the

Myhill-Nerode Theorem - can be recreated using only regular

expressions. From this theorem many closure properties of regular

languages follow.

From ANU:

- Dirk Pattinson

From Bath:

- Anupam Das
- John Power
- Cai Wingfield

From Birmingham:

- Achim Jung
- Paul Levy

From Copenhagen:

- Rasmus Mogelberg

From Erlangen:

- Lutz Schroeder

From Imperial:

- Faris Abou-Saleh
- Nick Bezhanishvili
- Fredrik Dahlqvist
- Runa Jesmin
- Andrew Jones
- Bjoern Lellman
- Florian Widmann
- Nobuko Yoshida

From King's College London:

- Christian Urban

From Leicester:

- Tadeusz Litak

From Liverpool:

- Frank Wolter

From Montreal:

- Claudio Hermida

From Nijmegen:

- Alexandra Silva

From Oxford:

- Clemens Kupke

From Queen Mary:

- Edmund Robinson

From Salzburg:

- Ana Sokolova

From Southampton:

- Corina Cirstea

From Strathclyde:

- Peter Hancock

From Sussex:

- Bernhard Reus

From University College London:

- James Brotherston

See all Wessex sites involved and meetings so far.