Minimum-violation LTL planning with conflicting specifications
Minimum-violation LTL planning with conflicting specifications
复制标题
DOI：
10.1109/acc.2013.6579837
复制
发表时间：
2013-03
期刊：
影响因子：
--
通讯作者：
Jana Tumova;L. I. R. Castro;S. Karaman;Emilio Frazzoli;D. Rus
中科院分区：
文献类型：
--
作者：
Jana Tumova;L. I. R. Castro;S. Karaman;Emilio Frazzoli;D. Rus
在给定一组高级任务规范的情况下，我们考虑了机器人车辆控制策略的自动生成问题，例如，车辆X最终必须访问目标区域，然后返回基地，区域A和B必须定期测量，或者车辆都不能进入不安全区域。我们关注的是由于不兼容和/或环境限制而无法同时达到所有给定规范的实例。我们的目标是在考虑满足任务不同部分的不同优先级的同时，找到违反最少的控制策略。形式上，我们考虑以线性时间逻辑公式的形式给出的任务，每个任务都被分配了当公式满足时赚取的奖励。利用基于自动机的模型检测的思想，我们提出了一种算法，用于寻找最优控制策略，以最大化该控制策略所获得的回报之和。最后，通过一个算例验证了该算法的有效性。
We consider the problem of automatic generation of control strategies for robotic vehicles given a set of high-level mission specifications, such as “Vehicle x must eventually visit a target region and then return to a base,” “Regions A and B must be periodically surveyed,” or “None of the vehicles can enter an unsafe region.” We focus on instances when all of the given specifications cannot be reached simultaneously due to their incompatibility and/or environmental constraints. We aim to find the least-violating control strategy while considering different priorities of satisfying different parts of the mission. Formally, we consider the missions given in the form of linear temporal logic formulas, each of which is assigned a reward that is earned when the formula is satisfied. Leveraging ideas from the automata-based model checking, we propose an algorithm for finding an optimal control strategy that maximizes the sum of rewards earned if this control strategy is applied. We demonstrate the proposed algorithm on an illustrative case study.