Compositional hierarchical monitoring automaton construction for LTL

In this paper we give a compositional (or inductive) construction of monitoring automata for LTL formulas. Our construction is similar in spirit to the compositional construction of Kesten and Pnueli [5]. We introduce the notion of hierarchical Büchi automata and phrase our constructions in the framework of these automata. We give detailed constructions for all the principal LTL operators including past operators, along with proofs of correctness of the constructions.

基于SAT的LTL限界模型检测与验证

模型检测是一种自动验证有限状态系统的形式化方法。状态爆炸问题是模型检测面临的主要挑战，限界模型检测是缓和状态空间爆炸限制的手段之一。该方法通常对限界模型和性质进行编码而转化成SAT问题，依次增加限界值以寻找反例或者无法找到反例而得证。限界模型检测方法往往查错迅速。 基于SAT的限界验证方法是限界模型检测的一个分支。它与限界模型检测的不同在于它不是查找反例，而是验证性质的反命题在限界模型上不可成立。相比于限界模型检测，该方法对于正确性质的验证有时会快许多。但是它不能用来验证含有G算子的LTL公式。鉴于此，我们选取一部分包含G算子的LTL公式。然后在这个公式集合上构造出新的限界验证编码。并且证明了对于该LTL公式子集，我们的编码是可靠并且完备的。新编码可以作为限界验证的一个补充。

时间自动机关于LTL性质的符号化模型检测工具及其改进

许多系统需要在规定时间内响应外部发生的事件，并迅速完成对事件的处理，这样的系统称之为实时系统。实时系统经常出现在与生命财产安全息息相关的领域，如果无法及时响应外部事件，可能会造成十分严重的后果。如何保证实时系统的正确性、可靠性受到越来越广泛的关注。 模型检测是一种对系统进行形式化验证的算法，它可以自动的在模型状态空间中搜索不满足规范的路径或状态，设计者可以根据找到的反例修改系统设计，进而提高系统的可靠性。模型检测方法的主要瓶颈是状态爆炸，符号化方法和抽象是延缓状态爆炸发生的重要手段。 时间自动机是一种使用广泛的描述实时系统的数学模型， 时序逻辑LTL是是一种常用的针对实时和并发系统的规范语言，本文主要研究了时间自动机关于LTL性质的符号化模型检测方法，并实现了相应的模型检测工具CTAV。 CTAV以DBM作为表示符号化状态的数据结构，使用DBM的操作和运算完成符号化状态的生成、存储及比较等，它通过on-the-fly的方法在生成系统符号化状态空间的同时进行性质的检测。 本文还研究了最大上下界抽象等在模型检测中的使用，比较了不同的抽象在LTL模型检测中的效果。此外还针对符号化状态的特点，对模型检测过程进行了改进，避免了不必要的状态展开。 为了方便建模，CTAV对UPPAAL模型描述语言进行了支持，并针对检测过程中变量存储的各种情况，设计了一次索引和二次索引的方法提高读写变量的速度。

带时间约束的LTL公式的模型检测技术及工具实现

