correctreactivehighlevelrobotcontrol阅读报告

《correctreactivehighlevelrobotcontrol阅读报告》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、阅读报告Correct,Reactive,High-LevelRobotControlMitigatingtheStateExplosionProblemofTemporalLogicSynthesis缓解时序逻辑合成的状态空间爆炸问题主要涉及的知识背景：1、自动机2、LTL线性时序逻辑，克里普克结构3、多层次的协同方法4、模拟与互模拟5、抽象的粒度6、滚动时域框架综述：本文通过以美国国防部高级研究计划局举办的城市挑战赛为例引机器人控制中存在的问题，进而介绍模拟和互模拟来保证抽象的解决方案与连续执行的一

2、致性。但是，同时导致计算复杂度加大，文中主要介绍抽象粒度和状态空间的关系，并介绍了解决状态空间爆炸的方法：1、使用粒度大的抽象，并将任务分解成互不相交的四个自动机以进一步降低复杂度；2、使用粒度小的抽象，使用滚动时域框架来降低复杂。Robotsthesedaysfeatureatightinterplaybetweencomputationalandphysicalcomponents.现今，机器人的计算和物理部件之间有着紧密的相互作用。举例：DARPAUrbanChallenge在城市挑战赛中，参赛车辆

3、需要在全自动控制下，在模拟城市的场景中识别静/动态的障碍物，执行不同的任务（如在不同路况的环境中，在遵守当地交通法规的前提条件下完成驾驶，泊车，到达指定地域等操作）。在执行这些任务的同时，智能车也许满足底层物理部件和实际动作的局限性（如，不可能达到超出发动机的极限的速度，不可能实现瞬间的大角度转弯）。因此，关于控制车辆行为的高层逻辑需要适当的集成到底层的控制器中。现存在的问题：系统是通过某种特定的方法将计算和物理部件紧密耦合在一起。即使单个部件通过大量的测试和形式化验证满足正确性，但是，整个系统的复杂度已

4、经超出了形式化验证的承受能力，同时迫使人们放弃大部分的测试。如在2007年参加城市挑战赛的车辆”Alice”在研发期间经过了上千小时的模拟和300英里的现场测试。但是一旦发现一个问题未覆盖到再修改底层的特定设计是不可能的。最终导致取消Alice的挑战资格。因此，要想实现智能车和机器人的自主调度，需要经过形式化验证并设计期结构合理的嵌入式控制器。并使用形式化语言(如LTL)说明规范，以说明其在所有有效环境参数下的行为。一、实施上述方案的通常步骤为：1、构造一个基于底层物理系统的有穷状态的抽象2、制定满足高层

5、逻辑规范的自动机控制策略。二、上述的步骤导致控制机构的分层（类似于混合型系统）1、高层离散的事件2、底层控制器连续的执行。三、模拟和互模拟验证了连续的执行确保了离散事件的正确性。但是上述的方法将导致庞大的计算复杂度。四、为此，文章描述了两种缓解状态空间爆炸的方法1、coarseabstraction基于低层控制器，通过RNDF和MDF文件，考虑所有可能的情况，以及相应的操作。2、fine-abstraction使用滚动时域的方法，对未来较短时间段的事件作出预判，并根据实时感受器接收到的信息对控制信息进行修

6、正。Background:我们先将问题抽象成离散的时间，再在物理层面上对于机器人的动作和反应生成连续的控制。为了方便进步的论述，这里先介绍几个基础的背景知识。这个自动机表示了一个机器人控制问题的离散事件。传感器的信息对应了六元组的输入字母表，机器人的动作和反应对应输出字母表。1、automata这里我们使用自动机的概念并不是太贴切，因为我们并没有定义通常的接收状态。更精确的说应该是”KripkeStructure”。1、是有穷状态集2、为初始状态集3、是输入字母表4、是输出字母表5、是状态转换函数6、是输

7、出函数2、LinearTemporalLogicLTL=原子命题+时间轴+时态算子In logic,lineartemporallogicorlinear-timetemporallogic(LTL)isa modal temporallogic withmodalitiesreferringtotime.线性时序逻辑是基于时间的形式化时序逻辑。Itisafragmentofthemorecomplex CTL*,whichadditionallyallowsbranchingtimeandquantif

8、iers.它可以看做更为复杂的CTL*的一个分支。本文将使用LTL作为形式化表示来定义机器人高层,反馈的行为.从广义上来说,LTL允许原子命题的真值随着时间的推移而改变.递归定义的LTL的语法如下，其中是一个原子命题组中的AP(所有原子命题和他们的否定命题的集合)，其中还包括真与假命题。基本的时态算子：Semantics基础语义B,s0

9、=piffp∈L(s0),foratomicpropositionpB,s0

10、=p∧qif