Random propagation in complex systems : nonlinear matrix recursions and epidemic spread

This dissertation studies long-term behavior of random Riccati recursions and mathematical epidemic model. Riccati recursions are derived from Kalman filtering. The error covariance matrix of Kalman filtering satisfies Riccati recursions. Convergence condition of time-invariant Riccati recursions are well-studied by researchers. We focus on time-varying case, and assume that regressor matrix is random and identical and independently distributed according to given distribution whose probability distribution function is continuous, supported on whole space, and decaying faster than any polynomial. We study the geometric convergence of the probability distribution. We also study the global dynamics of the epidemic spread over complex networks for various models. For instance, in the discrete-time Markov chain model, each node is either healthy or infected at any given time. In this setting, the number of the state increases exponentially as the size of the network increases. The Markov chain has a unique stationary distribution where all the nodes are healthy with probability 1. Since the probability distribution of Markov chain defined on finite state converges to the stationary distribution, this Markov chain model concludes that epidemic disease dies out after long enough time. To analyze the Markov chain model, we study nonlinear epidemic model whose state at any given time is the vector obtained from the marginal probability of infection of each node in the network at that time. Convergence to the origin in the epidemic map implies the extinction of epidemics. The nonlinear model is upper-bounded by linearizing the model at the origin. As a result, the origin is the globally stable unique fixed point of the nonlinear model if the linear upper bound is stable. The nonlinear model has a second fixed point when the linear upper bound is unstable. We work on stability analysis of the second fixed point for both discrete-time and continuous-time models. Returning back to the Markov chain model, we claim that the stability of linear upper bound for nonlinear model is strongly related with the extinction time of the Markov chain. We show that stable linear upper bound is sufficient condition of fast extinction and the probability of survival is bounded by nonlinear epidemic map.

Formal methods for control synthesis in partially observed environments : application to autonomous robotic manipulation

Modern robots are increasingly expected to function in uncertain and dynamically challenging environments, often in proximity with humans. In addition, wide scale adoption of robots requires on-the-fly adaptability of software for diverse application. These requirements strongly suggest the need to adopt formal representations of high level goals and safety specifications, especially as temporal logic formulas. This approach allows for the use of formal verification techniques for controller synthesis that can give guarantees for safety and performance. Robots operating in unstructured environments also face limited sensing capability. Correctly inferring a robot's progress toward high level goal can be challenging.

This thesis develops new algorithms for synthesizing discrete controllers in partially known environments under specifications represented as linear temporal logic (LTL) formulas. It is inspired by recent developments in finite abstraction techniques for hybrid systems and motion planning problems. The robot and its environment is assumed to have a finite abstraction as a Partially Observable Markov Decision Process (POMDP), which is a powerful model class capable of representing a wide variety of problems. However, synthesizing controllers that satisfy LTL goals over POMDPs is a challenging problem which has received only limited attention.

This thesis proposes tractable, approximate algorithms for the control synthesis problem using Finite State Controllers (FSCs). The use of FSCs to control finite POMDPs allows for the closed system to be analyzed as finite global Markov chain. The thesis explicitly shows how transient and steady state behavior of the global Markov chains can be related to two different criteria with respect to satisfaction of LTL formulas. First, the maximization of the probability of LTL satisfaction is related to an optimization problem over a parametrization of the FSC. Analytic computation of gradients are derived which allows the use of first order optimization techniques.

The second criterion encourages rapid and frequent visits to a restricted set of states over infinite executions. It is formulated as a constrained optimization problem with a discounted long term reward objective by the novel utilization of a fundamental equation for Markov chains - the Poisson equation. A new constrained policy iteration technique is proposed to solve the resulting dynamic program, which also provides a way to escape local maxima.

The algorithms proposed in the thesis are applied to the task planning and execution challenges faced during the DARPA Autonomous Robotic Manipulation - Software challenge.

Information-theoretic Studies and Capacity Bounds: Group Network Codes and Energy Harvesting Communication Systems

Network information theory and channels with memory are two important but difficult frontiers of information theory. In this two-parted dissertation, we study these two areas, each comprising one part. For the first area we study the so-called entropy vectors via finite group theory, and the network codes constructed from finite groups. In particular, we identify the smallest finite group that violates the Ingleton inequality, an inequality respected by all linear network codes, but not satisfied by all entropy vectors. Based on the analysis of this group we generalize it to several families of Ingleton-violating groups, which may be used to design good network codes. Regarding that aspect, we study the network codes constructed with finite groups, and especially show that linear network codes are embedded in the group network codes constructed with these Ingleton-violating families. Furthermore, such codes are strictly more powerful than linear network codes, as they are able to violate the Ingleton inequality while linear network codes cannot. For the second area, we study the impact of memory to the channel capacity through a novel communication system: the energy harvesting channel. Different from traditional communication systems, the transmitter of an energy harvesting channel is powered by an exogenous energy harvesting device and a finite-sized battery. As a consequence, each time the system can only transmit a symbol whose energy consumption is no more than the energy currently available. This new type of power supply introduces an unprecedented input constraint for the channel, which is random, instantaneous, and has memory. Furthermore, naturally, the energy harvesting process is observed causally at the transmitter, but no such information is provided to the receiver. Both of these features pose great challenges for the analysis of the channel capacity. In this work we use techniques from channels with side information, and finite state channels, to obtain lower and upper bounds of the energy harvesting channel. In particular, we study the stationarity and ergodicity conditions of a surrogate channel to compute and optimize the achievable rates for the original channel. In addition, for practical code design of the system we study the pairwise error probabilities of the input sequences.

