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.

Direct detection of Yersinia pestis from the infected animal specimens by a fiber optic biosensor

The FOB-3, anew type fiber optic biosensor, is designed to rapidly detect a variety of biological agents or analytes with better stability, sensitivity and specificity. In order to detect Y. Pestis, a sandwich immunoassay was developed by using the purified antibody against antigen FI immobilized on polystyrene probes as the capture antibody and the monoclonal antibody-Cy5 conjugate as the detector. After a series of optimization for the stability, sensitivity and specificity of the FOB-3, 50-1000 ng/ml of antigen FI and 6 x 10(1)-6 x 10(7) CFU/ml Y. pestis could be detected constantly in about 20 min, and Y pestis could be detected specifically from Y. pseudotuberculosis, Y. enterocolitica, B. anthracis and E. coli. Then, 39 blind samples, including 27 tissues of mice infected with Y pestis and 12 tissues of healthy mice as negative control, were detected with the FOB-3. 92.6% infected tissues were identified from the tissues of healthy mice and the tissues containing more than 100 CFU/ml bacteria could be detected by the biosensor. The results demonstrated the feasibility of the FOB-3 as an effective method to detect Y. pestis rapidly and directly from the infected animal specimens with the advantage of portability, simple-operation as well as high sensitivity and specificity. (c) 2006 Elsevier B.V. All rights reserved.

Brca1 is expressed in human microglia and is dysregulated in human and animal model of ALS

Background: There is growing evidence that microglia are key players in the pathological process of amyotrophic lateral sclerosis (ALS). It is suggested that microglia have a dual role in motoneurone degeneration through the release of both neuroprotective and neurotoxic factors. Results: To identify candidate genes that may be involved in ALS pathology we have analysed at early symptomatic age (P90), the molecular signature of microglia from the lumbar region of the spinal cord of hSOD1(G93A) mice, the most widely used animal model of ALS. We first identified unique hSOD1(G93A) microglia transcriptomic profile that, in addition to more classical processes such as chemotaxis and immune response, pointed toward the potential involvement of the tumour suppressor gene breast cancer susceptibility gene 1 (Brca1). Secondly, comparison with our previous data on hSOD1(G93A) motoneurone gene profile substantiated the putative contribution of Brca1 in ALS. Finally, we established that Brca1 protein is specifically expressed in human spinal microglia and is up-regulated in ALS patients. Conclusions: Overall, our data provide new insights into the pathogenic concept of a non-cell-autonomous disease and the involvement of microglia in ALS. Importantly, the identification of Brca1 as a novel microglial marker and as possible contributor in both human and animal model of ALS may represent a valid therapeutic target. Moreover, our data points toward novel research strategies such as investigating the role of oncogenic proteins in neurodegenerative diseases.

Management of broodstock and quality control of fish seed in Hungary

Common carp (Cyprinus carpio) breeding has a long tradition in Hungary. However, recent economic changes in Eastern Europe and new developments in aquaculture necessitated the need for ensuring quality of the brood stock used in hatcheries and the legal and institutional frameworks needed to implement the program. In addition to good research and development programs and gene banking, it became essential to establish an appropriate legal framework, organize, coordinate and control breeding activities, and provide financial support. It was a major breakthrough for carp breeding when C.carpio was recognized as one of the cultivated animals in the Animal Breeding Act in 1993. The Carp Breeding Section of the Hungarian Fish Producers Association plays an important role in carp breeding programs. Thirteen breeding farms of the Carp Breeding Section have 24 certified C.carpio varieties. In Hungary, about 80 % of the seed used as stocking for commercial production are from high quality certified breeders.

Adaptive agent-based manufacturing control and its application to flow shop routing control

