Clare Dixon

TCS Journal 2025 Journal Article

Monodic fragments of probabilistic first-order temporal logic with bounded semantics

• Georgios Kourtis
• Clare Dixon
• Michael Fisher

We extend (type-2) probabilistic first-order logic with temporal operators, interpreted over fixed-length initial segments of (discrete) time. Given a formula φ of the resulting logic and a natural number N, we ask: is φ satisfiable over a space of length N + 1 sequences of states (first-order structures)? We show the problem to be decidable for monodic fragments of the logic whose first-order part has a decidable satisfiability problem and we also establish the problem's computational complexity when the first-order part is among some well-known decidable fragments of first-order logic.

EUMAS Conference 2023 Conference Paper

Adaptive Cognitive Agents: Updating Action Descriptions and Plans

• Peter Stringer
• Rafael C. Cardoso 0001
• Clare Dixon
• Michael Fisher 0001
• Louise A. Dennis

Abstract In this paper we present an extension of Belief-Desire-Intention agents which can adapt their performance in response to changes in their environment. We consider situations in which the agent’s actions no longer perform as anticipated. Our agents maintain explicit descriptions of the expected behaviour of their actions, are able to track action performance, learn new action descriptions and patch affected plans at runtime. Our main contributions are the underlying theoretical mechanisms for data collection about action performance, the synthesis of new action descriptions from this data and the integration with plan reconfiguration. The mechanisms are supported by a practical implementation to validate the approach.

AAMAS Conference 2023 Conference Paper

Updating Action Descriptions and Plans for Cognitive Agents

• Peter Stringer
• Rafael C. Cardoso
• Clare Dixon
• Michael Fisher
• Louise A. Dennis

In this paper, we present an extension of Belief-Desire-Intention agents which can adapt their performance in response to changes in their environment. Our main contributions are the underlying theoretical mechanisms for data collection about action performance, the synthesis of new action descriptions from this data, the integration with plan reconfiguration, and a practical implementation to validate the semantics.

TIME Conference 2020 Conference Paper

Verifying Autonomous Robots: Challenges and Reflections (Invited Talk)

• Clare Dixon

Autonomous robots such as robot assistants, healthcare robots, industrial robots, autonomous vehicles etc. are being developed to carry out a range of tasks in different environments. The robots need to be able to act autonomously, choosing between a range of activities. They may be operating close to or in collaboration with humans, or in environments hazardous to humans where the robot is hard to reach if it malfunctions. We need to ensure that such robots are reliable, safe and trustworthy. In this talk I will discuss experiences from several projects in developing and applying verification techniques to autonomous robotic systems. In particular we consider: a robot assistant in a domestic house, a robot co-worker for a cooperative manufacturing task, multiple robot systems and robots operating in hazardous environments.

I&C Journal 2019 Journal Article

Sublogics of a branching time logic of robustness

• John McCabe-Dansted
• Clare Dixon
• Tim French
• Mark Reynolds

In this paper we study sublogics of RoCTL*, a recently proposed logic for specifying robustness. RoCTL* allows specifying robustness in terms of properties that are robust to a certain number of failures. RoCTL* is an extension of the branching time logic CTL* which in turn extends CTL by removing the requirement that temporal operators be paired with path quantifiers. In this paper we consider three sublogics of RoCTL*. We present a tableau for RoBCTL*, a bundled variant of RoCTL* that allows fairness constraints to be placed on allowable paths. We then examine two CTL-like restrictions of CTL*. Pair-RoCTL* requires a temporal operator to be paired with a path quantifier; we show that Pair-RoCTL* is as hard to reason about as the full CTL*. State-RoCTL* is restricted to State formulas, and we show that there is a linear truth preserving translation of State-RoCTL into CTL, allowing State-RoCTL to be reasoned about as efficiently as CTL.

IJCAI Conference 2017 Conference Paper

KSP: A Resolution-based Prover for Multimodal K, Abridged Report

• Cláudia Nalon
• Ullrich Hustadt
• Clare Dixon

In this paper, we briefly describe an implementation of a hyper-resolution-based calculus for the propositional basic multimodal logic, Kn. The prover, KSP, is designed to support experimentation with different combinations of refinements for its basic calculus. The prover allows for both local and global reasoning. We present an experimental evaluation that compares KSP with a range of existing reasoners for Kn.

