Analysis and Mechanisation of Decidable First-Order Temporal Logics

Research Team

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:

  1. to develop practical proof algorithms, based on decidable (extensions of) monodic FOTL, using both tableau and resolution techniques;
  2. to carry out a detailed analysis of logical and computational properties of monodic FOTL;
  3. to extend current results concerning axiomatisable and decidable classes beyond the monodic case;
  4. to implement some of the tableau/resolution systems developed in (1); and
  5. 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:

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.