实时系统是能够在指定或确定的时间内完成事件处理的计算机应用系统，它的正确性不仅依赖于系统计算的逻辑结果，还依赖于产生这个结果的时间。实时系统在国防以及工业控制等领域的到广泛应用，为保证系统的正确性和可靠性，使用模型检测方法对其进行检测十分重要。 时间自动机是对实时系统进行建模的一种形式化方法，线性时序逻辑（LTL）是当前常用的描述性质的时序逻辑。CTAV是国际上目前唯一的可对时间自动机直接进行线性时序逻辑性质验证的符号化模型检测工具，但CTAV还不能直接检测带时间约束的线性时序逻辑性质，如果要检测带时间约束的线性时序逻辑性质，需要使用者通过手动构造test时间自动机来实现，这增加了使用者的困难。 为了验证时间自动机M是否满足一个带时间约束的线性时序逻辑q， 本文首先在LTL公式转化Büchi自动机的基础上给出了将带时间约束的LTL公式q转化为时间Büchi自动机Bq的方法，其次针对由性质转化而来的时间Büchi自动机Bq（性质自动机）的特点，本文给出了一个构造乘积自动机M*Bq的过程，使得可将验证M是否满足的问题化归为乘积自动机M*Bq的空性检测问题，由于乘积自动机M*Bq是一个时间Büchi自动机，这样通过调用CTAV中以前已实现的关于时间Büchi自动机的空性检测过程就得到了带时间约束的线性时序逻辑关于时间自动机的一个模型检测过程。此外还修改了LU的计算过程，最后给出了实验数据对比，得到了一个比较好的实现方法。 本文还完善了CTAV对UPPAL模型描述语言中函数成分的支持，以及模型检测完成后反例的输出，方便用户对模型的修改和完善。

An examination of the development of LTL hub-and-spoke freight distribution systems

Over recent years, hub-and-spoke distribution techniques have attracted widespread research attention. Despite there being a growing body of literature in this area there is less focus on the spoke-terminal element of the hub-and-spoke system as being a key component in the overall service received by the end-user. Current literature is highly geared towards discussing bulk optimization of freight units rather than to the more discrete and individualistic profile characteristics of shared-user Less-than-truckload (LTL) freight. In this paper, a literature review is presented to review the role hub-and-spoke systems play in meeting multi-profile customer demands, particularly in developing sectors with more sophisticated needs, such as retail. The paper also looks at the use of simulation technology as a suitable tool for analyzing spoke-terminal operations within developing hub-and spoke systems.

A simulation analysis of spoke-terminals operating in LTL Hub-and-Spoke freight distribution systems

DUE TO COPYRIGHT RESTRICTIONS ONLY AVAILABLE FOR CONSULTATION AT ASTON UNIVERSITY LIBRARY AND INFORMATION SERVICES WITH PRIOR ARRANGEMENT The research presented in this thesis is concerned with Discrete-Event Simulation (DES) modelling as a method to facilitate logistical policy development within the UK Less-than-Truckload (LTL) freight distribution sector which has been typified by “Pallet Networks” operating on a hub-and-spoke philosophy. Current literature relating to LTL hub-and-spoke and cross-dock freight distribution systems traditionally examines a variety of network and hub design configurations. Each is consistent with classical notions of creating process efficiency, improving productivity, reducing costs and generally creating economies of scale through notions of bulk optimisation. Whilst there is a growing abundance of papers discussing both the network design and hub operational components mentioned above, there is a shortcoming in the overall analysis when it comes to discussing the “spoke-terminal” of hub-and-spoke freight distribution systems and their capabilities for handling the diverse and discrete customer profiles of freight that multi-user LTL hub-and-spoke networks typically handle over the “last-mile” of the delivery, in particular, a mix of retail and non-retail customers. A simulation study is undertaken to investigate the impact on operational performance when the current combined spoke-terminal delivery tours are separated by ‘profile-type’ (i.e. retail or nonretail). The results indicate that a potential improvement in delivery performance can be made by separating retail and non-retail delivery runs at the spoke-terminal and that dedicated retail and non-retail delivery tours could be adopted in order to improve customer delivery requirements and adapt hub-deployed policies. The study also leverages key operator experiences to highlight the main practical implementation challenges when integrating the observed simulation results into the real-world. The study concludes that DES be harnessed as an enabling device to develop a ‘guide policy’. This policy needs to be flexible and should be applied in stages, taking into account the growing retail-exposure.

Preliminary assessment of the artisanal fishery sector around Lac Maï-Ndombe in the Lac Tele-Lac Tumba (LTL) CARPE Landscape

