Sandor M. Veres

A control system verification framework is presented for unmanned aerial vehicles using theorem proving. The framework’s aim is to set out a procedure for proving that the mathematically designed control system of the aircraft satisfies robustness requirements to ensure safe performance under varying environmental conditions. Extensive mathematical derivations, which have formerly been carried out manually, are checked for their correctness on a computer. To illustrate the procedures, a higher-order logic interactive theorem-prover and an automated theorem-prover are utilised to formally verify a nonlinear attitude control system of a generic multi-rotor UAV over a stability domain within the dynamical state space of the drone. Further benefits of the procedures are that some of the resulting methods can be implemented onboard the aircraft to detect when its controller breaches its flight envelope limits due to severe weather conditions or actuator/sensor malfunction. Such a detection procedure can be used to advise the remote pilot, or an onboard intelligent agent, to decide on some alterations of the planned flight path or to perform emergency landing.

The evolution of driving technology has recently progressed from active safety features and ADAS systems to fully sensor-guided autonomous driving. Bringing such a vehicle to market requires not only simulation and testing but formal verification to account for all possible traffic scenarios. A new verification approach, which combines the use of two well-known model checkers: model checker for multi-agent systems (MCMAS) and probabilistic model checker (PRISM), is presented for this purpose. The overall structure of our autonomous vehicle (AV) system consists of: (1) A perception system of sensors that feeds data into (2) a rational agent (RA) based on a belief–desire–intention (BDI) architecture, which uses a model of the environment and is connected to the RA for verification of decision-making, and (3) a feedback control systems for following a self-planned path. MCMAS is used to check the consistency and stability of the BDI agent logic during design-time. PRISM is used to provide the RA with the probability of success while it decides to take action during run-time operation. This allows the RA to select movements of the highest probability of success from several generated alternatives. This framework has been tested on a new AV software platform built using the robot operating system (ROS) and virtual reality (VR) Gazebo Simulator. It also includes a parking lot scenario to test the feasibility of this approach in a realistic environment. A practical implementation of the AV system was also carried out on the experimental testbed.

Quadcopter controllers are in use today and in practice they can often cope well in non adverse weather conditions such as lack of strong sudden gusts of wind around the corner of a building or no frequent demands of travel directions by remote control or a guidance law. Different payloads can alter the boundaries of the stable state space region of a drone, its flight envelop, beyond which its autopilot may not be able to regain stable control of the craft. For fixed gain autopilot controllers, reaching the boundary of the flight envelop can be caused by (1) external disturbance like gusts of wind and turbulence, (2) altered drone mass and its distribution and (3) reduction or misalignment of thrust output in the propulsion system caused ware after multiple uses of the drone. This paper introduces symbolic computation to map out the numerical boundaries of controller tolerances in terms of these three factors that affect the autopilots ability to retain stability of the craft. Proof theoretic methods are developed that can be applied to quadcopter of various nominal parameters.

Simultaneous Search and Monitoring (SSM) is studied in this paper for a single Unmanned Aerial Vehicle (UAV) searcher and multiple moving ground targets. Searching for unknown targets and monitoring known targets are two intrinsically related problems, but have mostly been addressed in isolation. We combine the two problems with a joint objective function in a Partially Observable Markov Decision Process (POMDP). An online policy planning approach is proposed to plan a reactive policy to solve the POMDP, using both MonteCarlo sampling and Simulated Annealing. The simulation result shows that the searcher will successfully find unknown targets without losing known ones. We demonstrate, with a theoretical proof and comparative simulations, that the proposed approach can deliver a better performance than conventional foresight optimization methods.

A game theoretic distributed decision making approach is presented for the problem of control effort allocation in a robotic team based on a novel variant of fictitious play. The proposed learning process allows the robots to accomplish their objectives by coordinating their actions in order to efficiently complete their tasks. In particular, each robot of the team predicts the other robots' planned actions while making decisions to maximise their own expected reward that depends on the reward for joint successful completion of the task. Action selection is interpreted as an $n$-player cooperative game. The approach presented can be seen as part of the \emph{Belief Desire Intention} (BDI) framework, also can address the problem of cooperative, legal, safe, considerate and emphatic decisions by robots if their individual and group rewards are suitably defined. After theoretical analysis the performance of the proposed algorithm is tested on four simulation scenarios. The first one is a coordination game between two material handling robots, the second one is a warehouse patrolling task by a team of robots, the third one presents a coordination mechanism between two robots that carry a heavy object on a corridor and the fourth one is an example of coordination on a sensors network.

A stochastic model checker is presented for analysing the performance of game-theoretic learning algorithms. The method enables the comparison of short-term behaviour of learning algorithms intended for practical use. The procedure of comparison is automated and it can be tuned for accuracy and speed. Users can choose from among various learning algorithms to select a suitable one for a given practical problem. The powerful performance of the method is enabled by a novel behaviour-similarity-relation, which compacts large state spaces into small ones. The stochastic model checking tool is tested on a set of examples classified into four categories to demonstrate the effectiveness of selecting suitable algorithms for distributed decision making.

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.