检索结果-内蒙古大学图书馆

Temporal Logic Task Allocation in Heterogeneous Multirobot Systems

IEEE TRANSACTIONS ON robotics 2022年第6期38卷 3602-3621页

作者： Luo, Xusheng Zavlanos, Michael M. Duke Univ Dept Mechan Engn & Mat Sci Durham NC 27708 USA

We consider the problem of optimally allocating tasks, expressed as global linear temporal logic (LTL) specifications, to teams of heterogeneous mobile robots of different types. Each task may require robots of multiple types. To obtain a scalable solution, we propose a hierarchical approach that first allocates specific robots to tasks using the information about the tasks contained in the nondeterministic B ii chi automaton (NBA) that captures the LTL specification and then designs low-level paths for robots that respect the high-level assignment. Specifically, motivated by "lazy collision checking" methods in robotics, we first prune and relax the NBA by removing all negative atomic propositions, which simplifies the planning problem by checking constraint satisfaction only when needed. Then, we extract sequences of subtasks from the relaxed NBA along with their temporal orders and formulate a mixed integer linear program to allocate these subtasks to robots. Finally, we define generalized multirobot path planning problems to obtain low-level paths that satisfy both the high-level task allocation and the constraints captured by the negative atomic propositions in the original NBA. We show that our method is complete for a subclass of LTL that covers a broad range of tasks and present numerical simulations demonstrating that it can generate paths with lower cast, considerably faster than existing methods.

关键词： formal methods in robotics and automation motion and path planning path planning for multiple mobile robots or agents task planning

来源：评论

学校读者我要写书评

暂无评论

Probabilistic Coordination of Heterogeneous Teams From Capability Temporal Logic Specifications

引用

IEEE robotics AND automation LETTERS 2022年第2期7卷 1190-1197页

作者： Cai, Mingyu Leahy, Kevin Serlin, Zachary Vasile, Cristian-Ioan Lehigh Univ Mech Engn Bethlehem PA 18015 USA MIT Lincoln Lab Lexington MA 02421 USA

This letter explores coordination of heterogeneous teams of agents from high-level specifications. We employ Capability Temporal Logic (CaTL) to express rich, temporal-spatial tasks that require cooperation between many agents with unique capabilities. CaTL specifies combinations of tasks, each with desired locations, duration, and set of capabilities, freeing the user from considering specific agent trajectories and their impact on multi-agent cooperation. CaTL also provides a quantitative robustness metric of satisfaction based on availability of required capabilities for each task. The novelty of this letter focuses on satisfaction of CaTL formulas under probabilistic conditions. Specifically, we consider uncertainties in robot motion (e.g., agents may fail to transition between regions with some probability) and local probabilistic workspace properties (e.g., if there are not enough agents of a required capability to complete a collaborative task). The proposed approach automatically formulates a mixed-integer linear program given agents, their dynamics and capabilities, an abstraction of the workspace, and a CaTL formula. In addition to satisfying the given CaTL formula, the optimization considers the following secondary goals (in decreasing order of priority): 1) minimize the risk of transition failure due to uncertainties;2) maximize probabilities of regional collaborative satisfaction (if there is an excess of agents);3) maximize the availability robustness of CaTL for potential agent attrition;4) minimize the total agent travel time. We evaluate the performance of the proposed framework and demonstrate its scalability via numerical simulations.

关键词： formal methods in robotics and automation multi-robot systems planning scheduling and coordination

来源：评论

学校读者我要写书评

暂无评论

Coloured Petri Nets for Temporal Performance Evaluation of Distributed Control Systems-Application to a FIFO Queue

引用

IEEE robotics AND automation LETTERS 2022年第4期7卷 11268-11274页

作者： Bal Dit Sollier, Louis Ourghanlian, Alain Amari, Said EDF R&D PRISME F-78400 Chatou France ENS Paris Saclay LURPA F-91190 Gif Sur Yvette France

Temporal performances (like response time) of distributed control systems must he measurable for critical systems. The delay and reliability requirements require us to develop an exhaustive method to evaluate these performances through the most accurate models, such as (max,+) algebra combined with timed event graphs. Among the common mechanisms encountered in a distributed control system, the FIFO policy remains one of the mast used and cannot be modeled with timed event graphs. We show that the formalism of timed coloured Petri nets described in the (max,+) algebra can model the FIFO queue of a Programmable Logic Controller communication module. We also aim to reveal some exciting features of coloured Petri nets when analytically evaluating temporal performances. We present, therefore, a Timed Coloured Petri net modeling the emptying of a FIFO queue with a periodic task, and the formulas of delays associated with the induced system of (max, +) equations. We also test the consistency of our hounds in a numerical application of our model with positive results.

关键词： Discrete event dynamic automation systems distributed control systems formal methods in robotics and automation Petri nets for automation control response time evaluation