The WorldFish Center was contracted by the World Wide Fund for Nature (WWF) to lead a preliminary assessment of the Lac Maï-Ndombe fishery, one of three water bodies for which such an assessment will be completed in the Lac Tele-Lac Tumba Landscape of the CARPE program. Between Aug.29-Sept.5, 2007, a joint WorldFish Center-WWF team traveled to Lac Maï-Ndombe in Bandundu Province, and conducted an analysis of the conditions surrounding the fishery and fisherfolk livelihoods in a total of 19 villages and camps. Included in this assessment were preliminary analyses of market-chain networks and stakeholders’ receptivity to NGO capacity-building to improve commercialization of fish catches and/or to introduce local fisheries management regimes. While perceptions of declining fish stocks prevail, the absence of changes in reported fish sizes bring into doubt any urgent need for fishery management interventions. However, lacking scientific fish population structure data the team would not recommend any NGO interventions to increase fishing effort. Lac Maï-Ndombe fisherfolk have highly diversified levels of dependence on fishing, and while there is evidence that some stakeholder groups are flourishing, the majority of the fishery appears to be characterized by a livelihood insecurity and a lack of capital. This limits fishers’ abilities to negotiate with transporters and with Kinshasa-based market brokers, and in combination with a heavy burden of rent-seeking behavior by civil servants, this condition forces over half of the fishers to sell their fish and buy all manufactured products through local intermediaries at disadvantageous prices.

DCAF4, a novel gene associated with leucocyte telomere length

Background Leucocyte telomere length (LTL), which is fashioned by multiple genes, has been linked to a host of human diseases, including sporadic melanoma. A number of genes associated with LTL have already been identified through genome-wide association studies. The main aim of this study was to establish whether DCAF4 (DDB1 and CUL4-associated factor 4) is associated with LTL. In addition, using ingenuity pathway analysis (IPA), we examined whether LTL-associated genes in the general population might partially explain the inherently longer LTL in patients with sporadic melanoma, the risk for which is increased with ultraviolet radiation (UVR). Results Genome-wide association (GWA) meta-analysis and de novo genotyping of 20 022 individuals revealed a novel association (p=6.4×10−10) between LTL and rs2535913, which lies within DCAF4. Notably, eQTL analysis showed that rs2535913 is associated with decline in DCAF4 expressions in both lymphoblastoid cells and sun-exposed skin (p=4.1×10−3 and 2×10−3, respectively). Moreover, IPA revealed that LTL-associated genes, derived from GWA meta-analysis (N=9190), are over-represented among genes engaged in melanoma pathways. Meeting increasingly stringent p value thresholds (p<0.05, <0.01, <0.005, <0.001) in the LTL-GWA meta-analysis, these genes were jointly over-represented for melanoma at p values ranging from 1.97×10−169 to 3.42×10−24. Conclusions We uncovered a new locus associated with LTL in the general population. We also provided preliminary findings that suggest a link of LTL through genetic mechanisms with UVR and melanoma in the general population.

Identification of seven loci affecting mean telomere length and their association with disease

Interindividual variation in mean leukocyte telomere length (LTL) is associated with cancer and several age-associated diseases. We report here a genome-wide meta-analysis of 37,684 individuals with replication of selected variants in an additional 10,739 individuals. We identified seven loci, including five new loci, associated with mean LTL (P < 5 x 10(-8)). Five of the loci contain candidate genes (TERC, TERT, NAF1, OBFC1 and RTEL1) that are known to be involved in telomere biology. Lead SNPs at two loci (TERC and TERT) associate with several cancers and other diseases, including idiopathic pulmonary fibrosis. Moreover, a genetic risk score analysis combining lead variants at all 7 loci in 22,233 coronary artery disease cases and 64,762 controls showed an association of the alleles associated with shorter LTL with increased risk of coronary artery disease (21% (95% confidence interval, 5-35%) per standard deviation in LTL, P = 0.014). Our findings support a causal role of telomere-length variation in some age-related diseases.