JELIA Conference 2012 Conference Paper

Verifying Brahms Human-Robot Teamwork Models

• Richard Stocker 0001
• Louise A. Dennis
• Clare Dixon
• Michael Fisher 0001

Abstract Collaboration between robots and humans is an increasingly important aspect of industrial and scientific settings. In addition, significant effort is being put into the development of robot helpers for more general use in the workplace, at home, and in health-care environments. However, before such robots can be fully utilised, a comprehensive analysis of their safety is necessary. Formal verification techniques are regularly used to exhaustively assess system behaviour. Our aim is to apply such techniques to Brahms, a human-agent-robot modelling language. We show how to translate from Brahms scenarios, using a formal semantics for Brahms, into the input language of a model checker. We illustrate the approach by defining, translating, and verifying a domestic robot helper example.

TIME Conference 2010 Conference Paper

CTL-Like Fragments of a Temporal Logic of Robustness

• John Christopher McCabe-Dansted
• Clare Dixon

The logic RoCTL* is an extension of the branching time temporal logic CTL* to represent robustness of systems to transient failures such as loss of data packets. New operators are introduced dealing with obligation (where no failures occur) and robustness (where at most one additional failure occurs). The only known decision procedures for the temporal logic of robustness RoCTL* are non-elementary. Here we propose two CTL-like restrictions of RoCTL*, Pair-RoCTL and State-RoCTL. We investigate whether it is possible to translate these fragments into CTL showing whilst this is not in general possible for Pair-RoCTL it is for State-RoCTL. We obtain a satisfiability preserving translation for State-RoCTL into CTL showing that the complexity of satisfiability of State-RoCTL is EXPTIME-complete. We also show that these fragments of RoCTL* are useful in specifying systems.

TIME Conference 2008 Conference Paper

Practical First-Order Temporal Reasoning

• Clare Dixon
• Michael Fisher 0001
• Boris Konev
• Alexei Lisitsa 0001

In this paper we consider the specification and verification of infinite-state systems using temporal logic. In particular, we describe parameterised systems using a new variety of first-order temporal logic that is both powerful enough for this form of specification and tractable enough for practical deductive verification. Importantly, the power of the temporal language allows us to describe (and verify) asynchronous systems, communication delays and more complex liveness and fairness properties. These aspects appear difficult for many other approaches to infinite-state verification.

IJCAI Conference 2007 Conference Paper

• Clare Dixon
• Michael Fisher
• Boris Konev

Temporal reasoning is widely used within both Computer Science and A. I. However, the underlying complexity of temporal proof in discrete temporal logics has led to the use of simplified formalisms and techniques, such as temporal interval algebras or model checking. In this paper we show that tractable sub-classes of propositional linear temporal logic can be developed, based on the use of XOR fragments of the logic. We not only show that such fragments can be decided, tractably, via clausal temporal resolution, but also show the benefits of combining multiple XOR fragments. For such combinations we establish completeness and complexity (of the resolution method), and also describe how such a temporal language might be used in application areas, for example the verification of multi-agent systems. This new approach to temporal reasoning provides a framework in which tractable temporal logics can be engineered by intelligently combining appropriate XOR fragments.

JELIA Conference 2006 Conference Paper

Anti-prenexing and Prenexing for Modal Logics

• Cláudia Nalon
• Clare Dixon

Abstract Efficient proof methods for normal modal logics are highly desirable, as such logical systems have been widely used in computer science to represent complex situations. Resolution-based methods are often designed to deal with formulae in a normal form and the efficiency of the method (also) relies on how efficient (in the sense of producing fewer and/or shorter clauses) the translation procedure is. We present a normal form for normal modal logics and show how the use of simplification, for specific normal logics, together with anti-prenexing and prenexing techniques help us to produce better sets of clauses.

TIME Conference 2006 Conference Paper

Is There a Future for Deductive Temporal Verification?

• Clare Dixon
• Michael Fisher 0001
• Boris Konev

