The Scottish Theorem Proving seminar series

[This is a copy of the page at http://www.cee.hw.ac.uk/~julianr/stp.html.]

Friday 15th December 2000

Dependable Systems Group, 
Department of Computing and Electrical Engineering,
Heriot-Watt University.

The next meeting in the Scottish Theorem Proving series will be held in the
Department of Computing and Electrical Engineering,
Heriot-Watt University.

We are pleased to announce the following talks:

On a Symbolic Semantics, Bisimulation and Modal Logic for Full LOTOS.

   Muffy Calder, Glasgow University

A PVS-assisted proof of adequacy of a modal logic for Full LOTOS:
Is Formal Proof a help or a hindrance?

   Savi Maharaj, University of Stirling

Focus games: satisfiability checking for temporal logic

   Colin Stirling, University of Edinburgh
 

Time: 2pm-5pm

Venue:

Room 1.82,
Department of computing and Electrical Engineering,
Mountbatten Building, Heriot-Watt University,
Riccarton, Edinburgh.

How to get here.

Programme:

14:00: Welcome
14:10-14:40: "On a Symbolic Semantics, Bisimulation and Modal Logic for Full LOTOS." 
 Muffy Calder, Glasgow University
14:50-15:20: "A PVS-assisted proof of adequacy of a modal logic for Full LOTOS:
 Is Formal Proof a help or a hindrance?"
 Savi Maharaj, University of Stirling 
15:30: Coffee and Tea
16:00-16:30: "Focus games: satisfiability checking for temporal logic."
 Colin Stirling, University of Edinburgh
16:40 Close

Abstracts:

"On a Symbolic Semantics, Bisimulation and Modal Logic for Full LOTOS."

Muffy Calder, Glasgow University

Although LOTOS has been in force for nearly 15 years, there are still a number of outstanding foundational problems which have practical implications.  The problems concern the treatment of data: the data is "hardwired" into transitions to enable an easy treatment of multi-way synchronisation.  This means that most transtition systems are infinite in breadth (and possibly in depth) and therefore not amenable to model-checking without restrictions.  To overcome this problem, we have defined a "symbolic" semantics and various notions of bisimulation, algorithms and modal logics. These will be outlined in the talk, along with selected highlights (and pitfalls) of this programme of work.

"A PVS-assisted proof of adequacy of a modal logic for Full LOTOS: Is Formal Proof a help or a hindrance?"

Savi Maharaj, University of Stirling

This talk presents a specific piece of work within the framework of research described by Muffy Calder. One goal of this project is to develop a logic for reasoning about LOTOS processes. The logic must be "adequate" with respect to bisimulation, in the sense that bisimilar LOTOS processes should have the same logical properties. There are many choices to be made in the design of such a logic, and many cases to consider in proving adequacy. We therefore thought that a theorem proving tool would be helpful to keep track of the book-keeping involved in developing the proof.

My remit, on joining this project, was to use the PVS theorem prover to carry out this proof. I shall describe what this involved and discuss how the use of formal proof was both a help and a hindrance.


Focus games: satisfiability checking for temporal logic

Colin Stirling, University of Edinburgh

I will talk about some recent work with Martin Lange, which uses games for understanding satisfiability of temporal logics.

When temporal logics began to be used in Computer Science, satisfiability checking was based on tableaux. However satisfiability for each variant or extension of a temporal logic then required a new hand crafted tableau decision procedure. Often these methods were far from optimal. This prompted the use of automata for deciding satisfiability of temporal formulas. Buchi or Rabin tree automata offer a very useful finite characterisation of the "infinite'' models of a temporal formula.

However decision procedures for satisfiability based on automata do not fit so well with the issue of finding a sound and complete axiomatisation of a temporal logic. Instead one tries to craft a model out of consistent sets of formulas.

Instead we propose a new basis for satisfiability of temporal logics using two player games, which employ a novel "focus'' feature. We show that there are very simple focus games for LTL (linear time temporal logic) and CTL (computation tree logic). In both these cases there is a  straightforward method for "reading off'' a complete axiom system for the logics.
 


Contact Julian Richardson for any information. julianr@cee.hw.ac.uk
 

Return to Scottish Theorem Proving page.