Estudio del crecimiento del camarón de agua dulce (M rosenbergu), en condiciones semi-intensivas en la comunidad de Alos Encuentros, Municipio de Limay, Esteli

Con el propósito de determinar el comportamiento de rasgos de crecimiento del camarón de agua dulce M. rosenbergii. Se montó un ensayo en la comunidad de los Encuentros, municipio de Limay, Estelí. Para tal efecto se utilizaron tres estanques de tierra de 200m 3 c/u en los que se sembraron 5 post larvas/m2. La alimentación fue a base de concentrado con 35%, 25%, 20% de proteína respectivamente de manera igual para los tres estanques. Se efectuaron muestreos, de talla, peso con respecto a la edad siendo estos el primer muestreo al momento de la siembra el segundo a los 30 días y los restantes cada 20 días, hasta los 190 días que culminó el ensayo, para determinar el crecimiento de los camarones de agua dulce M. rosenhergií mediante análisis estadísticos se empleó el modelo no lineal sugerido por Pearl-read (1923) y = k/1+bea:. Para realizar un menor ajuste de los datos se procedió a linealizarlos por medio de una regresión con la ecuación: Ln (k/y)-1 = Lnb±ax. Para el primer estanque se construyó el modelo Ln(k/y)-1 = 6.69459 = 0.97948 (cm), el error estándar para Lnb y a son de 0.338010.57300 respectivamente, laPr> ltl iguala 1.0001con r2 = 0.976605 y C.V= 29.66412. En el segundo estanque se obtuvo Ln(kly)-1 = 6.53469- 0.89897 (cm) el error standard para Lnb y a son de 0.4235;0.6858. La Pr > ltl para ambos son de 0.0001 con r1 = 0.96084 y C.V= 36.20477, para el tercer estanque se tiene valores de Ln (k/y)-1 = 6.93459- 1.116595 (cm) con error standard de Lnb y a = 1.04923; 0.180752 y para Pr > ltl fue de 0.0003;0.0005 con un r2= 0.8450 y C.V = 126.7102, al hacer un análisis de regresión combinando los tres estanques se obtuvo valores deLn(k/y)-1 = 5.5224-0.8068 (cm) con errores standard de Lnb y a= O.2878; 0.480 y para Pr > ltl fue de 0.0001 con un r2=; 0.9700 y C.V = 31.489, el comportamiento de crecimiento de los camarones de agua dulce M. rosenbergii sometidos a estudio bajo las mismas condiciones de cultivo tuvieron diferencias de talla y peso siendo éstas de 0.331 cm; 2.S02 g. del estanque 2 vs estanque 1; 1.093 cm, 4.3500 g del estanque 2 vs estanque 3 y 0.762 cm; 1.848 g para el estanque 1 vs estanque 3, sin embargo para los estanques en estudio se observó un aumento de talla y peso entre los 110-130 días de edad.

Design, specification, and synthesis of aircraft electric power systems control logic

Cyber-physical systems integrate computation, networking, and physical processes. Substantial research challenges exist in the design and verification of such large-scale, distributed sensing, ac- tuation, and control systems. Rapidly improving technology and recent advances in control theory, networked systems, and computer science give us the opportunity to drastically improve our approach to integrated flow of information and cooperative behavior. Current systems rely on text-based spec- ifications and manual design. Using new technology advances, we can create easier, more efficient, and cheaper ways of developing these control systems. This thesis will focus on design considera- tions for system topologies, ways to formally and automatically specify requirements, and methods to synthesize reactive control protocols, all within the context of an aircraft electric power system as a representative application area.

This thesis consists of three complementary parts: synthesis, specification, and design. The first section focuses on the synthesis of central and distributed reactive controllers for an aircraft elec- tric power system. This approach incorporates methodologies from computer science and control. The resulting controllers are correct by construction with respect to system requirements, which are formulated using the specification language of linear temporal logic (LTL). The second section addresses how to formally specify requirements and introduces a domain-specific language for electric power systems. A software tool automatically converts high-level requirements into LTL and synthesizes a controller.

