Resolution Based Theorem Proving for Temporal Logics of Knowledge and Belief with Interactions-Final Report Summary

Background/Context

The project involved the development of proof methods for combined temporal and modal logics which are useful for specifying and verifying complex systems such as multi-agent systems, security protocols and knowledge games. In particular, the focus of the project was on developing proof methods for the combination of propositional linear-time temporal logic with the modal logic S5 to represent knowledge, and allowing interaction between the modal and temporal components.

Work on temporal logic and verification is widespread, both within the UK and internationally. The work of this project is well known internationally, and members of the research team have been centrally involved in the development of the field of temporal logic during the period of this project. For example, Clare Dixon was local organisation co-chair in 2002 of the TIME International Symposium of Temporal Representation and Reasoning, the only regular international event concerning temporal reasoning. Clare was one of four editors of a Special Issue on Temporal Representation and Reasoning of the Annals of Mathematics and Artificial Intelligence journal in 2001 [2] and is currently co-editing a special issue of the Journal of Logic and Computation related to time in Computer Science, Artificial Intelligence and Databases.

Key Advances and Supporting Methodology

In the following sections, we outline the key advances made in areas relating to the project.

The Development of Resolution Methods for Temporal Logics of Knowledge with Interactions

Work was focused on interactions concerning synchrony and perfect recall, and synchrony and no learning (see for example [17]), which can be axiomatised by the usual axioms of temporal logic, the modal logics of knowledge and the axioms KOφ ⇒ OKφ or OKφ ⇒ KOφ respectively. It was noticed that these axioms correspond closely with particular clauses of the normal form for temporal logics of knowledge. Rather than developing special resolution rules to account for the axioms we applied the axioms directly to clauses in the normal form. Rather than allow a normal form that referred to both temporal and modal operators in a single clause, renaming was carried out to keep the temporal and modal components separate. This led to resolution methods for temporal logics of knowledge with synchrony and perfect recall or synchrony and no learning and associated soundness and completeness results [3,5,24]. Using these results, we considered how to generate resolution proof methods for interactions of the form KO^mφ ⇒ OⁿKφ or O^mKφ ⇒ KOⁿφ [23] (where Oⁱ denotes i next operators).

The Development of Tableaux Methods for Temporal Logics of Knowledge with Interactions

Having devised resolution methods for temporal logics of knowledge with interactions relating to synchrony it seemed natural to investigate other proof methods. Tableaux based methods involve attempting to construct a structure from which a model for the input formula can be generated. If no such structure can be constructed then the input formula is unsatisfiable otherwise the input formula is satisfiable. The grid like structure of these logics complicate the development of such methods. Related to the work on the resolution methods for these logics, we translated the input formulae to a normal form similar to that used in [8]. The axioms relating to the required interaction are then applied directly to formulae in the normal form. The tableau construction then follows that for tableau for temporal logics of knowledge without interaction. The correctness proofs involve showing that from the generated structure we really can build a model of the required form [9,10].

The Development of Resolution Methods for Combinations of Temporal and Modal Logics

Dealing with combinations of logics is an area of interest for many researchers. In [1] the issues relating to combining logics are discussed. This paper arose from the contributions during a panel session on this topic at the annual UK Automated Reasoning Workshop.

Prior to the commencement of the project we developed resolution methods for the fusion of propositional linear-time temporal logics with the modal logic S5 for knowledge [8]. This concentrated on the single modal case. This was extended to the multi-modal case in [4].

We have also developed resolution based proof methods for different combinations of temporal and modal logics. the fusion between the branching-time temporal logic CTL and the modal logic KD45 representing belief [6,7]. From the development of resolution methods for these particular combinations we have devised resolution rules for combinations of any normal modal logic with propositional-linear time temporal logics [23]. In an alternative approach to this problem we used a translation to a fragment of first order classical logic for the modal part whilst retaining the temporal clauses in their original form to provide a resolution based decision procedure for the fusion of any normal modal logic with propositional-linear time temporal logic [18].

Efficient Temporal Reasoning

In [11] we present the temporal resolution method and associated correctness proofs for propositional linear-time temporal logic. Whilst this method is complete, more work needed to be done to try apply the resolution rules in a more efficient way and develop relevant strategies to guide the proof.

Initially a set of support strategy was defined for normal form clauses without eventuality operators [13]. This was essentially an extension of the set of support strategy for classical propositional logic. Its extension to the full logic (i.e. allowing eventuality clauses) was not obvious.