The manufacturing industry is currently facing unprecedented challenges from changes and disturbances. The sources of these changes and disturbances are of different scope and magnitude. They can be of a commercial nature, or linked to fast product development and design, or purely operational (e.g. rush order, machine breakdown, material shortage etc.). In order to meet these requirements it is increasingly important that a production operation be flexible and is able to adapt to new and more suitable ways of operating. This paper focuses on a new strategy for enabling manufacturing control systems to adapt to changing conditions both in terms of product variation and production system upgrades. The approach proposed is based on two key concepts: (1) An autonomous and distributed approach to manufacturing control based on multi-agent methods in which so called operational agents represent the key physical and logical elements in the production environment to be controlled - for example, products and machines and the control strategies that drive them and (2) An adaptation mechanism based around the evolutionary concept of replicator dynamics which updates the behaviour of newly formed operational agents based on historical performance records in order to be better suited to the production environment. An application of this approach for route selection of similar products in manufacturing flow shops is developed and is illustrated in this paper using an example based on the control of an automobile paint shop.

Efeitos de modificação dietética associada ou não a uma rotina de exercícios aeróbicos na microcirculação em modelo animal de obesidade exógena

A obesidade atinge proporções epidêmicas em países industrializados e está relacionada a uma série de doenças metabólicas e circulatórias. Nesse contexto, a atividade física, tratamento não farmacológico da obesidade, acessível a diversas populações e está relacionada com a redução do risco cardiovasvascular mesmo. O objetivo deste trabalho foi avaliar, após mudança ou não da dieta, associação ou não a um programa de treinamento aeróbico (PTA) durante 8 semanas, a possível reversibilidade dos danos causados por uma dieta hiperlipídica por 12 semanas. Para tal, 120 hamsters machos da espécie Mesocricetus auratus, com massa corporal de 60 g, foram distribuídos em quatro grupos, cada um subdividido em três subgrupos, com dez animais para diferentes análises. Os grupos Obeso Controle (OBC) e Obeso Exercitado (OBEX) receberam a ração hiperlipídica por 20 semanas, com adição do PTA ao grupo OBEX nas últimas 8 semanas. Os Obeso Ração Padrão (OBRP) e Obeso Ração Padrão/Exercício (OBRP/EX) tiveram a ração modificada para comercial padrão e adição do PTA ao grupo OBRP/EX após as 12 semanas iniciais. Para as análises microcirculatórias, a bolsa da bochecha foi usada para determinação do número máximo de extravasamentos induzidos por 30 min de isquemia seguida de reperfusão e da reatividade microvascular após a aplicação tópica de acetilcolina e nitroprussiato de sódio. No sangue coletado foi avaliado o perfil lipídico, glicemias quinzenais e leptina. As expressões de eNOS e iNOS foram determinadas na aorta por imunoblotting e a composição corporal avaliada nos tecidos adiposos visceral, urogenital e retroperitoneal, retirados no dia do experimento. Os resultados foram analisados com os métodos o teste estatístico de análise de variância (One Way ANOVA - Teste de Kruskal-Wallis), seguido pelo pós-teste de Dunn. Resultados mostram que a modificação dietética, associada ou não ao PTA, reduziu significativamente a massa corporal (p<0,0001), comprimento naso-anal (p=0,0011) e tecido adiposo (visceral [p<0,0001], urogenital [p=0.0004] e retroperitoneal [p= 0,0083]). Nas análises sanguíneas não foram encontradas diferenças com relação ao perfil lipídico e glicemia, já na leptina houve uma redução significativa (p=0,0039). A análise da reatividade microvascular mostrou melhora significativa na vasodilatação endotélio-dependente nos grupos submetidos à modificação dietética associada ou não ao PTA. Nas medidas de permeabilidade a macromoléculas houve redução significativa no número de extravasamentos nos grupos submetidos à modificação dietética associada ou não ao PTA, (5 min [p= 0,0207] e 10 min [p= 0,0057]). Houve um aumento na expressão de eNOS nos grupos submetidos à modificação dietética associada ou não ao PTA, em comparação ao grupo OBC (p=0,0352). Os resultados mostraram que a modificação dietética, associada ao protocolo de treinamento aeróbico melhora a vasodilatação endotélio-dependente, aumenta a expressão da óxido nítrico sintase endotelial e reduz o número de extravasamentos induzidos por isquemia e reperfusão, mesmo sem melhoras nos marcadores bioquímicos tradicionais como glicemia e perfil lipídico.

RNA processing and Arabidopsis flowering time control.