Rule-based grapheme-to-phoneme method for the Greek

This paper describes a trainable method for generating letter to sound rules for the Greek language, for producing the pronunciation of out-of-vocabulary words. Several approaches have been adopted over the years for grapheme-to-phoneme conversion, such as hand-seeded rules, finite state transducers, neural networks, HMMs etc, nevertheless it has been proved that the most reliable method is a rule-based one. Our approach is based on a semi-automatically pre-transcribed lexicon, from which we derived rules for automatic transcription. The efficiency and robustness of our method are proved by experiments on out-of-vocabulary words which resulted in over than 98% accuracy on a word-base criterion.

Use of contexts in language model interpolation and adaptation

Language models (LMs) are often constructed by building multiple individual component models that are combined using context independent interpolation weights. By tuning these weights, using either perplexity or discriminative approaches, it is possible to adapt LMs to a particular task. This paper investigates the use of context dependent weighting in both interpolation and test-time adaptation of language models. Depending on the previous word contexts, a discrete history weighting function is used to adjust the contribution from each component model. As this dramatically increases the number of parameters to estimate, robust weight estimation schemes are required. Several approaches are described in this paper. The first approach is based on MAP estimation where interpolation weights of lower order contexts are used as smoothing priors. The second approach uses training data to ensure robust estimation of LM interpolation weights. This can also serve as a smoothing prior for MAP adaptation. A normalized perplexity metric is proposed to handle the bias of the standard perplexity criterion to corpus size. A range of schemes to combine weight information obtained from training data and test data hypotheses are also proposed to improve robustness during context dependent LM adaptation. In addition, a minimum Bayes' risk (MBR) based discriminative training scheme is also proposed. An efficient weighted finite state transducer (WFST) decoding algorithm for context dependent interpolation is also presented. The proposed technique was evaluated using a state-of-the-art Mandarin Chinese broadcast speech transcription task. Character error rate (CER) reductions up to 7.3 relative were obtained as well as consistent perplexity improvements. © 2012 Elsevier Ltd. All rights reserved.