来源：评论

学校读者我要写书评

暂无评论

Event-Based Signal Temporal Logic Tasks: Execution and Feedback in Complex Environments

引用

IEEE robotics AND automation LETTERS 2022年第4期7卷 10001-10008页

作者： Gundana, David Kress-Gazit, Hadas Cornell Univ Sibley Sch Mech & Aerosp Engn Ithaca NY 14853 USA

In this work, we synthesize control for high-level, reactive robot tasks that include timing constraints and choices over goals and constraints. We enrich Event-based Signal Temporal Logic by adding disjunctions, and propose a framework for synthesizing controllers that satisfy such specifications. If there are multiple ways to satisfy a specification, we choose, at run-time, a controller that instantaneously maximizes robustness. During execution, we automatically generate feedback in the form of pre-failure warnings that give users insight as to why a specification may be violated in the future. We demonstrate our work through physical and simulated multi-robot systems operating in complex environments.

关键词： formal methods in robotics and automation hybrid logical/dynamical planning and verification multi-robot systems

来源：评论

学校读者我要写书评

暂无评论

A framework for formal verification of robot kinematics

引用

JOURNAL OF LOGICAL AND ALGEBRAIC methods IN PROGRAMMING 2024年 139卷

作者： Xie, Guojun Yang, Huanhuan Chen, Gang Nanjing Univ Aeronaut & Astronaut Coll Comp Sci & Technol Nanjing 211106 Jiangsu Peoples R China Natl Univ Def Technol Coll Comp Changsha 410073 Hunan Peoples R China

As robotic applications continue to expand and task complexity increases, the adoption of more advanced and sophisticated control algorithms and models becomes critical. Traditional methods, relying on manual abstraction and modeling to verify these algorithms and models, may not fully encompass all potential design paths, leading to incomplete models, design defects, and increased vulnerability to security risks. The verification of control systems using formal methods is crucial for ensuring the safety of robots. This paper introduces a formal verification framework for robot kinematics implemented in Coq. It constructs a formal proof for the theory of robot motion and control algorithms, specifically focusing on the theory of robot kinematics, which includes the homogeneous representation of robot coordinates and the transformation relations between different coordinate systems. Subsequently, we provide formal definitions and verification for several commonly used structural robots, along with their coordinate transformation algorithms. Finally, we extract the Coq code, convert the functional algorithms into OCaml code, and perform data validation using various examples. It is worth emphasizing that the framework we have built possesses a high level of reusability, providing a solid technological foundation for the development of kinematics theorem libraries.

关键词： formal methods in robotics and automation Kinematics formal verification Coq proof assistant Coordinate conversion

来源：评论

学校读者我要写书评

暂无评论

An Abstraction-Free Method for Multirobot Temporal Logic Optimal Control Synthesis

引用

IEEE TRANSACTIONS ON robotics 2021年第5期37卷 1487-1507页

作者： Luo, Xusheng Kantaros, Yiannis Zavlanos, Michael M. Duke Univ Dept Mech Engn & Mat Sci Durham NC 27708 USA

The majority of existing linear temporal logic (LTL) planning methods rely on the construction of a discrete product automaton, which combines a discrete abstraction of robot mobility and a Buchi automaton that captures the LTL specification. Representing this product automaton as a graph and using graph search techniques, optimal plans that satisfy the LTL task can be synthesized. However, constructing expressive discrete abstractions makes the synthesis problem computationally intractable. In this article, we propose a new sampling-based LTL planning algorithm that does not require any discrete abstraction of robot mobility. Instead, it incrementally builds trees that explore the product state-space, until a maximum number of iterations is reached or a feasible plan is found. The use of trees makes data storage and graph search tractable, which significantly increases the scalability of our algorithm. To accelerate the construction of feasible plans, we introduce bias in the sampling process, which is guided by transitions in the Buchi automaton that belong to the shortest path to the accepting states. We show that our planning algorithm, with and without bias, is probabilistically complete and asymptotically optimal. Finally, we present numerical experiments showing that our method outperforms relevant temporal logic planning methods.

关键词： Task analysis Planning Automata Sampling methods Navigation Heuristic algorithms Acceleration formal methods in robotics and automation motion and path planning optimization and optimal control path planning for multiple mobile robots or agents

来源：评论

学校读者我要写书评

暂无评论

Data-Driven Energy Estimation of Individual Instructions in User-Defined Robot Programs for Collaborative Robots

引用

IEEE robotics AND automation LETTERS 2021年第4期6卷 6836-6843页

作者： Heredia, Juan Schlette, Christian Kjaergaard, Mikkel Baun Univ Southern Denmark Maersk Mc Kinney Moller Inst Campusvej 55 DK-5230 Odense Denmark

