CorrectReactiveHighLevelRobotControl阅读报告.ppt

阅读报告,Correct,Reactive,High-LevelRobotControlMitigatingtheStateExplosionProblemofTemporalLogicSynthesis缓解时序逻辑合成的状态空间爆炸问题,主要涉及的知识背景：1、自动机2、LTL线性时序逻辑，克里普克结构3、多层次的协同方法4、模拟与互模拟5、抽象的粒度6、滚动时域框架,综述：本文通过以美国国防部高级研究计划局举办的城市挑战赛为例引机器人控制中存在的问题，进而介绍模拟和互模拟来保证抽象的解决方案与连续执行的一致性。但是，同时导致计算复杂度加大，文中主要介绍抽象粒度和状态空间的关系，并介绍了解决状态空间爆炸的方法：1、使用粒度大的抽象，并将任务分解成互不相交的四个自动机以进一步降低复杂度；2、使用粒度小的抽象，使用滚动时域框架来降低复杂。,Robotsthesedaysfeatureatightinterplaybetweencomputationalandphysicalcomponents.现今，机器人的计算和物理部件之间有着紧密的相互作用。,举例：DARPAUrbanChallenge在城市挑战赛中，参赛车辆需要在全自动控制下，在模拟城市的场景中识别静/动态的障碍物，执行不同的任务（如在不同路况的环境中，在遵守当地交通法规的前提条件下完成驾驶，泊车，到达指定地域等操作）。在执行这些任务的同时，智能车也许满足底层物理部件和实际动作的局限性（如，不可能达到超出发动机的极限的速度，不可能实现瞬间的大角度转弯）。因此，关于控制车辆行为的高层逻辑需要适当的集成到底层的控制器中。,现存在的问题：系统是通过某种特定的方法将计算和物理部件紧密耦合在一起。即使单个部件通过大量的测试和形式化验证满足正确性，但是，整个系统的复杂度已经超出了形式化验证的承受能力，同时迫使人们放弃大部分的测试。如在2007年参加城市挑战赛的车辆”Alice”在研发期间经过了上千小时的模拟和300英里的现场测试。但是一旦发现一个问题未覆盖到再修改底层的特定设计是不可能的。最终导致取消Alice的挑战资格。因此，要想实现智能车和机器人的自主调度，需要经过形式化验证并设计期结构合理的嵌入式控制器。并使用形式化语言(如LTL)说明规范，以说明其在所有有效环境参数下的行为。,一、实施上述方案的通常步骤为：1、构造一个基于底层物理系统的有穷状态的抽象2、制定满足高层逻辑规范的自动机控制策略。二、上述的步骤导致控制机构的分层（类似于混合型系统）1、高层离散的事件2、底层控制器连续的执行。三、模拟和互模拟验证了连续的执行确保了离散事件的正确性。但是上述的方法将导致庞大的计算复杂度。四、为此，文章描述了两种缓解状态空间爆炸的方法1、coarseabstraction基于低层控制器，通过RNDF和MDF文件，考虑所有可能的情况，以及相应的操作。2、fine-abstraction使用滚动时域的方法，对未来较短时间段的事件作出预判，并根据实时感受器接收到的信息对控制信息进行修正。,Background:,我们先将问题抽象成离散的时间，再在物理层面上对于机器人的动作和反应生成连续的控制。为了方便进步的论述，这里先介绍几个基础的背景知识。,这个自动机表示了一个机器人控制问题的离散事件。传感器的信息对应了六元组的输入字母表，机器人的动作和反应对应输出字母表。,1、automata这里我们使用自动机的概念并不是太贴切，因为我们并没有定义通常的接收状态。更精确的说应该是”KripkeStructure”。1、是有穷状态集2、为初始状态集3、是输入字母表4、是输出字母表5、是状态转换函数6、是输出函数,2、LinearTemporalLogicLTL=原子命题+时间轴+时态算子Inlogic,lineartemporallogicorlinear-timetemporallogic(LTL)isamodaltemporallogicwithmodalitiesreferringtotime.线性时序逻辑是基于时间的形式化时序逻辑。ItisafragmentofthemorecomplexCTL*,whichadditionallyallowsbranchingtimeandquantifiers.它可以看做更为复杂的CTL*的一个分支。本文将使用LTL作为形式化表示来定义机器人高层,反馈的行为.从广义上来说,LTL允许原子命题的真值随着时间的推移而改变.递归定义的LTL的语法如下，其中是一个原子命题组中的AP(所有原子命题和他们的否定命题的集合)，其中还包括真与假命题。,基本的时态算子：,Semantics基础语义B,s0|=piffpL(s0),foratomicpropositionpB,s0|=pqiffB,s0|=pandB,s0|=qB,s0|=piffitisnotthecasethatB,s0|=pB,s0|=pUqiffj.(sj|=qandkj(sk|=p)B,s0|=Xpiffs1|=pB,s0|=Fpiffj.(sj|=p)B,s0|=Gpiffj.(sj|=p),LTLSynthesisSynthesizinganLTLformulareferstotheprocessofautomaticallygeneratinganautomatonAsuchthat,foreveryinfiniterunoftheautomaton,thebehavioroftherunsatisfiestheformula.LTL合成指自动生成自动机A的过程，自动机在无穷，连续的控制行为总是满足定义的公式。,ifthespecificationisrestrictedtoasubsetofLTL,thecomplexitybecomespolynomialinthestatespace随机的合成LTL公式已经被证明复杂度太高。但是，如果将规格限定在LTL的一个子集，那么复杂度就变成一个关于状态空间的多项式。,SpecificationandControlSynthesisofRoboticTasks,Wenowdiscusshowtheseformalmethodsareusedwithinthecontextofcorrect-by-construction,high-levelrobotcontrol.Wewillusethefollowingexampletoillustratethetechniquesandtradeoffs.我们现在将讨论在这个结构正确，高层机器人控制器的范围内如何使用这些形式化方法。我们将用下面几个事例来说明它的技术和局限。,Example1以DUC为例，智能车重要的属性是自动避开障碍物，遵守当地的交通法规（如靠右车道行驶），到达指定的区域等，而这些属性需要被形式化表示出来。将物理世界连续无穷的动作抽象成由诸多原子命题和有穷状态组成的模型。以智能车为例，主要涉及3个命题：1、SensorpropositionsSi(abstracttheperceptionsystemoftherobotandprovideinformationabouttheenvironment)2、Locationpropositionsri(abstractthepositionoftherobotinworkspace)3、Actionpropositionsai(abstractactiontherobotperform)Si是环境行为，机器人无法控制它们的值，ri,si表示机器人控制行为,Example2,如左图所示，图a为对路况的粒度大的抽象，它只是粗略的将道路情况抽象为路段R1，R2，R3，R4而将交叉路段抽象为I1，I2。图b为对双向单车道道路的粒度小的抽象，它只是精细的将道路情况抽象为一个个的单元。如C1,1，C2,1，C3,1可以看做一小段道路的切片，C1,1表示右车道，C2,1表示中间黄虚线，C3,1表示左车道。这里主要是对感知原子命题的抽象。该命题状态的改变只与当前周边环境有关，不受控制器的影响。,Example1假设环境命题的集合为：机器人控制的原子命题集合：一旦任务被抽象为原子命题的组合。那么机器人任务可以被写为给定结构的LTL公式的组合。这些形式化公式包括：1、周边环境和机器人状态的初始化2、机器人在区域转化时的运动操作3、设定环境命题所有可能的行为4、机器人行为的限制，条件，目标,Example2我们将简单的介绍用不同粒度来抽象自动驾驶问题用形式化方法如何描述：1、coarseabstractionR1表示机器人在R1路段行驶STOP表示机器人停止RoadBlocked表示堵车(环境命题)RedLight表示前方为红灯(环境命题)用LTL语言来描述几个基本的行为如下：,2、fineabstraction如上图所示：C1,1，C1,2.C1,L表示右车道，C2,1，C2,2.C2,L表示中间黄虚线，C3,1，C3,2.C3,L表示左车道。Ci,j就代表马路上的一个单元。而Oi,j表示在Ci,j区域有障碍物。用LTL语言来描述几个基本的行为如下：,下图表示在粒度小的抽象中，当C1,3单元存在障碍物时，自动机的执行情况。,2、FromDiscreteSolutiontoContinuousExecution满足LTL公式的自动机需要用混合控制器实现实际的功能操作1、自动机对机器人状态进行初始化，如当前位置，当前所需执行的操作，当前的环境条件等。2、根据迭代环境命题的值来确定机器人的下一状态和下区域。3、低层控制器连续的执行操作，驱使机器人到达下一区域。若在此过程中机器人出现了并未在当前区域和下一区域的状态，说明实际环境状况超出了原先设定的环境命题的集合。控制器将报错停止运行。,左图为对混合型机器人控制连续执行离散事件的算法描述。根据环境命题的值来判定机器人下一状态和下一所在区域（达到下一区域的过程是连续的）。,SimulationandBisimulationKripke结构:设AP是一个原子命题集合,AP上的Kripke结构是一个四元组,其中:S是状态的有限集合;是初始状态集合;是状态迁移关系;是标记函数,该函数把状态sS映射到AP的一个子集,该集合包含S中所有为真的原子命题。M可用一个有根的、带标记的有向图表示。图的结点集合为S,边的集合为R,结点的标记为L,根集合为S0。,模拟(Simulation):和是AP上的两个Kripke结构,关系是M1和M2之上的一个模拟关系,如果(1)(2)对于(s1,s2)H,下列条件成立:对M1中的每一个状态迁移关系,M2中都存在一个对应的状态迁移关系。则称M2模拟M1,记做模拟关系是模型之间的一种偏序关系,具有自反性和传递性。,互模拟(Bisimulation):和是AP上的两个Kripke结构,关系是M1和M2之上的一个模拟关系,如果(1)(2)则称M1和M2是互模拟的,记做互模拟是模型之间的一种等价关系,具有自反性、对称性和传递性。可以保证抽象的离散空间与实际连续世界的等价性。,形式化方法的主要挑战1、找到合适的抽象使问题可以用离散的事件说明并能正确地连续执行2、状态空间爆炸问题这两个问题是紧密联系的。当抽象粒度越小，则状态空间越紧凑；反之亦然,CoarseAbstractionsSynthesizingtheFullController,采用粗粒度抽象和一组鲁棒，连续，反馈控制器，将所有可能的环境行为与机器人行为写入，如通过十字路口，躲避障碍物和堵塞路段，到达指定检查点，紧急刹车等。我们将任务分解为四个互不相交的部分，然后，各自独立的生成自动机，最后由四个自动机组合生成正确的动作。,图五为DUC的国家资格赛的A区域模型，机器人尽可能多的经过两个检查点。图B中，当机器人遭遇障碍时，在等待了预定时间片后，就使用备用路径行驶。,图六表示机器人在国家资格赛C区域的行为。蓝色方块表示智能车。当到达十字路口时，机器人先停止，等待绿色车辆通过后再行驶穿过十字路口。,FineAbstraction:RecedingHorizonFramework,这里我们用事例1来说明状态空间爆炸的问题。假设一辆车从C1,1开始行驶，目标是到达Ci,L。对于这个问题，系统计算的可能状态有.计算的复杂度是随着L的增加成指数型增长。而在机器人任务中，L的值将使状态数指数爆炸。但是，机器人在执行任务时，计算整个执行路径中所有的状态时没有必要的，就像我们日常生活中，一辆几公里之外迎面而来的车辆不会对我们当前的行驶路径有影响。所以可以使用使用滚动时域框架来降低复杂度。通俗的说就是并不在运行的开始计算从开始区域到目标区域所有的路径。而是缩小前瞻的距离，指计算从当前位置开始一段距离的可能路径。假设设定一个前瞻距离为l,那么状态数为，当设定前瞻长度为2时，无论L的取值为多少，它的状态空间大小为384。而如果不是用滚动时域的话，当L=100，状态空间大小为：，由此可见滚动时域框架可以有效的解决状态空间爆炸问题。而且此处还未考虑交叉路口，否则状态空间将要更加的庞大。,滚动时域：滚动时域是在每个采样时刻，它对该时刻起的一个有限区间进行优化，在下一时刻到来时，将优化区间向前滚动一个时刻，按照相同的方法进行优化。滚动时域在静态的状况下虽然得到