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
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 |
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.
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. |