BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Sandor M. Veres

Sandor M. Veres appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
RoboticsArtificial IntelligenceMultiagent SystemsSystems and ControlLogic in Computer ScienceSoftware EngineeringComputer Science and Game Theoryeess.SY

Catalog footprint

What is connected

13works
8topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

13 published item(s)

preprint2020arXiv

Verification Framework for Control System Functionality of Unmanned Aerial Vehicles

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 proceedures, a higher-order logic interactive theorem-prover and an automated theorem-prover are utilized 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 proceedures are that some of the resulting methods can be implemented onboard the aircraft to detect when its controller breaches its flight envelop 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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

A Continuous-Time Model of an Autonomous Aerial Vehicle to Inform and Validate Formal Verification Methods

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 developing 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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

A stochastically verifiable autonomous control architecture with reasoning

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Collision Avoidance of Two Autonomous Quadcopters

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Dynamical Behavior Investigation and Analysis of Novel Mechanism for Simulated Spherical Robot named "RollRoller"

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Fictitious play for cooperative action selection in robot teams

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Formal Verification of Autonomous Vehicle Platooning

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Reducing complexity of autonomous control agents for verifiability

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

SMCL - Stochastic Model Checker for Learning in Games

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Testing, Verification and Improvements of Timeliness in ROS processes

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Verification of Logical Consistency in Robotic Reasoning

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.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Practical Verification of Decision-Making in Agent-Based Autonomous Systems

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.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Agent Based Approaches to Engineering Autonomous Space Software

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.

0 citations0 reviewsNo code linkedOpen access