(Apologies if you receive multiple copies of this announcement)
BCS-FACS Evening Seminar
Using Temporal Logic to Analyse Temporal Logic:
A Hierarchical Approach Based on Intervals
Dr Ben Moszkowski
De Montfort University
>>> 4 June 2007 <<<
5.45pm
BCS London Offices
First Floor
The Davidson Building
5 Southampton Street
London WC2E 7HA
Temporal logic has been extensively utilized in academia and industry to
formally specify and verify behavioural properties of numerous kinds of
hardware and software. We present a novel way to apply temporal logic to
the study of a version of itself, namely, propositional linear-time temporal
logic (PTL). This involves a hierarchical framework for obtaining standard
results for PTL, including a small model property, decision procedures and
axiomatic completeness. A large number of the steps involved are expressed
in a propositional version of Interval Temporal Logic (ITL) which is
referred to as PITL. It is a natural generalization of PTL and includes
operators for reasoning about periods of time and sequential composition.
Versions of PTL with finite time and infinite time are both considered and
one benefit of the framework is the ability to systematically reduce
infinite-time reasoning to finite-time reasoning. The treatment of PTL with
the operator Until and past time naturally reduces to that for PTL without
either one. The interval-oriented methodology differs from other analyses
of PTL which typically use sets of formulas and sequences of such sets for
canonical models. Instead we represent models as time intervals expressible
in PITL. The analysis furthermore relates larger intervals with smaller
ones. Being an interval-based formalism, PITL is well suited for
sequentially combining and decomposing the relevant formulas. Consequently,
we can articulate issues of equal significance in more conventional analyses
of PTL but normally only considered at the metalevel. A good example of
this is the existence of bounded models with periodic suffixes for PTL
formulas which are satisfiable in infinite time. We also describe decision
procedures based on binary decision diagrams and exploit some links with
finite-state automata.
Beyond the specific issues involving PTL, the research is a significant
application of ITL and interval-based reasoning and illustrates a general
approach to formally reasoning about sequential and parallel behaviour in
discrete linear time. The work also includes some interesting
representation theorems. In addition, it has relevance to hardware
description and verification since the specification languages PSL/Sugar
(IEEE Standard 1850) and 'temporal e' (part of IEEE Standard 1647) both
contain temporal constructs concerning intervals of time as does the related
SystemVerilog Assertion language contained in SystemVerilog (IEEE Standard
1800), an extension of the IEEE 1364-2001 Verilog language.
Refreshments will be served from 5.15pm
The seminar is free of charge and open to everyone. If you would like to
attend, please email Paul Boca [ [log in to unmask]] by
>>> 2 June 2007 <<<. Pre-registration is required, as security at the BCS
Offices is tight.
Directions on how to get to venue:
http://www.epsg.org.uk/locations/bcsss-guide.html
BCS-FACS website:
http://www.bcs-facs.org
Evening Seminars:
http://www.bcs-facs.org/events
|