The final sections focus on design space exploration. A design methodology is proposed that uses mixed-integer linear programming to obtain candidate topologies, which are then used to synthesize controllers. The discrete-time control logic is then verified in real-time by two methods: hardware and simulation. Finally, the problem of partial observability and dynamic state estimation is ex- plored. Given a set placement of sensors on an electric power system, measurements from these sensors can be used in conjunction with control logic to infer the state of the system.

Control of dynamical systems with temporal logic specifications

This thesis is motivated by safety-critical applications involving autonomous air, ground, and space vehicles carrying out complex tasks in uncertain and adversarial environments. We use temporal logic as a language to formally specify complex tasks and system properties. Temporal logic specifications generalize the classical notions of stability and reachability that are studied in the control and hybrid systems communities. Given a system model and a formal task specification, the goal is to automatically synthesize a control policy for the system that ensures that the system satisfies the specification. This thesis presents novel control policy synthesis algorithms for optimal and robust control of dynamical systems with temporal logic specifications. Furthermore, it introduces algorithms that are efficient and extend to high-dimensional dynamical systems.

The first contribution of this thesis is the generalization of a classical linear temporal logic (LTL) control synthesis approach to optimal and robust control. We show how we can extend automata-based synthesis techniques for discrete abstractions of dynamical systems to create optimal and robust controllers that are guaranteed to satisfy an LTL specification. Such optimal and robust controllers can be computed at little extra computational cost compared to computing a feasible controller.

The second contribution of this thesis addresses the scalability of control synthesis with LTL specifications. A major limitation of the standard automaton-based approach for control with LTL specifications is that the automaton might be doubly-exponential in the size of the LTL specification. We introduce a fragment of LTL for which one can compute feasible control policies in time polynomial in the size of the system and specification. Additionally, we show how to compute optimal control policies for a variety of cost functions, and identify interesting cases when this can be done in polynomial time. These techniques are particularly relevant for online control, as one can guarantee that a feasible solution can be found quickly, and then iteratively improve on the quality as time permits.

The final contribution of this thesis is a set of algorithms for computing feasible trajectories for high-dimensional, nonlinear systems with LTL specifications. These algorithms avoid a potentially computationally-expensive process of computing a discrete abstraction, and instead compute directly on the system's continuous state space. The first method uses an automaton representing the specification to directly encode a series of constrained-reachability subproblems, which can be solved in a modular fashion by using standard techniques. The second method encodes an LTL formula as mixed-integer linear programming constraints on the dynamical system. We demonstrate these approaches with numerical experiments on temporal logic motion planning problems with high-dimensional (10+ states) continuous systems.

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.

Incremental Control Synthesis for Robotics in the Presence of Temporal Logic Specifications

This thesis presents methods for incrementally constructing controllers in the presence of uncertainty and nonlinear dynamics. The basic setting is motion planning subject to temporal logic specifications. Broadly, two categories of problems are treated. The first is reactive formal synthesis when so-called discrete abstractions are available. The fragment of linear-time temporal logic (LTL) known as GR(1) is used to express assumptions about an adversarial environment and requirements of the controller. Two problems of changes to a specification are posed that concern the two major aspects of GR(1): safety and liveness. Algorithms providing incremental updates to strategies are presented as solutions. In support of these, an annotation of strategies is developed that facilitates repeated modifications. A variety of properties are proven about it, including necessity of existence and sufficiency for a strategy to be winning. The second category of problems considered is non-reactive (open-loop) synthesis in the absence of a discrete abstraction. Instead, the presented stochastic optimization methods directly construct a control input sequence that achieves low cost and satisfies a LTL formula. Several relaxations are considered as heuristics to address the rarity of sampling trajectories that satisfy an LTL formula and demonstrated to improve convergence rates for Dubins car and single-integrators subject to a recurrence task.