Plants control their flowering time in order to ensure that they reproduce under favourable conditions. The components involved in this complex process have been identified using a molecular genetic approach in Arabidopsis and classified into genetically separable pathways. The autonomous pathway controls the level of mRNA encoding a floral repressor, FLC, and comprises three RNA-binding proteins, FCA, FPA and FLK. FCA interacts with the 3'-end RNA-processing factor FY to autoregulate its own expression post-transcriptionally and to control FLC. Other components of the autonomous pathway, FVE and FLD, regulate FLC epigenetically. This combination of epigenetic and post-transcriptional control gives precision to the control of FLC expression and flowering time.

An allelic series reveals essential roles for FY in plant development in addition to flowering-time control

The autonomous pathway functions to promote flowering in Arabidopsis by limiting the accumulation of the floral repressor FLOWERING LOCUS C (FLC). Within this pathway FCA is a plant-specific, nuclear RNA-binding protein, which interacts with FY, a highly conserved eukaryotic polyadenylation factor. FCA and FY function to control polyadenylation site choice during processing of the FCA transcript. Null mutations in the yeast FY homologue Pfs2p are lethal. This raises the question as to whether these essential RNA processing functions are conserved in plants. Characterisation of an allelic series of fy mutations reveals that null alleles are embryo lethal. Furthermore, silencing of FY, but not FCA, is deleterious to growth in Nicotiana. The late-flowering fy alleles are hypomorphic and indicate a requirement for both intact FY WD repeats and the C-terminal domain in repression of FLC. The FY C-terminal domain binds FCA and in vitro assays demonstrate a requirement for both C-terminal FY-PPLPP repeats during this interaction. The expression domain of FY supports its roles in essential and flowering-time functions. Hence, FY may mediate both regulated and constitutive RNA 3'-end processing.

Origin of rabbit (Oryctolagus cuniculus) in China: evidence from mitochondrial DNA control region sequence analysis

A fragment of mitochondrial DNA (mtDNA) control region (similar to700 bp) was sequenced in 104 individuals from 20 breeds (three Chinese domestic breeds, five recently derived breeds and 12 introduced breeds) of domestic rabbits, Oryctolagus cuniculus . Nineteen sites were polymorphic, with 18 transitions and one insertion/deletion, and eight haplotypes (A1, A2, A3, A4, A5, A6, A7 and A8) were identified. Haplotype A1 was the most common and occurred in 89 individuals. In the 25 Chinese rabbits, only haplotype A1 was observed, while four haplotypes (A1, A3, A5 and A6) were found in 26 recently derived individuals. Haplotype A2 was shared by seven individuals among three introduced strains. The other six haplotypes accounted for 0. 96-1. 92% of the animals. Combined with the published sequences of European rabbits, a reduced median-joining network was constructed. The Chinese rabbit mtDNAs were scattered into two clusters of European rabbits. These results suggest that the (so-called) Chinese rabbits were introduced from Europe. Genetic diversity in Chinese rabbits was very low.

The water hyacinth problem and the biological control option in the highland lake region of the upper Nile basin: Uganda's experience

The rapid proliferation and extensive spread of water hyacinth Eichhornia crassipes (Mart) Solms in the highland lakes of the Nile Basin within less than 15 years of introduction into the basin in the 1980s pauses potential environmental and social economic menace if the noxious weed is not controlled soon. The water weed has spread all round Lake Victoria and, in Uganda where infes tation is mos t severe, water hyacinth estimated at 1,330,000 ton smothers over 2,000 ha of the lakeshore (August,1994). Lake Kyoga which already constantly supplies River Nile with the weed is infested with over 570 ha, while over 80% of the river course in Uganda is fringed on either side with an average width of about 5m of water hyacinth. As the impact of infestation with water hyacinth on water quality and availability, transportation by water, fishing activities, fisheries ecology, hydro-power generation etc becomes clear in Uganda, serious discussion is under way on how to control and manage the noxious weed. This paper pauses some of the questions being asked regarding the possible application of mechanical and chemical means to control the water weed.Uganda has already initiated the use of biological control of water hyacinth on Lake Kyoga with a strategy to use two weevils namely Neochetinabruchi and Neochetina eichhorniae. The strategy to build capacity and infrastructure for mass multiplication and deployment of biological control of the weevils in the field developed in Uganda by the Fisheries Research Insti tu te (FIRI) and the Namulonge Agricultural and Animal production Research Insti tute (NAARI) is proposed in outline for evaluation. Plans to deploy this strategy on lake Kyoga are under way