In this paper, we consider a tractable sub-class of propositional linear time temporal logic, and provide a complete clausal resolution calculus for it. The fragment is important as it can be used to represent simple Buchi automata. We also show that, just as the emptiness check for a Buchi automaton is tractable, the complexity of deciding unsatisfiability, via resolution, of our logic is polynomial (rather than exponential). Consequently, a Buchi automaton can be represented within our logic, and its emptiness can be tractably decided via deductive methods. This may have a significant impact upon approaches to verification, since techniques such as model checking inherently depend on the ability to check emptiness of an appropriate Buchi automaton. Thus, we also discuss how such a logic might form the basis for practical deductive temporal verification

I&C Journal 2005 Journal Article

Mechanising first-order temporal resolution

• Boris Konev
• Anatoli Degtyarev
• Clare Dixon
• Michael Fisher
• Ullrich Hustadt

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. Although a complete and correct resolution-style calculus has already been suggested for this specific fragment, this calculus involves constructions too complex to be of practical value. In this paper, we develop a machine-oriented clausal resolution method which features radically simplified proof search. We first define a normal form for monodic formulae and then introduce a novel resolution calculus that can be applied to formulae in this normal form. By careful encoding, parts of the calculus can be implemented using classical first-order resolution and can, thus, be efficiently implemented. We prove correctness and completeness results for the calculus and illustrate it on a comprehensive example. An implementation of the method is briefly discussed.

ECAI Conference 2004 Conference Paper

Miss Scarlett in the Ballroom with the Lead Piping

• Clare Dixon

TIME Conference 2004 Conference Paper

Using Temporal Logics of Knowledge in the Formal Verification of Security Protocols

• Clare Dixon
• M. Carmen Fernández Gago
• Michael Fisher 0001
• Wiebe van der Hoek

Temporal logics of knowledge are useful for reasoning about situations where the knowledge of an agent or component is important, and where change in this knowledge may occur over time. Here we use temporal logics of knowledge to reason about security protocols. We show how to specify part of the Needham-Schroeder protocol using temporal logics of knowledge and prove various properties using a clausal resolution calculus for this logic.

TIME Conference 2003 Conference Paper

Tableaux for Temporal Logics of Knowledge: Synchronous Systems of Perfect Recall or No Learning

• Clare Dixon
• Cláudia Nalon
• Michael Fisher 0001

The paper describes tableaux based proof methods for temporal logics of knowledge allowing interaction axioms between the modal and temporal components. Such logics can be used to specify systems that involve the knowledge of processes or agents and which change over time, for example agent based systems or knowledge games. The interaction axioms allow the description of how knowledge evolves over time and makes reasoning in such logics theoretically more complex. Completeness arguments for the tableaux are discussed.

TIME Conference 2003 Conference Paper

Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case

• Boris Konev
• Anatoli Degtyarev
• Clare Dixon
• Michael Fisher 0001
• Ullrich Hustadt

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. In this paper, we develop a clausal resolution method for the monodic fragment of first-order temporal logic over expanding domains. We first define a normal form for monodic formulae and then introduce novel resolution calculi that can be applied to formulae in this normal form. We state correctness and completeness results for the method. We illustrate the method on a comprehensive example. The method is based on classical first-order resolution and can, thus, be efficiently implemented.

AIJ Journal 2002 Journal Article

Clausal resolution in a logic of rational agency

• Clare Dixon
• Michael Fisher
• Alexander Bolotov

A resolution based proof system for a Temporal Logic of Possible Belief is presented. This logic is the combination of the branching-time temporal logic CTL (representing change over time) with the modal logic KD45 (representing belief). Such combinations of temporal or dynamic logics and modal logics are useful for specifying complex properties of multi-agent systems. Proof methods are important for developing verification techniques for these complex multi-modal logics. Soundness, completeness and termination of the proof method are shown and simple examples illustrating its use are given.

TIME Conference 2001 Conference Paper

Reasoning about agents in the KARO framework

• Ullrich Hustadt
• Clare Dixon
• Renate A. Schmidt
• Michael Fisher 0001
• John-Jules Ch. Meyer
• Wiebe van der Hoek

This paper proposes two methods for realising automated reasoning about agent-based systems. The framework for modelling intelligent agent behaviour that we focus on is a core of KARO logic, an expressive combination of various modal logics including propositional dynamic logic, a modal logic of knowledge, a modal logic of wishes, and additional non-standard operators. The first method we present is based on a translation of core KARO logic to first-order logic combined with first-order resolution. The second method uses an embedding of core KARO logic into a combination of branching-time temporal logic CTL and multi-modal S5 plus a clausal resolution calculus for these combined logics. We discuss the advantages and shortcomings of each approach and suggest ways to extend each variant to cover more of the KARO framework.

