Analysis and Mechanisation of Decidable First-Order
Temporal Logics
Research Team
Principal Investigators:
Co-Investigators:
- Anatoli Degtyarev,
Department of Computer Science, King's College,
London WC2R 2LS
- Clare Dixon,
Department of Computer
Science, University of Liverpool
- Dov Gabbay,
Department of Computer Science, King's College,
London WC2R 2LS
- Ullrich Hustadt,
Department of Computer
Science, University of Liverpool
- Ian Hodkinson,
Department of Computing, Imperial College,
London SW7 2BZ
- Frank Wolter
Department of Computer
Science, University of Liverpool
Research Staff:
- Ulle Endriss,
Department of Computer Science, King's College,
London WC2R 2LS
- David Gabelaia,
Department of Computer Science, King's College,
London WC2R 2LS
- Boris Konev,
Department of Computer
Science, University of Liverpool
- Roman Kontchakov,
Department of Computer Science, King's College,
London WC2R 2LS
Aims and Objectives
The long-term aim of our work is to develop sophisticated temporal
verification tools that can be widely applied.
In this project we will investigate FOTL in depth, and develop, implement,
and analyse tools mechanising the axiomatisable and decidable fragments of
FOTL identified. We believe this approach represents a sound,
necessary, and feasible step towards our ultimate goal.
Our principal objectives for this proposed research programme are:
- to develop practical proof algorithms, based on decidable
(extensions of) monodic FOTL, using both tableau and
resolution techniques;
- to carry out a detailed analysis of logical and
computational properties of monodic FOTL;
- to extend current results concerning axiomatisable and decidable
classes beyond the monodic case;
- to implement some of the tableau/resolution systems developed in
(1); and
- to evaluate the systems developed, and to apply them to a range of
verification case studies.
Background
It is widely believed in computer science (CS) and artificial
intelligence (AI) that if first-order temporal logic (FOTL) were not
so impregnable, it could provide elegant solutions to fundamental
long-standing problems in many practically important fields. Areas
where FOTL may be exploited, and where propositional temporal logic
(PTL) has already made significant impact, include:
- specification and verification of reactive (e.g. distributed or
concurrent) systems [20] - FOTL
allows extension of these techniques to both data dependent
systems and hybrid systems [15];
- synthesis of programs from temporal specifications
[24,18] - FOTL again allows the
synthesis technique to be extended to more complex
specifications;
- semantics of executable temporal logic
[11,12] - FOTL provides not
only more expressive tools for formalising the behaviour of
executable temporal logics, but can itself be used as a more
powerful programming notation;
- model-checking [17,8] - FOTL provides
the possibility of extending model checking techniques to non
finite-state systems, and to systems containing multiple
concurrent processes;
- knowledge representation and reasoning
[9,5,29] - FOTL
allows the extension of techniques for reasoning about
knowledge to more dynamic and powerful classes.
In addition to current applications of temporal logic that would be
enhanced by the use of first-order techniques, there are several novel
applications that may become feasible via such extensions. For
example, query languages for temporal databases are often based on
(variants of) FOTL [7]. In turn, FOTL could
provide a means for temporal constraint checking [6] and
for verifying properties of transaction protocols (or business models)
in e-commerce [2,25].
As the above enhanced and potential application areas are themselves
increasingly important in both mainstream CS and AI, the development
of appropriate reasoning systems for FOTL will ultimately contribute
to many strands within these disciplines.
Unfortunately, while FOTL is clearly useful, it is a very expressive
language with extremely high computational complexity. Many varieties
of FOTL are not even recursively enumerable
[1,3,13,22,26],
and so do not admit finite proof methods at all. As a consequence,
in-depth investigations of FOTL have been rare, with attention largely
focused on developing practical tools based only on PTL. The few
either recursively enumerable or decidable fragments of FOTL that have
been found either use non-standard time-lines [3],
weaker versions of validity [1], minimal interaction
between quantifiers and temporal
operators [21,6,25] or very restricted
first-order features [23,22]. In each of these
cases, either the logic is so restricted that it represents only a
small extension of PTL, or the logical calculus described is very
difficult to implement in practice.
However, within the past year, this situation has started to
change. In a seminal paper, Hodkinson, Wolter, and
Zakharyaschev [16] introduced a new natural monodic
fragment of FOTL (where formulas beginning with a temporal operator
contain at most one free variable) and showed that it is quite
expressive and yet computationally manageable.
The whole monodic
fragment can be represented as a finite axiomatic system
[30], and so in principle can be supported by
tableau or resolution-type reasoning machinery. Moreover, by
restricting the pure first-order part to certain decidable fragments,
we obtain decidable monodic fragments of FOTL over various
flows of time - for example, the monodic guarded or even loosely
guarded fragments [4,27,14].
These recent research results have opened up
new and exciting opportunities for identifying, extending and
mechanising relatively expressive subsets of FOTL
In particular, certain similarities between monodic FOTL and
effective multi-dimensional knowledge representation formalisms
described in [28] suggest that the
monodic FOTL can be considerably extended. Although
[16,30] establish strict boundaries beyond which
fragments of FOTL again become non-enumerable, there is still scope
for enriching the expressive power of the monodic fragment. For
example, we may allow applications of local temporal operators,
such as `next-time', to formulas with two or more free variables -
formulas of this form are not only particularly welcome in temporal
databases, but also cover the decidable fragments of FOTL developed by
Pliuskevicius [23].
As regards mechanisation, recent papers
[19] present tableau-based satisfiability
checking algorithms for description logics with temporal and epistemic
operators. Again, similarities between such logics and monodic FOTL
suggest that tableau-based reasoning systems can also be constructed
for decidable monodic fragments of FOTL. Moreover, [19]
shows that this can be carried out in a modular way by
combining existing tableau systems for PTL and the classical
first-order components. In addition, we intend to develop
an alternative approach to modular proof-search in FOTL based on the
resolution method, which is more amenable
to automated reasoning in classical first-order logic than
tableau. As most of the known decidable fragments of first-order
classical logic are supported by resolution decision
procedures [10], a modular style
resolution-based decision method for FOTL immediately gains access to
all the benefits, both theoretical and practical, of resolution-based
decision methods for fragments of classical first-order logic.
The development of two different approaches to mechanisation will not
only generate further analysis of the monodic fragment, but will
provide alternative tools for practical applications.
Thus, the aim of this project is to analyse, in depth, monodic FOTL
and its decidable extensions, and to develop, implement and apply
methods of automated deduction for the constructed temporal
formalisms. Thus, this project will combine work on logical and
computational properties of well-behaved fragments of FOTL (Gabbay,
Hodkinson, Kurucz, Zakharyaschev) with work on the theory,
implementation and application of temporal verification methods
(Degtyarev, Dixon, Fisher). It will extend and enhance both areas. The
new work on monodic fragments of FOTL has opened up a range of
important opportunities and it is our aim to follow these up as soon
as possible, providing significant advances in the area of temporal
verification.
The work comprising this project constitutes a natural and feasible
extension to our ongoing work and brings together two of the world's
foremost research teams. In addition, this project complements the
ongoing EPSRC project on ``Mechanising First-Order Temporal
Logic'' (GR/M46631), being carried out between Liverpool (Fisher,
Quigley) and Edinburgh (Smaill, Bundy), which is tackling the
undecidable/non-enumerable parts of FOTL using inductive proof
techniques and proof planning.
References
-
- 1
-
Martin Abadi.
The power of temporal proofs.
Theoretical Computer Science, 64:35-84, 1989.
- 2
-
S. Abiteboul, V. Vianu, B. Fordham, and Y. Yesha.
Relational transducers for electronic commerce.
In PODS'98, pp.179-187, ACM Press, 1998.
- 3
-
H. Andréka, I. Németi, and I. Sain.
Completeness problems in verification of programs and program
schemes.
In Mathematical Foundations of Computer Science.
LNCS 74. Springer, 1979.
- 4
-
H. Andréka, I. Németi, and J. van Benthem.
Modal languages and bounded fragments of predicate logic.
J. of Philosophical Logic, 27:217-274, 1998.
- 5
-
A. Artale and E. Franconi.
Temporal description logics.
In
Handbook of Time and Temporal Reasoning in
Artificial Intelligence. MIT Press, to appear.
- 6
-
J. Chomicki.
Efficient checking of temporal integrity constraints using
bounded history encoding.
ACM Transactions on Database Systems, 20(2):149-186,
1995.
- 7
-
J. Chomicki and D. Toman.
Temporal logics in information systems.
In
Logics for Database and
Information Systems. Kluwer, 1998.
- 8
-
E. Clarke, O. Grumberg and D. A. Peled.
Model Checking.
MIT Press, 2000.
- 9
-
R. Fagin, J. Halpern, Y. Moses, and M. Vardi.
Reasoning About Knowledge.
MIT Press, 1996.
- 10
-
C. Fermüller, A. Leitsch, U. Hustadt, and T. Tammet.
Resolution Decision Procedures.
In
Handbook of Automated Reasoning.
Elsevier Science. To appear.
- 11
-
M. Fisher.
An introduction to executable temporal logics.
Knowledge Engineering Review, 11:43-56, 1996.
- 12
-
M. Fisher.
A temporal semantics for concurrent MetateM.
J. Symbolic Computation, 22(5/6):627-648,
1996.
- 13
-
D. Gabbay, I. Hodkinson, and M. Reynolds.
Temporal Logic. Part I.
Clarendon Press, Oxford, 1994.
- 14
-
E. Grädel.
Decision procedures for guarded logics.
In CADE'99, vol.1632 of
LNAI, pp.31-51, Springer, 1999.
- 15
-
T. Henzinger, P.-H. Ho and H. Wong-Toi.
HyTech: a model checker for hybrid systems.
Software Tools for Technology Transfer, 1(1):110-122,
Springer, 1997.
- 16
-
I. Hodkinson, F. Wolter, and M. Zakharyaschev.
Decidable fragments of first-order temporal logics.
Annals of Pure and Applied Logic, 106:85-134, 2000.
- 17
-
G.J. Holzmann.
Design and Validation of Computer Protocols.
Prentice Hall, New Jersey, 1991.
- 18
-
O. Kupferman and M. Vardi.
Synthesis with incomplete informatio.
In Advances in Temporal Logic. pp.109-128. Kluwer,
2000.
- 19
-
C. Lutz, H. Sturm, F. Wolter, and M. Zakharyaschev.
A tableau decision procedure for modalized ALC with
constant domains.
Submitted, 2000.
- 20
-
Z. Manna and A. Pnueli.
The Temporal Logic of Reactive and Concurrent Systems:
Specification.
Springer, 1992.
- 21
-
Z. Manna and the STeP group.
Step: Deductive-algorithmic verification of reactive and real-time
systems.
In CAV'96, vol.1102 of LNCS.
Springer, 1996.
- 22
-
S. Merz.
Decidability and incompleteness results for first-order temporal
logics of linear time.
J. Applied Non-classical Logic, 2:139-156,
1992.
- 23
-
R. Pliuskevicius.
On the completeness and decidability of a restricted first-order
linear temporal logic.
In LNCS 1289, pp.241-254. Springer, 1997.
- 24
-
A. Pnueli and R. Rosner.
On the synthesis of a reactive module.
In Proc. 16th ACM Symp. Princip.
Prog. Lang., pp.179-190, 1989.
- 25
-
M. Spielmann.
Verification of relational transducers for electronic commerce.
In PODS'2000, pp.92-103, ACM, 2000.
- 26
-
A. Szalas and L. Holenderski.
Incompleteness of first-order temporal logic with
Until.
Theoretical Computer Science, 57:317-325, 1988.
- 27
-
J. van Benthem.
Dynamic bits and pieces.
Technical Report LP-97-01, ILLC, University of Amsterdam, 1997.
- 28
-
F. Wolter and M. Zakharyaschev.
Modal description logics: modalizing roles.
Fundamenta Informaticae, 39:411-438, 1999.
- 29
-
F. Wolter and M. Zakharyaschev.
Temporalizing description logics.
In
Frontiers of Combining Systems II, pp.379-401.
Research Studies Press LTD, England, 2000.
- 30
-
F. Wolter and M. Zakharyaschev.
Axiomatizing the monodic fragment of first-order temporal logic.
Submitted, 2000.