Synthesis for Robots: Guarantees and Feedback for Robot Behavior

2018 ◽  
Vol 1 (1) ◽  
pp. 211-236 ◽  
Author(s):  
Hadas Kress-Gazit ◽  
Morteza Lahijanian ◽  
Vasumathi Raman
Keyword(s):  
Formal Methods ◽  
Robot Control ◽  
Formal Synthesis ◽  
Complex Tasks ◽  
Current State ◽  
Robot Behavior ◽  
Mathematical Techniques ◽  
Task Specification

Robot control for tasks such as moving around obstacles or grasping objects has advanced significantly in the last few decades. However, controlling robots to perform complex tasks is still accomplished largely by highly trained programmers in a manual, time-consuming, and error-prone process that is typically validated only through extensive testing. Formal methods are mathematical techniques for reasoning about systems, their requirements, and their guarantees. Formal synthesis for robotics refers to frameworks for specifying tasks in a mathematically precise language and automatically transforming these specifications into correct-by-construction robot controllers or into a proof that the task cannot be done. Synthesis allows users to reason about the task specification rather than its implementation, reduces implementation error, and provides behavioral guarantees for the resulting controller. This article reviews the current state of formal synthesis for robotics and surveys the landscape of abstractions, specifications, and synthesis algorithms that enable it.

scholarly journals Building the Foundation of Robot Explanation Generation Using Behavior Trees

2021 ◽  
Vol 10 (3) ◽  
pp. 1-31
Author(s):  
Zhao Han ◽  
Daniel Giger ◽  
Jordan Allspaw ◽  
Michael S. Lee ◽  
Henny Admoni ◽  
...  
Keyword(s):  
Autonomous Robots ◽  
Free Form ◽  
Static Structure ◽  
Simulation Code ◽  
Causal Information ◽  
Robot Behavior ◽  
Behavior Trees ◽  
Robot Task ◽  
Task Specification ◽  
Explanation Generation

As autonomous robots continue to be deployed near people, robots need to be able to explain their actions. In this article, we focus on organizing and representing complex tasks in a way that makes them readily explainable. Many actions consist of sub-actions, each of which may have several sub-actions of their own, and the robot must be able to represent these complex actions before it can explain them. To generate explanations for robot behavior, we propose using Behavior Trees (BTs), which are a powerful and rich tool for robot task specification and execution. However, for BTs to be used for robot explanations, their free-form, static structure must be adapted. In this work, we add structure to previously free-form BTs by framing them as a set of semantic sets {goal, subgoals, steps, actions} and subsequently build explanation generation algorithms that answer questions seeking causal information about robot behavior. We make BTs less static with an algorithm that inserts a subgoal that satisfies all dependencies. We evaluate our BTs for robot explanation generation in two domains: a kitting task to assemble a gearbox, and a taxi simulation. Code for the behavior trees (in XML) and all the algorithms is available at github.com/uml-robotics/robot-explanation-BTs.

Formal Approaches to Systems Analysis Using UML

2002 ◽  
pp. 324-341
Author(s):  
Jonathan Whittle
Keyword(s):  
Formal Methods ◽  
Development Strategy ◽  
Ad Hoc ◽  
Formal Analysis ◽  
Daily Basis ◽  
Software Systems ◽  
Industry Standard ◽  
Mathematical Techniques ◽  
Software Lifecycle ◽  
Modeling Level

Formal methods, whereby a system is described and/or analyzed using precise mathematical techniques, is a well-established and yet, under-used approach for developing software systems. One of the reasons for this is that project deadlines often impose an unsatisfactory development strategy in which code is produced on an ad hoc basis without proper thought about the requirements and design of the piece of software in mind. The result is a large, often poorly documented and un-modular monolith of code that does not lend itself to formal analysis. Because of their complexity, formal methods work best when code is well structured, e.g., when they are applied at the modeling level. UML is a modeling language that is easily learned by system developers and, more importantly, an industry standard, which supports communication between the various project stakeholders. The increased popularity of UML provides a real opportunity for formal methods to be used on a daily basis within the software lifecycle. Unfortunately, the lack of precision of UML means that many formal techniques cannot be applied directly. If formal methods are to be given the place they deserve within UML, a more precise description of UML must be developed. This chapter surveys recent attempts to provide such a description, as well as techniques for analyzing UML models formally.

Risk-Aware Control

2014 ◽  
Vol 26 (12) ◽  
pp. 2669-2691 ◽  
Author(s):  
Terence D. Sanger
Keyword(s):  
Feedback Control ◽  
Robot Control ◽  
Human Movement ◽  
Spiking Neurons ◽  
Cost Functions ◽  
Control Law ◽  
Time Varying ◽  
Unknown Parameters ◽  
Current State ◽  
The Cost