Traditionally, the objective of industrial production focuses on fast and low-cost production, regardless of resources and energy consumption (EC). However, in alignment with the UN Sustainable Development Goals (SDG), governments worldwide have proposed regulations to reduce resources and energy. In their production lines, an increasing number of companies are using collaborative robots (cobots). Cobots are programmed to accomplish their task as fast as possible, ignoring the robot's EC. This letter estimates the cobot EC from individual instructions of user-defined robot programs. Thus, the user has an additional design parameter to create energy-optimal programs. In the literature, current EC estimation models for manipulators are not reliable or have not been assessed to test the model's reliability. Our modeling methodology possesses three steps: motion planning, dynamic model, and EC model. Using cobots of different sizes (UR3e and UR10e) and loading, we collected over 55000 samples per case and trained the model to identify the model's unknown parameters. The model estimated the power consumption of a testing dataset with a maximum RMS error of 6 [W] - 3.85%. In the final experiment, the complete system was tested using a user-defined program composed of six instructions. The results showed an accurate estimation of the power profile with an RMS error of 2.39 [W] and 4.23 [W] for UR3e and UR10e.

关键词： Energy and environment-aware automation simulation and animation calibration and identification dynamics formal methods in robotics and automation

来源：评论

学校读者我要写书评

暂无评论

Planning of Heterogeneous Multi-Agent Systems Under Signal Temporal Logic Specifications With Integral Predicates

引用

IEEE robotics AND automation LETTERS 2021年第2期6卷 1375-1382页

作者： Buyukkocak, Ali Tevfik Aksaray, Derya Yazcoglu, Yasin Univ Minnesota Dept Aerosp Engn & Mech Minneapolis MN 55455 USA Univ Minnesota Dept Elect & Comp Engn Minneapolis MN 55455 USA

We address the problem of coordinating the trajectories of heterogeneous multi-agent systems under spatio-temporal specifications. In particular, we consider global Signal Temporal Logic (STL) constraints to express the number and type of agents that should be present at specific locations within the desired time windows. We also introduce an integral predicate to specify cumulative progress that can he achieved asynchronously by multiple agents. In order to generate optimal trajectories, we formulate a mixed-integer linear program whose objective is minimizing the agent movement subject to the heterogeneous abstracted dynamics of the agents and a global STL specification including the novel integral predicate. We demonstrate the performance of the proposed method via simulations and experiments with drones.

关键词： formal methods in robotics and automation multi-robot systems optimization and optimal control

来源：评论

学校读者我要写书评

暂无评论

Event-Based Signal Temporal Logic Synthesis for Single and Multi-Robot Tasks

引用

IEEE robotics AND automation LETTERS 2021年第2期6卷 3687-3694页

作者： Gundana, David Kress-Gazit, Hadas Cornell Univ Sibley Sch Mech & Aerosp Engn Ithaca NY 14853 USA

We propose a new specification language and control synthesis technique for single and multi-robot high-level tasks;these tasks include timing constraints and reaction to environmental events. Specifically, we define Event-based Signal Temporal Logic (STL) and use it to encode tasks that are reactive to uncontrolled environment events. Our control synthesis approach to Event-based STL tasks combines automata and control barrier functions to produce robot behaviors that satisfy the specification when possible. Our method automatically provides feedback to the user if an Event-based STL task cannot be achieved. We demonstrate the effectiveness of the framework through simulations and physical demonstrations of multi-robot tasks.

关键词： formal methods in robotics and automation hybrid logical/dynamical planning and verification multi-robot systems

来源：评论

学校读者我要写书评

暂无评论

Interval-Based Visua LiDAR Sensor Fusion

引用

IEEE robotics AND automation LETTERS 2021年第2期6卷 1304-1311页

作者： Voges, Raphael Wagner, Bernardo Leibniz Univ Hannover Inst Syst Engn Real Time Syst Grp RTS D-30167 Hannover Germany

Since cameras and Light Detection and Ranging (LiDAR) sensors provide complementary information about the environment, it is beneficial for mobile robot localization to fuse their information by assigning distances measured by the LiDAR to visual features detected in the image. However, existing approaches neglect the uncertainty of the fused information or model it in an optimistic way (e.g., without taking extrinsic calibration errors into account). Since the actual distribution of errors during sensor fusion is often unknown, we assume to only know bounds (or intervals) enclosing the errors. Consequently, we propose to use interval analysis to propagate the error from the input sources to the fused information in a straightforward way. To show the applicability of our approach, we use the fused information for dead reckoning. Since interval analysis is used, the result of our approach are intervals that are guaranteed to enclose the robot's true pose. An evaluation using real data shows that we are indeed able to localize the robot in a guaranteed way. This enables us to detect faults of an established approach, which neglects the uncertainty of the fused information, in three out of ten cases.

关键词： Sensor fusion formal methods in robotics and automation localization interval analysis

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：