London Logic Forum: Logic day

UCL Contact: Robin Hirsch (Visitors from outside UCL please email in advance).
Date/Time: 27 Jan 17, 10:00 - 17:00
Venue: 103, Front Executive Suite, Front Engineering Building

Abstract

10am Mark Reynolds
Title: Synthesis for monadic logic over the reals
Abstract:
Propositional linear time temporal logic (LTL) is the standard temporal logic for computing applications and many reasoning techniques and tools have been developed for it. Tableaux for deciding satisfiability have existed since the 1980s. However, the tableaux for this logic do not look like traditional tree-shaped tableau systems and their processing is often quite complicated.

In this talk, we introduce a novel style of tableau rule
which supports a new simple traditional-style tree-shaped tableau for LTL. We prove that it is sound and complete. As well as being simple to understand, to introduce to students and to use, it is also simple to implement and is competitive against state of the art systems. It is particularly suitable for parallel implementations.

11.30am
Axiomatising Domain Algebras, Szabolcs Mikulas (joint work with Marcel Jackson)

Domain algebras provide an elegant, one-sorted formalism for automated reasoning
about program and system verification. Unfortunately, in the case of the basic
signature of composition and domain, the class of relational domain algebras
is not finitely axiomatizable (Hirsch-M). The proof exploits the fact that the natural
ordering is unavailable in these algebras. One remedy is to expand the signature with
and ordering - in fact we get a finitely axiomatized representation class for the signature
consisting of composition, domain, range and converse (Bredikhin, Hirsch-M).
But converse does not seem to be a natural operation from the verification point of view.
In this talk we show that for the signature consisting of compostion, domain, range and
join, the equational theory of relational domain algebras is finitely axiomatizable.

2pm Misha Zakharyashev. Survey of Horn-related fragments of various temporal logics

3.30pm Mark Reynolds. Title: A new rule for LTL tableaux
Abstract:
We say that a first-order monadic logic of order (FOMLO) sentence is satisfiable over the reals if there is some valuation for the monadic predicates which makes the formula true. Burgess and Gurevich showed that satisfiability for this logic is decidable. They built on pioneering work by Lauchli and Leonard who, in showing a similar result for linear orders in general, had presented some basic operations for the compositional building of monadic linear structures.

We look at some recent work in using these basic operations to give a synthesis result. That is, we present an algorithm which given a FOMLO sentence which is satisfiable over the reals, outputs a specific finite description of a model.