Formalization and specification for controlling process modularity in mobile computing

新的计算模式，普适计算和全局计算，正在作为高度分布式和移动计算的计算模式展现出来。这篇论文探讨了在抽象层面上支持这些新型计算模式的适合的形式化基础，关注在进程移动单位上的控制, 以便在分布式与移动计算环境下更好地协调进程的移动性。 论文的第一部分概述了针对分布式、移动计算的现有进程演算模型中的进程移动单元，并且设计了一种在此方面更优、更具弹性的进程框架。为了表示这种进程框架，我们提出了一种新的、针对移动和分布式系统的进程演算,这种进程演算的优点是动态、弹性的控制进程的移动单元；具体的思路就是扩展π- calculus以及其支持分布式和移动性的变体。我们把这种新的演算叫做Modular π-calculus。我们通过这种演算的提出来说明进程框架提供了一种针对移动进程更为合适的协调机制以及编程模型，例如移动的代理和动态组件载入的支持。之后，我们通过讨论互模拟的几种提法来具体说明能够反映演算设计的进程描述的关键，之后我们讨论了它们的具体性质。 本文的第二部分提出了一个对进程模型的行为和性质进行推理的规约框架。首先，提出了一个对Modularπ-calculus中进程的系统性质进行规约的模态逻辑。为了更好的理解该逻辑，文中对由这个逻辑推出的进程等价的特征进行了研究，并且证明了该逻辑的区分能力介于互模拟和结构一致之间。接下来关于这个规约框架的自动化，本文针对该逻辑和Modular π-calculus的有限控制子集，提出了模型检测算法，并且给出了算法正确性的证明。同时文中贯穿了一些实际且直观的例子，以展现本文提出的一组框架即演算、逻辑和模型算法的有效性。

An Obstacle Cluster Based Data Fusion Method for Mobile Robot

首先给出了一种通过融合多个超声波传感器和一台激光全局定位系统的数据建立机器人环境地图的方法 ,并在此基础上 ,首次提出了机器人在非结构环境下识别障碍物的一种新方法 ,即基于障碍物群的方法 .该方法的最大特点在于它可以更加简洁、有效地提取和描述机器人的环境特征 ,这对于较好地实现机器人的导航、避障 ,提高系统的自主性和实时性是至关重要的 .大量的实验结果表明了该方法的有效性 .

Stabilization of Dynamic Systems for Multiple Omni-Directional Mobile Robots

本文考虑了由2个全方位移动机器人组成的混合动力学系统的协调拟镇定问题.利用机器人位置之间的向量与机器人目标之间向量的内积,设计了多步拟镇定律,该控制律能够在避碰后按指数速率运动到目标点,且在整个过程中两机器人之间的距离不小于避碰的安全距离.最后对2个全方位移动机器人进行了仿真,验证了所给方法的有效性。