Swarm robotic systems consist of numerous simple robots coordinating in a decentralised manner to achieve a common goal. Ensuring that individual robot behaviours lead to the desired swarm-level outcomes is challenging due to the lack of a central controller. This article uses two frameworks to facilitate formal specification and verification of robot swarms: (1) NuXMV, which models the system as a Finite State Machine, specifies properties using temporal logic, and verifies them through model checking with BDDs and SMT-solvers; and (2) GROOVE, which models the system as a Graph Grammar, specifies properties using temporal logic with graphical states, and verifies them via graph-specific model checking algorithms. We compare these formal approaches by modelling the Alpha swarm aggregation algorithm, which ensures that any robot disconnected from the swarm, capable only of short-range wireless communications, will eventually return to it. We find that GROOVE effectively leverages symmetry to reduce the state space, while NuXMV excels in handling models requiring extensive calculations and data manipulations not optimally expressed through graphs. We discuss the suitability of each approach for different systems and properties, suggesting future directions that combine the strengths of both approaches.

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.

Abstract We present deterministic model construction algorithms for sets of modal clauses saturated with respect to three refinements of the modal-layered resolution calculus implemented in the prover "Image missing". The model construction algorithms are inspired by the Bachmair-Ganzinger method for constructing a model for a set of ground first-order clauses saturated with respect to ordered resolution with selection. The challenge is that the inference rules of the modal-layered resolution calculus for modal operators are more restrictive than an adaptation of ordered resolution with selection for these would be. While these model construction algorithms provide an alternative means to proving completeness of the calculus, our main interest is the provision of a ‘certificate’ for satisfiable modal formulae that can be independently checked to assure a user that the result of "Image missing" is correct. This complements the existing provision of proofs for unsatisfiable modal formulae.

Autonomous robotic systems systems are both safety- and security-critical, since a breach in system security may impact safety. In such critical systems, formal verification is used to model the system and verify that it obeys specific functional and safety properties. Independently, threat modelling is used to analyse and manage the cyber security threats that such systems may encounter. Both verification and threat analysis serve the purpose of ensuring that the system will be reliable, albeit from differing perspectives. In prior work, we argued that these analyses should be used to inform one another and, in this paper, we extend our previously defined methodology for security-minded verification by incorporating runtime verification. To illustrate our approach, we analyse an algorithm for sending Cooperative Awareness Messages between autonomous vehicles. Our analysis centres on identifying STRIDE security threats. We show how these can be formalised, and subsequently verified, using a combination of formal tools for static aspects, namely Promela/SPIN and Dafny, and generate runtime monitors for dynamic verification. Our approach allows us to focus our verification effort on those security properties that are particularly important and to consider safety and security in tandem, both statically and at runtime.

We introduce a variant of a formalism appearing in recent work geared towards modelling systems in which a distinguished entity (leader) orchestrates the operation of an arbitrary number of identical entities (followers). Our variant is better suited for the verification of system properties involving complex arithmetic conditions. Whereas the original formalism is translated into a tractable fragment of first-order temporal logic, aiming to utilize automated (first-order temporal logic) theorem provers for verification, our variant is translated into linear integer arithmetic, aiming to utilize satisfiability modulo theories (SMT) solvers for verification. In particular, for any given system specified in our formalism, we prove, for any natural numbern, the existence of a linear integer arithmetic formula whose models are in one-to-one correspondence with certain counting abstractions (profiles) of executions of the system forntime steps. Thus, one is able to verify, for any natural numbern, that all executions forntime steps of any such system have a given property by establishing that said formula logically entails the property. To highlight the practical utility of our approach, we specify and verify three consensus protocols, actively used in distributed database systems and low-power wireless networks.

Abstract We are interested in widening the reasoning support for propositional modal logics in the so-called modal cube. The modal cube consists of extensions of the basic modal logic $$\textsf{K}_{}$$ K with an arbitrary combination of the modal axioms $$\textsf{B}$$ B , $$\textsf{D}$$ D , $$\textsf{T}$$ T , $$\textsf{4}$$ 4 and $$\textsf{5}$$ 5 . We revisit recently developed local reductions from all logics in the modal cube to a normal form comprising sets of clausal formulae with associated modal levels. We extend these reductions further to the basic modal logic $$\textsf{K}_{}$$ K , called definitional reductions. This enables any prover for $$\textsf{K}_{}$$ K to be used to solve the satisfiability problem for all logics in the modal cube. We also present alternative, axiomatic, reductions based on ideas originally proposed by Kracht, providing new theoretical results and improved bounds on the size of the reductions. We compare both sets of reductions combined with state-of-the-art provers for $$\textsf{K}_{}$$ K on a large set of parametric benchmarks for all logics in the modal cube. The results show that the provers perform better with reductions based on the clausal normal form than the axiomatic reductions.