Human movement differs from robot control because of its flexibility in unknown environments, robustness to perturbation, and tolerance of unknown parameters and unpredictable variability. We propose a new theory, risk-aware control, in which movement is governed by estimates of risk based on uncertainty about the current state and knowledge of the cost of errors. We demonstrate the existence of a feedback control law that implements risk-aware control and show that this control law can be directly implemented by populations of spiking neurons. Simulated examples of risk-aware control for time-varying cost functions as well as learning of unknown dynamics in a stochastic risky environment are provided.

scholarly journals The Implementation of a Hierarchical Hybrid Navigation System for a Mobile Robotic Vehicle

2021 ◽  
Author(s):  
◽  
Buddika Kasun Talwatta
Keyword(s):  
Control System ◽  
Robot Control ◽  
Service Oriented Architecture ◽  
Infrared Sensors ◽  
Current State ◽  
Service Oriented ◽  
Software And Hardware ◽  
Differential Drive Robot ◽  
Robotic Vehicle ◽  
State Of The Environment

<p>One of the challenges of robotics is to develop a robot control system capable of obtaining intelligent, suitable responses to dynamic environments. The basic requirements for accomplishing this is a robot control architecture and a hardware platform that can adapt the software and hardware to the current state of the environment. This has led researchers to design control architectures composed of distributed, independent and asynchronous behaviours. In line with this research, this thesis details the development of a control system which adopts a hierarchical hybrid navigation architecture designed at Victoria University of Wellington. The implementation of the control system is aimed towards one of Victoria University of Wellington’s fleet of mobile robotic platforms called MARVIN. MARVIN is a differential drive robot and the sensory equipment on the device includes infrared sensors and odometry. The control system has been implemented in C# .NET programming language adopting a Service- Oriented Architecture. This software framework provides several services along with a graphical user interface to configure the control system. Several experiments have been carried out to test the control system and the results indicate that the features of the navigation architecture have been accomplished</p>

scholarly journals Online Reconfiguration of Distributed Robot Control Systems for Modular Robot Behavior Implementation

2020 ◽  
Vol 100 (3-4) ◽  
pp. 1283-1308
Author(s):  
Malte Wirkus ◽  
Sascha Arnold ◽  
Elmar Berghöfer
Keyword(s):  
Control Systems ◽  
Robot Control ◽  
Autonomous Robots ◽  
High Complexity ◽  
Software Developer ◽  
Robot Controller ◽  
Software Complexity ◽  
Robot Behavior ◽  
Development Approach ◽  
Operational Modes

AbstractThe use of autonomous robots in areas that require executing a broad range of different tasks is currently hampered by the high complexity of the software that adapts the robot controller to different situations the robot would face. Current robot software frameworks facilitate implementing controllers for individual tasks with some variability, however, their possibilities for adapting the controllers at runtime are very limited and don’t scale with the requirements of a highly versatile autonomous robot. With the software presented in this paper, the behavior of robots is implemented modularly by composing individual controllers, between which it is possible to switch freely at runtime, since the required transitions are calculated automatically. Thereby the software developer is relieved of the task to manually implement and maintain the transitions between different operational modes of the robot, what largely reduces software complexity for larger amounts of different robot behaviors. The software is realized by a model-based development approach. We will present the metamodels enabling the modeling of the controllers as well as the runtime architecture for the management of the controllers on distributed computation hardware. Furthermore, this paper introduces an algorithm that calculates the transitions between two controllers. A series of technical experiments verifies the choice of the underlying middleware and the performance of online controller reconfiguration. A further experiment demonstrates the applicability of the approach to real robotics applications.

scholarly journals Formal Verification of Cloud and Fog Systems:A Review and Research Challenges

2021 ◽  
Vol 27 (4) ◽  
pp. 341-363
Author(s):  
Fairouz Fakhfakh ◽  
Slim Kallel ◽  
Saoussen Cheikhrouhou
Keyword(s):  
Formal Methods ◽  
State Of The Art ◽  
Fog Computing ◽  
Crucial Issue ◽  
Future Directions ◽  
Industrial Sectors ◽  
Current State ◽  
Verification Methods ◽  
Academic Researchers ◽  
Verification Tools

Cloud and Fog computing have been widely recognized as attractive solutions in both academic and industrial sectors. Despite their benefits, the adoption of Cloud and Fog computing still have considerable challenges to be handled due to the increase of client requirements. A crucial issue, in this context, is how to verify the correctness of Cloud and Fog systems. The use of formal methods is an efficient mean which provides a real help for the designer to evaluate the behaviour of a system and prevent errors before its implementation. In this paper, we present a systematic literature review (SLR) on the current state of the art in this field. We collect the existing studies on the use of formal methods for proving the correctness of Cloud and Fog systems. The proposed approaches are compared based on some technical properties such as the verification methods, the verification tools, the considered properties, and the application domains. In addition, future directions which need more investigations are presented. We believe that our paper will be useful for industry and academic researchers to understand the existing contributions that deal with the cor- rectness of Cloud and Fog systems. Moreover, it helps them to address several gaps in the literature.

