The advent of sophisticated robotics and AI technology makes sending humans into hazardous and distant environments to carry out inspections increasingly avoidable. Being able to send a robot, rather than a human, into a nuclear facility or deep space is very appealing. However, building these robotic systems is just the start and we still need to carry out a range of verification and validation tasks to ensure that the systems to be deployed are as safe and reliable as possible. Based on our experience across three research and innovation hubs within the UK’s “Robots for a Safer World” programme, we present an overview of the relevant techniques and challenges in this area. As the hubs are active across nuclear, offshore, and space environments, this gives a breadth of issues common to many inspection robots.

This paper presents an extension of the Predictive Runtime Verification (PRV) paradigm to consider multiple models of the System Under Analysis (SUA). We call this extension Multi-Model PRV. Typically, PRV attempts to predict the satisfaction or violation of a property based on a trace and a (single) formal model of the SUA. However, contemporary node- or component-based systems (e.g. robotic systems) may benefit from monitoring based on a model of each component. We show how a Multi-Model PRV approach can be applied in either a centralised or a compositional way (where the property is compositional), as best suits the SUA. Crucially, our approach is formalism-agnostic. We demonstrate our approach using an illustrative example of a Mars Curiosity rover simulation and evaluate our contribution via a prototype implementation.

We study ontology-mediated querying in the case where ontologies are formulated in the guarded fragment of first-order logic (GF) or extensions thereof with counting and where the actual queries are (unions of) conjunctive queries. Our aim is to classify the data complexity and Datalog rewritability of query evaluation depending on the ontology O , where query evaluation w.r.t. O is in PT ime (resp. Datalog rewritable) if all queries can be evaluated in PT ime w.r.t. O (resp. rewritten into Datalog under O ), and co NP-hard if at least one query is co NP-hard w.r.t. O . We identify several fragments of GF that enjoy a dichotomy between Datalog-rewritability (which implies PT ime ) and co NP-hardness as well as several other fragments that enjoy a dichotomy between PT ime and co NP-hardness, but for which PT ime does not imply Datalog-rewritability. For the latter, we establish and exploit a connection to constraint satisfaction problems. We also identify fragments for which there is no dichotomy between PT ime and co NP. To prove this, we establish a non-trivial variation of Ladner’s theorem on the existence of NP-intermediate problems. Finally, we study the decidability of whether a given ontology enjoys PT ime query evaluation, presenting both positive and negative results, depending on the fragment.

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.