TIME Conference 2000 Conference Paper

Resolution for Branching Time Temporal Logics: Applying the Temporal Resolution Rule

• Alexander Bolotov
• Clare Dixon

We propose algorithms to implement a branching time temporal resolution theorem prover. The branching time temporal logic considered is Computation Tree Logic (CTL), often regarded as the simplest useful logic of this class. Unlike the majority of the research into temporal logic, we adopt a resolution-based approach. The method applies step and temporal resolution rules to the set of formulae in a normal form. Whilst step resolution is similar to the classical resolution rule, the temporal resolution rule resolves a formula, /spl phi/, that must eventually occur with a set of formulae that together imply that /spl phi/ can never occur. Thus the method is dependent on the efficient detection of such sets of formulae. We present algorithms to search for these sets of formulae, give a correctness argument, and examples of their operation.

TIME Conference 2000 Conference Paper

Resolution-Based Proof for Multi-Modal Temporal Logics of Knowledge

• Clare Dixon
• Michael Fisher 0001

Temporal logics of knowledge are useful in order to specify complex systems in which agents are both dynamic and have information about their surroundings. We present a resolution method for propositional temporal logic combined with multi-modal S5 and illustrate its use on examples. This paper corrects a previous proposal for resolution in multi-model temporal logics of knowledge.

MFCS Conference 1999 Conference Paper

Clausal Resolution for CTL *

• Alexander Bolotov
• Clare Dixon
• Michael Fisher 0001

Abstract In this paper we consider proof techniques for branching-time temporal logics. While a considerable amount of research has been carried out regarding the relationship between finite automata and such logics, practical proof techniques for such logics have received relatively little attention. Recently, however, several applications requiring refined proof methods for branching-time temporal logics have appeared, most notably the specification and verification of multi-agent systems. Thus, here we extend our clausal resolution method for linear-time temporal logics to a branching-time framework, in particular to the powerful CTL* logic. The key elements of the resolution method, namely the normal form, the concept of step resolution and a novel temporal resolution rule, are introduced, justified, and applied.

TIME Conference 1998 Conference Paper

The Set of Support Strategy in Temporal Resolution

• Clare Dixon
• Michael Fisher 0001

A variety of proof methods have been developed to support the effective mechanisation of temporal logic. While clausal temporal resolution has been successfully employed for a range of problems, a number of improvements are still required. In particular, as there is no consistent control strategy underlying the method, and a large amount of irrelevant information may sometimes be generated. Following on from classical resolution, where the 'Set of Support' strategy has been used very successfully, we introduce, justify and apply a temporal version of this strategy, thus allowing the supporting set to be carried over between the different phases of the resolution method. This not only restricts the production of irrelevant information but, under certain conditions, retains the completeness of the refutation process.

TIME Conference 1997 Conference Paper

Temporal Resolution: Removing Irrelevant Information

• Clare Dixon

The generation of too much information prohibits efficient resolution proof search in classical logics. Hence subsumption is used to discard redundant information and strategies have been developed to guide the proof search avoiding irrelevant information. The extension of the resolution method to temporal logics, for example that by Fisher (1991) for propositional linear-time temporal logics, further magnifies this problem. We provide an algorithm to efficiently remove irrelevant information prior to the application of Fisher's temporal resolution rule, show that it retains the completeness of the temporal resolution system and demonstrate its efficiency on a set of examples.

TIME Conference 1996 Conference Paper

Temporal Resolution: A Breadth-First Search Approach

• Clare Dixon

An approach to applying clausal resolution, a proof method for classical logics suited to mechanisation, to temporal logics has been developed by Fisher. The method involves translation to a normal form, classical style resolution within states and temporal resolution between states. The method consists of only one temporal resolution rule and is therefore particularly suitable as the basis of an automated temporal resolution theorem prover. As the application of this temporal resolution rule is the most costly part of the method, involving search amongst graphs, it is on this area we focus. A breadth-first search approach to the application of this rule is presented and shown to be correct. Analysis of its operation is carried out and test results for its comparison to a previously developed depth-first style algorithm given.