Abstract We present novel reductions of extensions of the basic modal logic $${\textsf {K} }$$ K with axioms $$\textsf {B} $$ B , $$\textsf {D} $$ D , $$\textsf {T} $$ T , $$\textsf {4} $$ 4 and $$\textsf {5} $$ 5 to Separated Normal Form with Sets of Modal Levels $$\textsf {SNF} _{sml}$$ SNF sml . The reductions typically result in smaller formulae than the reductions by Kracht. The reductions to $$\textsf {SNF} _{sml}$$ SNF sml combined with a reduction to $$\textsf {SNF} _{ml}$$ SNF ml allow us to use the local reasoning of the prover $${\text {K}_{\text {S}}}{\text {P}}$$ K S P to determine the satisfiability of modal formulae in the considered logics. We show experimentally that the combination of our reductions with the prover $${\text {K}_{\text {S}}}{\text {P}}$$ K S P performs well when compared with a specialised resolution calculus for these logics, the built-in reductions of the first-order prover SPASS, and the higher-order logic prover LEO-III.

Abstract We present novel reductions of the propositional modal logics "Image missing" , "Image missing" , "Image missing" , "Image missing" and "Image missing" to Separated Normal Form with Sets of Modal Levels. The reductions result in smaller formulae than the well-known reductions by Kracht and allow us to use the local reasoning of the prover "Image missing" to determine the satisfiability of modal formulae in these logics. We show experimentally that the combination of our reductions with the prover "Image missing" performs well when compared with a specialised resolution calculus for these logics and with the b̆uilt-in reductions of the first-order prover SPASS.

Abstract We introduce a framework for the verification of protocols involving a distinguished machine (referred to as a leader) orchestrating the operation of an arbitrary number of identical machines (referred to as followers) in a network. At the core of our framework is a high-level formalism capturing the operation of these types of machines together with their network interactions. We show that this formalism automatically translates to a tractable form of first-order temporal logic. Checking whether a protocol specified in our formalism satisfies a desired property (expressible in temporal logic) then amounts to checking whether the protocol’s translation in first-order temporal logic entails that property. Many different types of protocols used in practice, such as cache coherence, atomic commitment, consensus, and synchronization protocols, fit within our framework. First-order temporal logic also facilitates parameterized verification by enabling us to model such protocols abstractly without referring to individual machines.

We develop a taxonomy that categorizes HRI failure types and their impact on trust to structure the broad range of knowledge contributions. We further identify research gaps in order to support fellow researchers in the development of trustworthy robots. Studying trust repair in HRI has only recently been given more interest and we propose a taxonomy of potential trust violations and suitable repair strategies to support researchers during the development of interaction scenarios. The taxonomy distinguishes four failure types: Design, System, Expectation, and User failures and outlines potential mitigation strategies. Based on these failures, strategies for autonomous failure detection and repair are presented, employing explanation, verification and validation techniques. Finally, a research agenda for HRI is outlined, discussing identified gaps related to the relation of failures and HR-trust.

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.

Abstract Algorithms for the synchronisation of clocks across networks are both common and important within distributed systems. We here address not only the formal modelling of these algorithms, but also the formal verification of their behaviour. Of particular importance is the strong link between the very different levels of abstraction at which the algorithms may be verified. Our contribution is primarily the formalisation of this connection between individual models and population-based models, and the subsequent verification that is then possible. While the technique is applicable across a range of synchronisation algorithms, we particularly focus on the synchronisation of (biologically-inspired) pulse-coupled oscillators, a widely used approach in practical distributed systems. For this application domain, different levels of abstraction are crucial: models based on the behaviour of an individual process are able to capture the details of distinguished nodes in possibly heterogenous networks, where each node may exhibit different behaviour. On the other hand, collective models assume homogeneous sets of processes, and allow the behaviour of the network to be analysed at the global level. System-wide parameters may be easily adjusted, for example environmental factors inhibiting the reliability of the shared communication medium. This work provides a formal bridge across the “abstraction gap” separating the individual models and the population-based models for this important class of synchronisation algorithms.

Abstract We study translations from metric temporal logic (MTL) over the natural numbers to linear temporal logic (LTL). In particular, we present two approaches for translating from MTL to LTL which preserve the complexity of the satisfiability problem for MTL. In each of these approaches we consider the case where the mapping between states and time points is given by (i) a strict monotonic function and by (ii) a non-strict monotonic function (which allows multiple states to be mapped to the same time point). We use this logic to model examples from robotics, traffic management, and scheduling, discussing the effects of different modelling choices. Our translations allow us to utilise LTL solvers to solve satisfiability and we empirically compare the translations, showing in which cases one performs better than the other. We also define a branching-time version of the logic and provide translations into computation tree logic.

