| Paul.Boca@googlemail.com 2007-05-30, 10:06 pm |
| (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
[color=darkred]
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 [ Paul.Boca@googlemail.com] by[color=darkred]
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
|