-
Concepts of Self-maintaining Robots and Their Design
Authors:
Chenjie Shi,
Sandor M Veres
Abstract:
This paper proposes an initial theory for robotic systems that can be fully self-maintaining. The new design principles focus on functional survival of the robots over long periods of time without human maintenance. Self-maintaining semi-autonomous mobile robots are in great demand in nuclear disposal sites from where their removal for maintenance is undesirable due to their radioactive contaminat…
▽ More
This paper proposes an initial theory for robotic systems that can be fully self-maintaining. The new design principles focus on functional survival of the robots over long periods of time without human maintenance. Self-maintaining semi-autonomous mobile robots are in great demand in nuclear disposal sites from where their removal for maintenance is undesirable due to their radioactive contamination. Similar are requirements for robots in various defence tasks or space missions. For optimal design, modular solutions are balanced against capabilities to replace smaller components in a robot by itself or by help from another robot. Modules are proposed for the basic platform, which enable self-maintenance within a team of robots hel** each other. The primary method of self-maintenance is replacement of malfunctioning modules or components by the robots themselves. Replacement necessitates a robot team's ability to diagnose and replace malfunctioning modules as needed. Due to their design, these robots still remain manually re-configurable if opportunity arises for human intervention. Apart from the basic principles, an evolutionary design approach is presented and a first mathematical theory of the reliability of a team of self-maintaining robots is introduced.
△ Less
Submitted 12 October, 2021;
originally announced October 2021.
-
SMCL - Stochastic Model Checker for Learning in Games
Authors:
Hongyang Qu,
Michalis Smyrnakis,
Sandor M. Veres
Abstract:
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 prac…
▽ More
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.
△ Less
Submitted 10 November, 2016;
originally announced November 2016.
-
Fictitious play for cooperative action selection in robot teams
Authors:
Michalis Smyrnakis,
Sandor M. Veres
Abstract:
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' plann…
▽ More
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.
△ Less
Submitted 17 November, 2016;
originally announced November 2016.
-
A stochastically verifiable autonomous control architecture with reasoning
Authors:
Paolo Izzo,
Hongyang Qu,
Sandor M. Veres
Abstract:
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…
▽ More
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.
△ Less
Submitted 10 November, 2016;
originally announced November 2016.
-
Testing, Verification and Improvements of Timeliness in ROS processes
Authors:
Mohammed Y. Hazim,
Hongyang Qu,
Sandor M. Veres
Abstract:
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 Pro…
▽ More
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.
△ Less
Submitted 10 November, 2016;
originally announced November 2016.
-
Verification of Logical Consistency in Robotic Reasoning
Authors:
Hongyang Qu,
Sandor M. Veres
Abstract:
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, belief…
▽ More
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.
△ Less
Submitted 10 November, 2016;
originally announced November 2016.
-
Dynamical Behavior Investigation and Analysis of Novel Mechanism for Simulated Spherical Robot named "RollRoller"
Authors:
Seyed Amir Tafrishi,
Sandor M. Veres,
Esmaeil Esmaeilzadeh,
Mikhail Svinin
Abstract:
This paper introduces a simulation study of fluid actuated multi-driven closed system as spherical mobile robot called "RollRoller". Robot's mechanism design consists of two essential parts: tubes to lead a core and mechanical controlling parts to correspond movements. Our robot gets its motivation force by displacing the spherical movable mass known as core in curvy manners inside certain pipes.…
▽ More
This paper introduces a simulation study of fluid actuated multi-driven closed system as spherical mobile robot called "RollRoller". Robot's mechanism design consists of two essential parts: tubes to lead a core and mechanical controlling parts to correspond movements. Our robot gets its motivation force by displacing the spherical movable mass known as core in curvy manners inside certain pipes. This simulation investigates by explaining the mechanical and structural features of the robot for creating hydraulic-base actuation via force and momentum analysis. Next, we categorize difficult and integrated 2D motions to omit unstable equilibrium points through derived nonlinear dynamics. We propose an algorithmic position control in forward direction that creates hybrid model as solution for motion planning problem in spherical robot. By deriving nonlinear dynamics of the spherical robot and implementing designed motion planning, we show how RollRoller can be efficient in high speed movements in comparison to the other pendulum-driven models. Then, we validate the results of this position control obtained by nonlinear dynamics via Adams/view simulation which uses the imported solid model of RollRoller. Lastly, We have a look to the circular maneuver of this robot by the same simulator.
△ Less
Submitted 19 October, 2016;
originally announced October 2016.
-
A Continuous-Time Model of an Autonomous Aerial Vehicle to Inform and Validate Formal Verification Methods
Authors:
Murray L. Ireland,
Ruth Hoffmann,
Alice Miller,
Gethin Norman,
Sandor M. Veres
Abstract:
If autonomous vehicles are to be widely accepted, we need to ensure their safe operation. For this reason, verification and validation (V&V) approaches must be developed that are suitable for this domain. Model checking is a formal technique which allows us to exhaustively explore the paths of an abstract model of a system. Using a probabilistic model checker such as PRISM, we may determine proper…
▽ More
If autonomous vehicles are to be widely accepted, we need to ensure their safe operation. For this reason, verification and validation (V&V) approaches must be developed that are suitable for this domain. Model checking is a formal technique which allows us to exhaustively explore the paths of an abstract model of a system. Using a probabilistic model checker such as PRISM, we may determine properties such as the expected time for a mission, or the probability that a specific mission failure occurs. However, model checking of complex systems is difficult due to the loss of information during abstraction. This is especially so when considering systems such as autonomous vehicles which are subject to external influences. An alternative solution is the use of Monte Carlo simulation to explore the results of a continuous-time model of the system. The main disadvantage of this approach is that the approach is not exhaustive as not all executions of the system are analysed. We are therefore interested in develo** a framework for formal verification of autonomous vehicles, using Monte Carlo simulation to inform and validate our symbolic models during the initial stages of development. In this paper, we present a continuous-time model of a quadrotor unmanned aircraft undertaking an autonomous mission. We employ this model in Monte Carlo simulation to obtain specific mission properties which will inform the symbolic models employed in formal verification.
△ Less
Submitted 1 September, 2016;
originally announced September 2016.
-
Collision Avoidance of Two Autonomous Quadcopters
Authors:
Michalis Smyrnakis,
Jonathan M. Aitken,
Sandor M. Veres
Abstract:
Traffic collision avoidance systems (TCAS) are used in order to avoid incidences of mid-air collisions between aircraft. We present a game-theoretic approach of a TCAS designed for autonomous unmanned aerial vehicles (UAVs). A variant of the canonical example of game-theoretic learning, fictitious play, is used as a coordination mechanism between the UAVs, that should choose between the alternativ…
▽ More
Traffic collision avoidance systems (TCAS) are used in order to avoid incidences of mid-air collisions between aircraft. We present a game-theoretic approach of a TCAS designed for autonomous unmanned aerial vehicles (UAVs). A variant of the canonical example of game-theoretic learning, fictitious play, is used as a coordination mechanism between the UAVs, that should choose between the alternative altitudes to fly and avoid collision. We present the implementation results of the proposed coordination mechanism in two quad-copters flying in opposite directions.
△ Less
Submitted 17 March, 2016;
originally announced March 2016.
-
Formal Verification of Autonomous Vehicle Platooning
Authors:
Maryam Kamali,
Louise A. Dennis,
Owen McAree,
Michael Fisher,
Sandor M. Veres
Abstract:
The coordination of multiple autonomous vehicles into convoys or platoons is expected on our highways in the near future. However, before such platoons can be deployed, the new autonomous behaviors of the vehicles in these platoons must be certified. An appropriate representation for vehicle platooning is as a multi-agent system in which each agent captures the "autonomous decisions" carried out b…
▽ More
The coordination of multiple autonomous vehicles into convoys or platoons is expected on our highways in the near future. However, before such platoons can be deployed, the new autonomous behaviors of the vehicles in these platoons must be certified. An appropriate representation for vehicle platooning is as a multi-agent system in which each agent captures the "autonomous decisions" carried out by each vehicle. In order to ensure that these autonomous decision-making agents in vehicle platoons never violate safety requirements, we use formal verification. However, as the formal verification technique used to verify the agent code does not scale to the full system and as the global verification technique does not capture the essential verification of autonomous behavior, we use a combination of the two approaches. This mixed strategy allows us to verify safety requirements not only of a model of the system, but of the actual agent code used to program the autonomous vehicles.
△ Less
Submitted 4 February, 2016;
originally announced February 2016.
-
Practical Verification of Decision-Making in Agent-Based Autonomous Systems
Authors:
Louise A. Dennis,
Michael Fisher,
Nicholas K. Lincoln,
Alexei Lisitsa,
Sandor M. Veres
Abstract:
We present a verification methodology for analysing the decision-making component in agent-based hybrid systems. Traditionally hybrid automata have been used to both implement and verify such systems, but hybrid automata based modelling, programming and verification techniques scale poorly as the complexity of discrete decision-making increases making them unattractive in situations where complex…
▽ More
We present a verification methodology for analysing the decision-making component in agent-based hybrid systems. Traditionally hybrid automata have been used to both implement and verify such systems, but hybrid automata based modelling, programming and verification techniques scale poorly as the complexity of discrete decision-making increases making them unattractive in situations where complex logical reasoning is required. In the programming of complex systems it has, therefore, become common to separate out logical decision-making into a separate, discrete, component. However, verification techniques have failed to keep pace with this development. We are exploring agent-based logical components and have developed a model checking technique for such components which can then be composed with a separate analysis of the continuous part of the hybrid system. Among other things this allows program model checkers to be used to verify the actual implementation of the decision-making in hybrid autonomous systems.
△ Less
Submitted 9 October, 2013;
originally announced October 2013.
-
Agent Based Approaches to Engineering Autonomous Space Software
Authors:
Louise A. Dennis,
Michael Fisher,
Nicholas Lincoln,
Alexei Lisitsa,
Sandor M. Veres
Abstract:
Current approaches to the engineering of space software such as satellite control systems are based around the development of feedback controllers using packages such as MatLab's Simulink toolbox. These provide powerful tools for engineering real time systems that adapt to changes in the environment but are limited when the controller itself needs to be adapted.
We are investigating ways in wh…
▽ More
Current approaches to the engineering of space software such as satellite control systems are based around the development of feedback controllers using packages such as MatLab's Simulink toolbox. These provide powerful tools for engineering real time systems that adapt to changes in the environment but are limited when the controller itself needs to be adapted.
We are investigating ways in which ideas from temporal logics and agent programming can be integrated with the use of such control systems to provide a more powerful layer of autonomous decision making. This paper will discuss our initial approaches to the engineering of such systems.
△ Less
Submitted 2 March, 2010;
originally announced March 2010.