In this paper we describe the implementation of , a resolution-based prover for the basic multimodal logic $${\textsf {K}}_{n}^{}$$ Kn. The prover implements a resolution-based calculus for both local and global reasoning. The user can choose different normal forms, refinements of the basic resolution calculus, and strategies. We describe these options in detail and discuss their implications. We provide experiments comparing some of these options and comparing the prover with other provers for this logic.

Resolution-based provers for multimodal normal logics require pruning of the search space for a proof to ameliorate the inherent intractability of the satisfiability problem for such logics. We present a clausal modal-layered hyper-resolution calculus for the basic multimodal logic, which divides the clause set according to the modal level at which clauses occur to reduce the number of possible inferences. We show that the calculus is complete for the logics being considered. We also show that the calculus can be combined with other strategies. In particular, we discuss the completeness of combining modal layering with negative and ordered resolution and provide experimental results comparing the different refinements.

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.

It is essential for robots working in close proximity to people to be both safe and trustworthy. We present a case study on formal verification for a high-level planner/scheduler for the Care-O-bot, an autonomous personal robotic assistant. We describe how a model of the Care-O-bot and its environment was developed using Brahms, a multiagent workflow language. Formal verification was then carried out by automatically translating this model to the input language of an existing model checker. Four sample properties based on system requirements were verified. We then refined the environment model three times to increase its accuracy and the persuasiveness of the formal verification results. The first refinement uses a user activity log based on real-life experiments, but is deterministic. The second refinement uses the activities from the user activity log nondeterministically. The third refinement uses “conjoined activities” based on an observation that many user activities can overlap. The four samples properties were verified for each refinement of the environment model. Finally, we discuss the approach of environment model refinement with respect to this case study.

We present a resolution-based calculus for Coalition Logic CL, a non-normal modal logic used for reasoning about cooperative agency. We introduce a normal form and a set of inference rules to solve the satisfiability problem in CL. We also show that the calculus presented here is sound, complete, and terminating.

The branching-time temporal logic CTL is useful for specifying systems that change over time and involve quantification over possible futures. Here we present a resolution calculus for CTL that involves the translation of formulae to a normal form and the application of a number of resolution rules. We use indices in the normal form to represent particular paths and the application of the resolution rules is restricted dependent on an ordering and selection function to reduce the search space. We show that the translation preserves satisfiability, the calculus is sound, complete, and terminating, and consider the complexity of the calculus.

Intrusion Detection Systems (IDS) aim to detect the actions that attempt to compromise the confidentiality, availability, and integrity of a resource by monitoring the events occurring in computer systems and/or networks. Stream data processing is a database technology applied to flows of data. Temporal Logic is a formalism for representing change over time. This paper proposes the development of a network intrusion detection system by combining temporal formalisms for representing attack patterns with stream processing for intruder detection. The experimental results show that this combination successfully was able to detect all the attacks of that type in the test data. Additionally, the solution provides a concise and unambiguous way to formally represent attack signatures and it is extensible and scalable.

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.

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.

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

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.

1Bolzano 2Liverpool 3Liverpool 4Bolzano

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.

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.

We consider the relationship between ω‐automata and a specific logical formulation based on a normal form for temporal logic formulae. While this normal form was developed for use with execution and clausal resolution in temporal logics, we here show how it can represent, syntactically, ω‐automata in a high‐level way. Technical proofs of the correctness of this representation are given.

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.

In this article, we examine how clausal resolution can be applied to a specific, but widely used, nonclassical logic, namely discrete linear temporal logic. Thus, we first define a normal form for temporal formulae and show how arbitrary temporal formulae can be translated into the normal form, while preserving satisfiability. We then introduce novel resolution rules that can be applied to formulae in this normal form, provide a range of examples, and examine the correctness and complexity of this approach. Finally, we describe related work and future developments concerning this work.

The generation of too much information prohibits efficient resolution proof search in classical logics. 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, further magnifies this problem. Here we develop an algorithm for the removal of irrelevant information during resolution proofs for a particular resolution proof system for propositional linear-time temporal logic. The resolution system operates on formulae in a normal form. Following a phase of classical style resolution, temporal resolution is carried out by detecting sets of formulae that together represent an □-formula to be resolved with a ◊-formula. It is before the application of the temporal resolution rule that the new algorithm is applied to efficiently remove irrelevant information. The completeness of the new algorithm is discussed and its complexity considered. Its practical efficiency is demonstrated by giving timings for a set of examples.

A resolution-based proof system for a temporal logic of knowledge is presented and shown to be correct. Such logics are useful for proving properties of distributed and multi-agent systems. Examples are given to illustrate the proof system. An extension of the basic system to the multi-modal case is given and illustrated using the ‘muddy children problem’.