Field programmable gate array based predictive control system for spacecraft rendezvous in elliptical orbits

Copyright © 2014 John Wiley & Sons, Ltd. Copyright © 2014 John Wiley & Sons, Ltd. Summary A field programmable gate array (FPGA) based model predictive controller for two phases of spacecraft rendezvous is presented. Linear time-varying prediction models are used to accommodate elliptical orbits, and a variable prediction horizon is used to facilitate finite time completion of the longer range manoeuvres, whilst a fixed and receding prediction horizon is used for fine-grained tracking at close range. The resulting constrained optimisation problems are solved using a primal-dual interior point algorithm. The majority of the computational demand is in solving a system of simultaneous linear equations at each iteration of this algorithm. To accelerate these operations, a custom circuit is implemented, using a combination of Mathworks HDL Coder and Xilinx System Generator for DSP, and used as a peripheral to a MicroBlaze soft-core processor on the FPGA, on which the remainder of the system is implemented. Certain logic that can be hard-coded for fixed sized problems is implemented to be configurable online, in order to accommodate the varying problem sizes associated with the variable prediction horizon. The system is demonstrated in closed-loop by linking the FPGA with a simulation of the spacecraft dynamics running in Simulink on a PC, using Ethernet. Timing comparisons indicate that the custom implementation is substantially faster than pure embedded software-based interior point methods running on the same MicroBlaze and could be competitive with a pure custom hardware implementation.

面向嵌入式实时软件的需求规约语言及检测方法

针对嵌入式实时软件需求规约及其检测问题,提出了基于层次并发有穷状态机的可合成的图形化建模语言RTRSM*(real-time requirements specification model*),利用转换有效期和事件预定机制来描述时间限制,能够较好地支持系统交互性和实时性的建模.为弥补RTRSM*作为操作性规约语言不便于性质描述的问题,提出了命题时序逻辑RITL(real-time interval temporal logic).该语言以时间状态序列为语义模型,具有基于区间和时间点的量化时间属性描述功能,能自然、全面地描述RTRSM*模型性质.介绍并讨论了基于两种语言的规约检测方法和技术,主要包括系统状态空间有穷的RTRSM*模型状态可达图的相关问题和规约的模拟执行.

Reaction time and replenishment time of SP and CGRP after incision in rat skin

Background. the skin neurogenic inflammation is mainly related to Substance P (SP) and Calcitonin Gene-related Peptide (CGRP). There is no data on their availability in the dynamics of skin nerve endings, concerning their release and replenishment after a nociceptive stimulus, so this was investigated. Materials and methods. 25 rats were randomly distributed in 5 groups. the animals of the control group (CG) determined the baseline levels of neuropeptides in the skin. the groups S0 and S30 did not receive any cutaneous stimulus at 30 and 60 minutes, respectively. in the group S1, an incision stimulus was made at 30 minutes. in the group S31, a nociceptive stimulus was performed by subdermal scratching at 30 minutes and, at 60 minutes, the incision stimulus was carried out in the same location (nociceptive hyperstimulation). the skin samples of the other animals were harvested from the back 1 minute after their death. SP, pro-CGRP and CGRP were quantified by Western Blotting. Results. the incision stimulus released SP, S1 compared to S0 (p < 0.05) detected in the first minute, and the replenishment time was more than 30 minutes. Also, it cleaved pro-CGRP, S1 compared to S31 (p < 0.05) in the first minute, and its replenishment time less than 30 minutes. Release of CGRP was not detected. Conclusion. the incision released SP already detected in the first minute; its replenishment time is more than 30 minutes. the incision decreased pro-CGRP, also detected in the first minute; and its replenishment time is less than 30 minutes.

Automatic verification of linear controller software

© 2015 IEEE.We consider the problem of verification of software implementations of linear time-invariant controllers. Commonly, different implementations use different representations of the controller's state, for example due to optimizations in a third-party code generator. To accommodate this variation, we exploit input-output controller specification captured by the controller's transfer function and show how to automatically verify correctness of C code controller implementations using a Frama-C/Why3/Z3 toolchain. Scalability of the approach is evaluated using randomly generated controller specifications of realistic size.

Temporal structure and enablement representation for mutual wills: A Petri net approach

Those temporal formalisms that are sporadically found nowadays in the literature of AI & Law are based on temporal logic. We claim a revived role for another major class of temporal representation: Petri nets. This formalism, popular in computing from the 1970s, had its potential recognized on occasion in the literature of legal computing as well, but apparently the discipline has lost sight of it, and its practitioners on average need be tutored into this kind of representation. Asynchronous, concurrent processes—for which the approach is well‐suited—are found in the legal domain, in disparate contexts. We develop an example for Mutual Wills.

Optimal alarms systems and its application to financial time series

This thesis focuses on the application of optimal alarm systems to non linear time series models. The most common classes of models in the analysis of real-valued and integer-valued time series are described. The construction of optimal alarm systems is covered and its applications explored. Considering models with conditional heteroscedasticity, particular attention is given to the Fractionally Integrated Asymmetric Power ARCH, FIAPARCH(p; d; q) model and an optimal alarm system is implemented, following both classical and Bayesian methodologies. Taking into consideration the particular characteristics of the APARCH(p; q) representation for financial time series, the introduction of a possible counterpart for modelling time series of counts is proposed: the INteger-valued Asymmetric Power ARCH, INAPARCH(p; q). The probabilistic properties of the INAPARCH(1; 1) model are comprehensively studied, the conditional maximum likelihood (ML) estimation method is applied and the asymptotic properties of the conditional ML estimator are obtained. The final part of the work consists on the implementation of an optimal alarm system to the INAPARCH(1; 1) model. An application is presented to real data series.