The temporal resolution method defined in [11] included a complex temporal resolution rule. To apply this rule, an external, non-resolution based procedure call is required to derive the sets of clauses to which this rule may be applied. To take the place of this procedure call we developed algorithms to generate formulae with which to apply the complex temporal resolution rule by repeatedly applying the (less complex) step resolution rule. This algorithm has been described in [14, 15, 16]. These algorithms have the advantage that they allow the reuse of previously derived clauses for subsequent applications of the temporal resolution rule to the same eventuality. This algorithm has been used to define a set of support strategy for the full propositional linear-time temporal logic [14].

Implementation

A prototype system in Prolog has been developed for the basic system of temporal logics of knowledge (without interactions) and allowing the synchrony and no learning interaction [23].

Similarly a prototype using the algorithms to apply the temporal resolution rule has been developed in Prolog [14]. These have been used to evaluate the proof methods experimentally on examples.

Whilst both these systems have been useful for initial experiments we expect that in the longer term extending the TRP++ program [21], an implementation of temporal resolution for propositional linear-time temporal logics in C++ developed as part of the EPSRC funded project GR/L87491, would be a more robust solution.

Applications

KARO is an agent specification language using a complex combination of dynamic logic and modal logics with several non-standard operators. In collaboration with the KARO developers we considered proof methods for KARO by defining a core of this complex language and using one of two methods [22,19,20]. The first involves a translation into a combination of the branching-time temporal logic (CTL) with knowledge or belief. The second requires direct translation into first-order classical logic. Whilst the core of KARO doesn't allow interactions, interactions analogous to synchrony and perfect recall and synchrony and no learning are required for the full KARO logic.

Recently we have been attempting to specify and verify properties of security protocols using combinations of temporal and modal logics. In [12] we specified a simple security protocol using temporal logics of knowledge and were able to prove properties of the protocol. A similar study of the Needham Schroeder Protocol is being carried out.

Research Impact

The work carried out in this project provided significant advances in a number of areas of temporal logic research, namely

The development of sound, complete and terminating resolution based proof procedures for temporal logics of knowledge with the interactions synchrony and perfect recall or synchrony and no learning [3,5,24].
The development of sound, complete and terminating tableaux based proof procedures for temporal logics of knowledge with the interactions synchrony and perfect recall or synchrony and no learning [9,10].
The development of sound, complete and terminating resolution based proof procedures for propositional linear time logics combined with normal modal logics [18, 23] and the branching-time temporal logic CTL combined with the modal logic KD45 representing belief [6,7].
Efficient algorithms for applying the temporal resolution rule for propositional linear-time temporal logics and the definition of a set of support for temporal resolution [14, 15,16]
An investigation into the agent based specification language KARO and development of proof methods for a core of its features [19,20,22].
Prototype implementations of resolution for temporal logics of knowledge with interactions [23], new algorithms for applying the temporal resolution rule and set of support strategy for temporal resolution [14].

References

1

B. Bennett, C. Dixon, M. Fisher, E. Franconi, I. Horrocks, U. Hustadt, and M. de Rijke.
Combinations of Modal Logics .
Artificial Intelligence Review, 17(1):1--20, March 2002.

2

C. Dixon, M. Finger, M. Fisher, and M. Reynolds, editors.
Special Issue on Temporal Representation and Reasoning, volume 30 of Annals of Mathematics and Artificial Intelligence.
Kluwer, 2001.

3

C. Dixon and M. Fisher.
Clausal Resolution for Logics of Time and Knowledge with Synchrony and Perfect Recall .
In H. Wansing and F. Wolter, editors, Proceedings of ICTL-00 the Third International Conference on Temporal Logic, Leipzig, Germany, October 2000.

4

C. Dixon and M. Fisher.
Resolution-Based Proof for Multi-Modal Temporal Logics of Knowledge .
In S. Goodwin and A. Trudel, editors, Proceedings of TIME-00 the Seventh International Workshop on Temporal Representation and Reasoning, Cape Breton, Nova Scotia, Canada, July 2000. IEEE Press.

5

C. Dixon and M. Fisher.
Clausal Resolution for Logics of Time and Knowledge with the Interaction Synchrony and Perfect Recall .
(Under journal review) , 2002.

6

C. Dixon, M. Fisher, and A. Bolotov.
Resolution in a Logic of Rational Agency .
In 14th European Conference on Artificial Intelligence (ECAI 2000), pages 358--362, Berlin, Germany, August 2000. IOS Press.

7