Verification of periodically controlled hybrid systems: Application to an autonomous vehicle

This article introduces Periodically Controlled Hybrid Automata (PCHA) for modular specification of embedded control systems. In a PCHA, control actions that change the control input to the plant occur roughly periodically, while other actions that update the state of the controller may occur in the interim. Such actions could model, for example, sensor updates and information received from higher-level planning modules that change the set point of the controller. Based on periodicity and subtangential conditions, a new sufficient condition for verifying invariant properties of PCHAs is presented. For PCHAs with polynomial continuous vector fields, it is possible to check these conditions automatically using, for example, quantifier elimination or sum of squares decomposition. We examine the feasibility of this automatic approach on a small example. The proposed technique is also used to manually verify safety and progress properties of a fairly complex planner-controller subsystem of an autonomous ground vehicle. Geometric properties of planner-generated paths are derived which guarantee that such paths can be safely followed by the controller. © 2012 ACM.

Periodically controlled hybrid systems verifying a controller for an autonomous vehicle

This paper introduces Periodically Controlled Hybrid Automata (PCHA) for describing a class of hybrid control systems. In a PCHA, control actions occur roughly periodically while internal and input actions may occur in the interim changing the discrete-state or the setpoint. Based on periodicity and subtangential conditions, a new sufficient condition for verifying invariance of PCHAs is presented. This technique is used in verifying safety of the planner-controller subsystem of an autonomous ground vehicle, and in deriving geometric properties of planner generated paths that can be followed safely by the controller under environmental uncertainties.

Autonomous rigid body attitude synchronization

Control laws to synchronize attitudes in a swarm of fully actuated rigid bodies, in the absence of a common reference attitude or hierarchy in the swarm, are proposed in [Smith, T. R., Hanssmann, H., & Leonard, N.E. (2001). Orientation control of multiple underwater vehicles with symmetry-breaking potentials. In Proc. 40th IEEE conf. decision and control (pp. 4598-4603); Nair, S., Leonard, N. E. (2007). Stable synchronization of rigid body networks. Networks and Heterogeneous Media, 2(4), 595-624]. The present paper studies two separate extensions with the same energy shaping approach: (i) locally synchronizing the rigid bodies' attitudes, but without restricting their final motion and (ii) relaxing the communication topology from undirected, fixed and connected to directed, varying and uniformly connected. The specific strategies that must be developed for these extensions illustrate the limitations of attitude control with reduced information. © 2008 Elsevier Ltd.

Autonomous rigid body attitude synchronization

This paper studies some extensions to the decentralized attitude synchronization of identical rigid bodies. Considering fully actuated Euler equations, the communication links between the rigid bodies are limited and the available information is restricted to relative orientations and angular velocities. In particular, no leader nor external reference dictates the swarm's behavior. The control laws are derived using two classical approaches of nonlinear control - tracking and energy shaping. This leads to a comparison of two corresponding methods which are currently considered for distributed synchronization - consensus and stabilization of mechanical systems with symmetries. © 2007 IEEE.

Identification of the steering control behaviour of five test subjects following a randomly curving path in a driving simulator

The paper is concerned with the identification of theoretical preview steering controllers using data obtained from five test subjects in a fixed-base driving simulator. An understanding of human steering control behaviour is relevant to the design of autonomous and semi-autonomous vehicle controls. The driving task involved steering a linear vehicle along a randomly curving path. The theoretical steering controllers identified from the data were based on optimal linear preview control. A direct-identification method was used, and the steering controllers were identified so that the predicted steering angle matched as closely as possible the measured steering angle of the test subjects. It was found that identification of the driver's time delay and noise is necessary to avoid bias in identification of the controller parameters. Most subjects' steering behaviour was predicted well by a theoretical controller based on the lateral/yaw dynamics of the vehicle. There was some evidence that an inexperienced driver's steering action was better represented by a controller based on a simpler model of the vehicle dynamics, perhaps reflecting incomplete learning by the driver. Copyright © 2014 Inderscience Enterprises Ltd.