When is `partial' adequate? A logic-based proof technique using partial specifications

A technique is presented for ascertaining when a (finite-state) partial process specification is adequate, in the sense of being specified enough, for contexts in which it is to be used. The method relies on the automatic generation of a modal formula from the partial specification; if the remainder of the network satisfies this formula, then any process that meets the specification is guaranteed to ensure correct behavior of the overall system. Using the results, the authors develop compositional proof rules for establishing the correctness of networks of parallel processes and illustrate their use with several examples

ISO 2022的有限状态机描述

ISO 2022编码体系对字符集国家标准的制订有很大影响,然而标准条款存在不确定性,有时难于理解。本文引入有限状态机(FSM)模型来形式化地刻画ISO 2022的特征。针对FSM五元组,详细说明了其状态空间的构成,提出了输入字母表的等效分类方法,给出了初始状态以及终结状态集合,分析了状态转移函数的规模,并采用FSM描述方法分析了ISO-2022-CN、EUC-CN、复合文本等标准,揭示了这些标准与ISO 2022的内在联系。这些工作有助于ISO 2022标准符合性检测、扩展标准的制订与系统实现复杂度评估。鉴于形式化描述方法在编码字符集标准领域未得到广泛应用,本文工作为该类研究引入了新的思路和方法。

事件驱动的BPEL引擎架构设计与实现

WS-BPEL(Web Service Business Process Execution Language，简称BPEL)是Web服务规范族中服务复合层的重要标准。BPEL支持通过对Web服务的编制(Orchestration)来构建业务流程，从而使编程人员能够集中关注业务逻辑。BPEL引擎系统是一个支持BPEL语言描述的业务流程运行的服务器中间件系统，使用BPEL引擎可以执行BPEL语言编写的业务流程。作为一个网络服务器系统，BPEL引擎将不可避免的处理大量的并发请求。如何设计实现BPEL引擎使之能高效的处理并发将是高性能BPEL引擎设计的关键问题。 并发服务器系统通常采用多线程和事件驱动两种并发模型。传统上大多数服务器软件都建立在多线程(或多进程)模型的基础上。但在高负载条件下，过多的线程和线程间的上下文切换会造成系统较大的开销，这些开销是导致系统性能下降的主要原因。事件驱动模型是一种只采用少量固定数量线程的并发模型，一般说来，它的伸缩性更好，并且有更高的处理效率。 本文对高并发服务器系统中所使用的事件驱动模型进行了分析和研究，并且结合BPEL语言规范的特点，提出了事件驱动的BPEL引擎实现技术方案。论文重点研究了BPEL事件结构和有限状态机(Finite State Machine，简称FSM)刻画BPEL流程和活动行为的原理，针对BPEL语言语法特点，构造了完整的BPEL FSM模型，包括了状态空间和基于ECA(Event-Condition-Action)模式的状态转移规则。 在基于事件驱动模型的BPEL引擎架构原理的指导下，我们设计并实现了基于事件驱动模型的OnceBPEL2.0引擎系统。并且，我们对采用多线程模型实现的OnceBPEL1.0系统和采用事件驱动模型实现的OnceBPEL2.0系统进行了性能测试和分析比较。从我们的测试数据和分析结果可以看出，采用事件驱动模型的OnceBPEL2.0系统比采用多线程模型的OnceBPEL1.0有了较大的性能提升。

生成诊断公式的有限状态进程等价验证

分析有限状态进程互模拟等价判定技术,探讨了诊断公式的生成问题。给出了将有限状态进程转化为带标号的迁移系统,修改了Paige和Trajan求解最粗划分的算法,使其适用于带标号的迁移系统。给出生成Hennessy-Milner逻辑描述的诊断公式的算法,当两个进程不能互模拟时,产生两个诊断公式。算法的时间复杂度为O(mlogn),空间复杂度为O(m+n)。

一种输电线路巡检机器人控制系统的设计与实现

介绍了一种超高压输电线路巡检机器人控制系统的设计与实现方法.根据巡检作业任务的要求,采用遥控与局部自主相结合的控制模式实现巡检机器人沿线行走及跨越障碍.设计了巡检机器人有限状态机模型,实现了机器人遥控与局部自主控制的有机结合.采用基于激光传感器定位的方法实现了巡检机器人的自主越障控制.实验结果表明,该机器人可实现沿线行走及自主跨越障碍,从而验证了控制系统设计的有效性与合理性.

基于有限状态机的空间对接仿真平台控制系统设计

给出了一种基于分层式有限状态机的五自由度空间对接仿真平台控制系统设计方法,对状态机进行了扩展定义.增加了一个定义于状态上的变量属性集合,使其有利于系统的代码实现.结合控制系统采用的10 ms定时中断机制,将状态机层次划分到了可以分析每个10 ms硬件中断程序所需实现的控制功能状态及其转移、继承关系的程度,可以更清晰地设计出中断程序所需要的构成结构.系统的实际应用结果证明了上述方法的有效性.

基于有限状态机与Petri网的系统分析与设计

从系统组成、功能需求和体系结构方面介绍了航天器空间对接仿真系统的实时多任务控制系统,基于有限状态机和Petri网方法对其进行了单任务级和多任务级的分析建模,并以此为基础完成系统的详细设计,其中应用分叉和资源共享模型实现了系统的同步和互斥问题。实际应用中应用工程化和模块化的方法完成系统设计,系统运行性能良好。试验证明这种分析设计方法合理可行。

双足爬壁机器人壁面凹过渡步态规划研究

针对腿足式爬壁机器人在壁面过渡时的步态规划问题,以一种真空吸附式双足爬壁机器人为研究对象,在步态分析的基础上,基于有限状态机建立了机器人的步态模型,进而提出了基于加权插值和BP神经网络的双足爬壁机器人壁面凹过渡在线步态规划算法,为提高机器人壁面过渡的自主控制能力奠定了基础.仿真分析和实验结果表明,该步态规划算法对于实际的机器人系统是有效的和可行的.

一个面向复杂任务的多机器人分布式协调系统

基于多智能体系统理论，研讨在非结构，不确定环境下面向复杂任务的多机器人分布式协调系统的实现原理，方法和技术。提出的递阶混合式协调结构，基于网络的通讯模式和基于有限状态机的规划与控制集成方法，充分考虑了复杂任务和真实自然环境的特点，通过构建一个全实物的多移动机器人实验平台，对规划，控制，传感，通讯，协调与合作的各关键技术进行了开发和集成，使多机器人分布式协调技术的研究直接面向实际应用，编队和物料搬运的演示实验结果展示了多机器人协调技术的广阔应用前景。

自主/遥控水下机器人水面/水下通信协议设计与实现

为了解决自主/遥控水下机器人（ARV）水面控制台与水下载体之间的通信问题，设计并实现了一种基于分层结构的水面/水下通信协议。该协议根据ARV 通信特殊需求，分为应用层，数据链路层与物理层，各层之间通过事件路由的方式进行调用，层内协议规则通过有限状态机来描述，整个协议结构清晰。ARV 实验结果证明这一通信协议具有传输速率快，可靠性高等优点。