C. Dixon, M. Fisher, and A. Bolotov.
Clausal Resolution in a Logic of Rational Agency .
Artificial Intelligence, 139(1):47--89, July 2002.

8

C. Dixon, M. Fisher, and M. Wooldridge.
Resolution for Temporal Logics of Knowledge.
Journal of Logic and Computation, 8(3):345--372, 1998.

9

C. Dixon, C. Nalon, and M. Fisher.
Tableaux for Logics of Time and Knowledge with Interactions Relating to Synchrony .
(In preparation) , 2003.

10

C. Dixon, C. Nalon, and M. Fisher.
Tableaux for Temporal Logics of Knowledge: Synchronous Systems of Perfect Recall or No Learning .
In M. Reynolds and A. Sattar, editors, Proceedings of the Tenth International Symposium on Temporal Representation and Reasoning and the Fourth International Conference on Temporal Logic (TIME-ICTL 2003), Cairns, Australia, July 2003. IEEE Computer Society Press.

11

M. Fisher, C. Dixon, and M. Peim.
Clausal Temporal Resolution .
ACM Transactions on Computational Logic, 2(1):12--56, January 2001.

12

M. Fisher, W. van der Hoek, M.C. Fernández Gago, and C. Dixon.
Specifying and Verifying Security Protocols .
(Internal technical note) , 2003.

13

M.C. Fernández Gago.
Efficient control of temporal reasoning.
Transfer Report, Manchester Metropolitan University, 2000.

14

M.C. Fernández Gago.
Efficient Control of Temporal Reasoning.
PhD thesis, Department of Computer Science, University of Liverpool, 2003.
In preparation.

15

M.C. Fernández Gago, M. Fisher, and C.Dixon.
Algorithms for Guiding Clausal Temporal Resolution .
In Proceedings of 25th German Conference on Artificial Intelligence (KI-2002), Lecture Notes in Artificial Intelligence, Aachen, Germany, September 2002. Springer.

16

M.C. Fernández Gago, M. Fisher, and C. Dixon.
An Algorithm for Guiding Clausal Temporal Resolution .
In Proceedings of 4th International Workshop on Strategies in Automated Deduction (STRATEGIES 2001) , Siena, Italy, June 2001.
Held in conjunction with IJCAR.

17

J. Y. Halpern and M. Y. Vardi.
The Complexity of Reasoning about Knowledge and Time. I Lower Bounds.
Journal of Computer and System Sciences, 38:195--237, 1989.

18

U. Hustadt, C. Dixon, R. A. Schmidt, and M. Fisher.
Normal Forms and Proofs in Combined Modal and Temporal Logics .
In Proceedings of the Third International Workshop on Frontiers of Combining Systems (FroCoS'2000), volume 1794 of LNAI. Springer, 2000.

19

U. Hustadt, C. Dixon, R. A. Schmidt, M. Fisher, J.-J. Meyer, and W. van der Hoek.
Reasoning about agents in the KARO framework.
In C. Bettini and A. Montanari, editors, Proceedings of the Eighth International Symposium on Temporal Representation and Reasoning (TIME-01), pages 206--213, Cividale del Friuli, Italy, June 2001. IEEE Press.

20

U. Hustadt, C. Dixon, R. A. Schmidt, M. Fisher, J.-J. Meyer, and W. van der Hoek.
Verification Within the KARO Agent Theory .
In Selected Papers from the first Goddard Workshop on Formal Approaches to Agent-Based Systems (FAABS). Kluwer Academic Publishers, 2001.

21

U. Hustadt and B. Konev.
TRP++: A Temporal Resolution Prover .
In Proceedings of 3rd International Workshop on the Implementation of Logics, Tbilisi, Georgia, October 2002.

22

Ullrich Hustadt, C. Dixon, R. A. Schmidt, M. Fisher, J.-J. C. Meyer, and W. van der Hoek.
Verification within the KARO agent theory.
In J. L. Rash, C. A. Rouff, W. Truszkowski, D. Gordon, and M. G. Hinchey, editors, Proceedings of the First International Workshop on Formal Approaches to Agent-Based Systems (FAABS 2000), volume 1871 of LNAI, pages 33--47. Springer, 2001.

23

C. Nalon.
Resolution for Interacting Modal Logics.
PhD thesis, Department of Computer Science, University of Liverpool, 2003.
In preparation.

24

C. Nalon, C. Dixon, and M. Fisher.
Resolution for synchrony and no learning: Preliminary report.
In Proceedings of the 8th International Workshop on Logic Language, Information and Computation (WoLLIC'2001), 2001.