scholarly journals Astrophysical Magnetic Fields

2021 ◽  
Author(s):  
Anvar Shukurov ◽  
Kandaswamy Subramanian
Keyword(s):  
Magnetic Fields ◽  
Current Knowledge ◽  
Cosmic Time ◽  
Worked Examples ◽  
Critical Discussion ◽  
Current State ◽  
Advanced Students ◽  
Extensive Introduction ◽  
Mathematical Techniques ◽  
Perceived Complexity

Magnetic fields permeate space and affect many major astrophysical phenomena, but they are often ignored due to their perceived complexity. This self-contained introduction to astrophysical magnetic fields provides both a comprehensive review of the current state of the subject and a critical discussion of the latest research. It presents our knowledge of magnetic fields from the Early Universe, their evolution in cosmic time through to their roles in present-day galaxies, galaxy clusters and the wider intergalactic medium, with attention given to both theory and observations. This volume also contains an extensive introduction into magnetohydrodynamics, numerous worked examples, observational and mathematical techniques and interpretations of the observations. Its review of our current knowledge, with an emphasis on results that are likely to form the basis for future progress, benefits a broad audience of advanced students and active researchers, including those from fields such as cosmology and general relativity.

scholarly journals A survey of challenges for runtime verification from advanced application domains (beyond software)

2019 ◽  
Vol 54 (3) ◽  
pp. 279-335 ◽  
Author(s):  
César Sánchez ◽  
Gerardo Schneider ◽  
Wolfgang Ahrendt ◽  
Ezio Bartocci ◽  
Domenico Bianculli ◽  
...  
Keyword(s):  
Dynamic Analysis ◽  
Formal Methods ◽  
Computational Models ◽  
State Of The Art ◽  
Runtime Verification ◽  
Formal Specifications ◽  
New Techniques ◽  
Execution Traces ◽  
Current State ◽  
Potential Applications

Abstract Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification.

scholarly journals The Implementation of a Hierarchical Hybrid Navigation System for a Mobile Robotic Vehicle

2021 ◽  
Author(s):  
◽  
Buddika Kasun Talwatta
Keyword(s):  
Control System ◽  
Robot Control ◽  
Service Oriented Architecture ◽  
Infrared Sensors ◽  
Current State ◽  
Service Oriented ◽  
Software And Hardware ◽  
Differential Drive Robot ◽  
Robotic Vehicle ◽  
State Of The Environment

<p>One of the challenges of robotics is to develop a robot control system capable of obtaining intelligent, suitable responses to dynamic environments. The basic requirements for accomplishing this is a robot control architecture and a hardware platform that can adapt the software and hardware to the current state of the environment. This has led researchers to design control architectures composed of distributed, independent and asynchronous behaviours. In line with this research, this thesis details the development of a control system which adopts a hierarchical hybrid navigation architecture designed at Victoria University of Wellington. The implementation of the control system is aimed towards one of Victoria University of Wellington’s fleet of mobile robotic platforms called MARVIN. MARVIN is a differential drive robot and the sensory equipment on the device includes infrared sensors and odometry. The control system has been implemented in C# .NET programming language adopting a Service- Oriented Architecture. This software framework provides several services along with a graphical user interface to configure the control system. Several experiments have been carried out to test the control system and the results indicate that the features of the navigation architecture have been accomplished</p>

Formal Methods for the Development and Verification of Autonomic IT Systems

2011 ◽  
pp. 1-37 ◽  
Author(s):  
Radu Calinescu ◽  
Shinji Kikuchi ◽  
Marta Kwiatkowska
Keyword(s):  
Formal Methods ◽  
Formal Specification ◽  
Autonomic Computing ◽  
Ad Hoc ◽  
Conflict Detection ◽  
It Systems ◽  
Challenges And Opportunities ◽  
Quantitative Verification ◽  
Mathematical Techniques

This chapter explores ways in which rigorous mathematical techniques, termed formal methods, can be employed to improve the predictability and dependability of autonomic computing. Model checking, formal specification, and quantitative verification are presented in the contexts of conflict detection in autonomic computing policies, and of implementation of goal and utility-function policies in autonomic IT systems, respectively. Each of these techniques is illustrated using a detailed case study, and analysed to establish its merits and limitations. The analysis is then used as a basis for discussing the challenges and opportunities of this endeavour to transition the development of autonomic IT systems from the current practice of using ad-hoc methods and heuristic towards a more principled approach.

Sign in / Sign up

Export Citation Format

Share Document