Integer-valued APARCH processes in the analysis of time series of counts

The Asymmetric Power Arch representation for the volatility was introduced by Ding et al.(1993) in order to account for asymmetric responses in the volatility in the analysis of continuous-valued financial time series like, for instance, the log-return series of foreign exchange rates, stock indices or share prices. As reported by Brannas and Quoreshi (2010), asymmetric responses in volatility are also observed in time series of counts such as the number of intra-day transactions in stocks. In this work, an asymmetric power autoregressive conditional Poisson model is introduced for the analysis of time series of counts exhibiting asymmetric overdispersion. Basic probabilistic and statistical properties are summarized and parameter estimation is discussed. A simulation study is presented to illustrate the proposed model. Finally, an empirical application to a set of data concerning the daily number of stock transactions is also presented to attest for its practical applicability in data analysis.

Modelling and Analysis of Some Time Series

The thesis deals with some of the non-linear Gaussian and non-Gaussian time models and mainly concentrated in studying the properties and application of a first order autoregressive process with Cauchy marginal distribution. In this thesis some of the non-linear Gaussian and non-Gaussian time series models and mainly concentrated in studying the properties and application of a order autoregressive process with Cauchy marginal distribution. Time series relating to prices, consumptions, money in circulation, bank deposits and bank clearing, sales and profit in a departmental store, national income and foreign exchange reserves, prices and dividend of shares in a stock exchange etc. are examples of economic and business time series. The thesis discuses the application of a threshold autoregressive(TAR) model, try to fit this model to a time series data. Another important non-linear model is the ARCH model, and the third model is the TARCH model. The main objective here is to identify an appropriate model to a given set of data. The data considered are the daily coconut oil prices for a period of three years. Since it is a price data the consecutive prices may not be independent and hence a time series based model is more appropriate. In this study the properties like ergodicity, mixing property and time reversibility and also various estimation procedures used to estimate the unknown parameters of the process.

Communicating neurons: a connectionist spiking neuron implementation of stochastic diffusion search

An information processing paradigm in the brain is proposed, instantiated in an artificial neural network using biologically motivated temporal encoding. The network will locate within the external world stimulus, the target memory, defined by a specific pattern of micro-features. The proposed network is robust and efficient. Akin in operation to the swarm intelligence paradigm, stochastic diffusion search, it will find the best-fit to the memory with linear time complexity. information multiplexing enables neurons to process knowledge as 'tokens' rather than 'types'. The network illustrates possible emergence of cognitive processing from low level interactions such as memory retrieval based on partial matching. (C) 2007 Elsevier B.V. All rights reserved.

Time complexity analysis of the stochastic diffusion search

The Stochastic Diffusion Search algorithm -an integral part of Stochastic Search Networks is investigated. Stochastic Diffusion Search is an alternative solution for invariant pattern recognition and focus of attention. It has been shown that the algorithm can be modelled as an ergodic, finite state Markov Chain under some non-restrictive assumptions. Sub-linear time complexity for some settings of parameters has been formulated and proved. Some properties of the algorithm are then characterised and numerical examples illustrating some features of the algorithm are presented.

A logic-based agent that plans for extended reachability goals

Planning to reach a goal is an essential capability for rational agents. In general, a goal specifies a condition to be achieved at the end of the plan execution. In this article, we introduce nondeterministic planning for extended reachability goals (i.e., goals that also specify a condition to be preserved during the plan execution). We show that, when this kind of goal is considered, the temporal logic CTL turns out to be inadequate to formalize plan synthesis and plan validation algorithms. This is mainly due to the fact that the CTL`s semantics cannot discern among the various actions that produce state transitions. To overcome this limitation, we propose a new temporal logic called alpha-CTL. Then, based on this new logic, we implement a planner capable of synthesizing reliable plans for extended reachability goals, as a side effect of model checking.

Mechanising first-order temporal resolution

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. Although a complete and correct resolution-style calculus has already been suggested for this specific fragment, this calculus involves constructions too complex to be of practical value. In this paper, we develop a machine-oriented clausal resolution method which features radically simplified proof search. We first define a normal form for monodic formulae and then introduce a novel resolution calculus that can be applied to formulae in this normal form. By careful encoding, parts of the calculus can be implemented using classical first-order resolution and can, thus, be efficiently implemented. We prove correctness and completeness results for the calculus and illustrate it on a comprehensive example. An implementation of the method is briefly discussed.

Monodic Temporal Resolution

First-order temporal logic is a coincise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics have identified important enumerable and even decidable fragments. In this paper we present the first resolution-based calculus for monodic first-order temporal logic. Although the main focus of the paper is on establishing completeness result, we also consider implementation issues and define a basic loop-search algorithm that may be used to guide the temporal resolution system.

Handling Equality in Monodic Temporal Resolution

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments including the guarded fragment with equality. In this paper, we specialise the monodic resolution method to the guarded monodic fragment with equality and first-order temporal logic over expanding domains. We introduce novel resolution calculi that can be applied to formulae in the normal form associated with the clausal resolution method, and state correctness and completeness results.