Hongyang Qu

Paolo Izzo, Hongyang Qu, Sandor M. Veres

The AgentSpeak type of languages are considered for decision making in autonomous control systems. To reduce the complexity and increase the verifiability of decision making, a limited instruction set agent (LISA) is introduced. The new decision method is structurally simpler than its predecessors and easily lends itself to both design time and runtime verification methods. The process of converting a control agent in LISA into a model in a probabilistic model checker is described. Due to the practical complexity of design time verification the feasibility of runtime probabilistic verification is investigated and illustrated in the LISA agent programming system for verifying symbolic plans of the agent using a probabilistic model checker.

Paolo Izzo, Hongyang Qu, Sandor M. Veres

A new agent architecture called Limited Instruction Set Agent (LISA) is introduced for autonomous control. The new architecture is based on previous implementations of AgentSpeak and it is structurally simpler than its predecessors with the aim of facilitating design-time and run-time verification methods. The process of abstracting the LISA system to two different types of discrete probabilistic models (DTMC and MDP) is investigated and illustrated. The LISA system provides a tool for complete modelling of the agent and the environment for probabilistic verification. The agent program can be automatically compiled into a DTMC or a MDP model for verification with Prism. The automatically generated Prism model can be used for both design-time and run-time verification. The run-time verification is investigated and illustrated in the LISA system as an internal modelling mechanism for prediction of future outcomes.

Mohammed Y. Hazim, Hongyang Qu, Sandor M. Veres

This paper addresses the problem of improving response times of robots implemented in the Robotic Operating System (ROS) using formal verification of computational-time feasibility. In order to verify the real time behaviour of a robot under uncertain signal processing times, methods of formal verification of timeliness properties are proposed for data flows in a ROS-based control system using Probabilistic Timed Programs (PTPs). To calculate the probability of success under certain time limits, and to demonstrate the strength of our approach, a case study is implemented for a robotic agent in terms of operational times verification using the PRISM model checker, which points to possible enhancements to the operation of the robotic agent.

Hongyang Qu, Sandor M. Veres

Most autonomous robotic agents use logic inference to keep themselves to safe and permitted behaviour. Given a set of rules, it is important that the robot is able to establish the consistency between its rules, its perception-based beliefs, its planned actions and their consequences. This paper investigates how a robotic agent can use model checking to examine the consistency of its rules, beliefs and actions. A rule set is modelled by a Boolean evolution system with synchronous semantics, which can be translated into a labelled transition system (LTS). It is proven that stability and consistency can be formulated as computation tree logic (CTL) and linear temporal logic (LTL) properties. Two new algorithms are presented to perform realtime consistency and stability checks respectively. Their implementation provides us a computational tool, which can form the basis of efficient consistency checks on-board robots.