并发系统的模型和自动验证

时序逻辑可以很好地应用于描述和验证并发系统的动态特性。AMC(Model Checker for Asynchronous concurrent systems)代替传统的从公理出发的形式推导,将并发系统描述转换为系统状态模型,然后应用模型实现对系统时序特性的自动验证。AMC能处理一般形式的合理性问题,并能对大的并发系统进行层次结构模型验证。     

并发系统的操作时序逻辑描述和验证

1.引言 近年来,为了在开发一个复杂系统的过程中尽量提高系统的正确性,减少开发过中重复、较琐的工作,国内外许多学者都从逻辑的角度进行研究,用逻辑系统对并发系统程序行描述、验证,以期通过逻辑系统的简洁和严密来保证友型并发系统的正确     

混合投影时序逻辑与混合系统的形式化验证

为了描述混合系统的性质和行为,10多年来,各种时序逻辑,如Hybrid Temporal Logic等相继出现。这些时序逻辑适用于刻画混合系统的性质和规范,但不适宜表示描述系统的实现模型。本文定义了一个混合投影时序逻辑（Hybrid Projection Temporal Logic,简称HPTL）,既能刻画混合系统的性质,又能表示混合系统的实现。这样,混合系统的验证就可以很方便地在统一的数学模型框架下进行。同时,给出了HPTL的基本的逻辑等价式系统和一个用HPTL进行混合系统验证的实例。     

线性时序逻辑公式的可监控性量化算法

在运行时验证中,对于给定的线性时序逻辑公式,常用其可监控性和弱可监控性来衡量其是否适合用于运行时验证.而实际上,可监控性的要求过于严格,弱可监控性解决的又仅仅是一个\"存在\"问题.为了量化公式的可监控性和弱可监控性,本文提出了概率可监控性,并给出了根据其定义进行求解的方法.此外,本文还提出了基于马尔可夫链的概率可监控性求...     

基于随机通信逻辑的网络控制器设计

设计具有带宽约束的网络控制器,采用带时倚强度的泊松过程形成随机通信逻辑调度策略,实现系统状态的有限次更新,根据其马尔科夫跳变本质,基于更新时刻特性,协同设计控制器。仿真结果表明,引入随机通信逻辑能减少状态更新的次数,降低网络带宽对控制性能的影响,提高系统的动态性能。     

XYZ／CFC与XYZ／PAD：图形一文本程序设计环境

ＸＹＺ系统是一个ＣＡＳＥ工具系统．它的核心是一个时序逻辑语言ＸＹＺ／Ｅ．ＸＹＺ／Ｅ有一基本的表示状态转换的低级形式ＸＹＺ／ＢＥ（或用于表示并发的ＸＹＺ／ＣＥ）及一个结构化的高级形式ＸＹＺ／ＳＥ．它们均有其相应的图形表示．ＸＹＺ／ＣＦＣ与ＸＹＺ／ＰＡＤ是分别以ＸＹＺ／ＢＥ（或ＸＹＺ／ＣＥ）及ＸＹＺ／ＳＥ用逐步求精方法进行程序设计的交互式的图形环境．每步均可由图形程序自动生成时序逻辑形式的程序．     

基于马氏链遗传与繁衍模型的随机L-系统

生物基因从亲代到子代的遗传具有马氏性,基于马氏链遗传与自繁衍模型的随机L-系统,将虚拟生物的形态生成模型与遗传生物学结合起来,同时,为人工生命的实现提供了有益的尝试。     

工作流时序约束模型分析与验证方法

为了解决工作流时间建模与时序一致性验证问题,以时序逻辑和模型检查为基础,提出了一种工作流时间建模与时序一致性验证方法.该方法用一阶逻辑描述工作流模型及其时间信息,用时序逻辑描述工作流的时序约束,用模型检查算法对时序约束进行验证与分析.该方法不是针对某一种时序约束提出来的,而是能够验证任何用时序逻辑描述的工作流时序约束.该方法还能够对未通过验证的时序约束提供工作流运行实例作为反例,帮助用户定位模型的问题.以一个工作流时间建模和时序一致性验证的实例证实了所提出方法的有效性.     

关于网络控制系统中的延迟对系统性能影响的研究

对于有关网络控制系统中存在的延迟对系统的稳定性及其它性能的消极影响及补偿方法,做了较系统的分析．把系统按其延迟大于或小于一个采样周期,定常或时变,确定或随机的不同性质进行分类．并对相继时刻的随机延迟相互独立或者条件相关的不同特点进行了讨论．总结了保证系统均方稳定性的随机控制方法,提出研究网络控制系统的模型方法具有多样性,但其模型框架有值得探讨的一致性,并指出了网络控制系统研究工作创新性之中的鲜明的继承性．     

带有随机时延的非线性网络控制系统的输出反馈镇定

考虑了一类非线性网络控制系统的输出反馈镇定问题.通过齐次马尔可夫链来描述采样器-控制器和控制器.执行器的时延,将网络控制系统建模为带跳非线性系统.利用Lyapunov方法和线性矩阵小等式技巧,得到了闭环系统随机稳定的充分条件,并给出了镇定控制器的设计方法.     

The stochastic semantics and verification for periodic control systems

Periodic control systems(PCS) are widely used in the embedded industry like aerospace and automotive.Such systems usually run periodic tasks and respond to the external signals.Based on our previous work on Mode diagram modeling(MDM) notations for specifying the periodic control system,we present the stochastic semantics for MDM in this paper.The stochastic semantics of MDM is based on the Markov chain.The semantics proposed here provides the basis for the satisfaction of formulae of the interval temporal logic(ITL) based specification language that is aimed to specify the properties of PCS.To verify whether the system satisfies the ITL-based properties,we apply the statistical model checking technique to efficiently estimate the probability of the system satisfying the given property with a desired level of confidence.The empirical experiments show that our approach is both effective and efficient.     

Satisfactory control of discrete-time linear periodic systems

In this paper satisfactory control for discrete-time linear periodic systems is studied. Based on a suitable time-invariant state sampled reformulation, periodic state feedback controller has been designed such that desired requirements of steady state covariance, H-infinity rejection bound and regional pole assignment for the periodic system are met simultaneously. By using satisfactory control theory, the problem of satisfactory periodic controller can be transformed into a linear programming problem subject to a set of linear matrix inequalities （LMIs）, and a feasible designing approach is presented via LMI technique. Numeric example validates the obtained conclusion.     

Preview control for a class of linear stochastic systems with multiplicative noise

ABSTRACT

In this paper, the preview control problem for a class of linear continuous time stochastic systems with multiplicative noise is studied based on the augmented error system method. First, a deterministic assistant system is introduced, and the original system is translated to the assistant system. Then, the integrator is employed to ensure the output of the closed-loop system tracking the reference signal accurately. Second, the augmented error system, which includes integrator vector, control vector and reference signal, is constructed based on the system after translation. As a result, the tracking problem is transformed into the optimal control problem of the augmented error system, and the optimal control input is obtained by the dynamic programming method. This control input is regarded as the preview controller of the original system. For a linear stochastic system with multiplicative noise, the difficulty being unable to construct an augmented error system by the derivation method is solved in this paper. And, the existence and uniqueness solution of the Riccati equation corresponding to the stochastic augmented error system is discussed. The numerical simulations show that the preview controller designed in this paper is very effective.     

Almost sure convergence of iterative learning control for stochastic systems

This paper proposes an iterative learning control (ILC) algorithm with the purpose of controling the output of a linear stochastic system presented in state space form to track a desired realizable trajectory. It is proved that the algorithm converges to the optimal one a.s. under the condition that the product input-output coupling matrices are full-column rank in addition to some assumptions on noises. No other knowledge about system matrices and covariance matrices is required.     

Receding horizon output feedback control for constrained uncertain systems using periodic invariance

In this article, we consider a receding horizon output feedback control (RHOC) method for linear discrete-time systems with polytopic model uncertainties and input constraints. First, we derive a set of estimator gains and then we obtain, on the basis of the periodic invariance, a series of state feedback gains stabilising the augmented output feedback system with these estimator gains. These procedures are formulated as linear matrix inequalities. An RHOC strategy is proposed based on these state feedback and state estimator gains in conjunction with their corresponding periodically invariant sets. The proposed RHOC strategy enhances the performance in comparison with the case in which static periodic gains are used, and increases the size of the stabilisable region by introducing a degree of freedom to steer the augmented state into periodically invariant sets.     

Variable structure control of stochastic systems

In this paper, the problem of variable structure control of stochastic (SVSC) systems is proposed and the corresponding variable structure control strategies with complete and incomplete state information are established. The concepts of stochastic sliding mode and sliding motion band are introduced which may be regarded as the basic characteristics of SVSC systems. Robustness of SVSC systems is considered and a general design procedure for SVSC systems is presented. The effectiveness of the proposed control method is shown by simulation results.     

Linear periodic controller design for decentralized control systems

In the decentralized control of linear time-invariant (LTI) systems, a decentralized fixed mode (DFM) is a system mode which is immoveable using an LTI controller, while a quotient DFM (QDFM) is one which is immoveable using any form of nonlinear time-varying compensation. If a system has no unstable DFMs, there are well-known procedures for designing an LTI stabilizing controller; for systems which have unstable DFMs but no unstable QDFMs, we provide a simple design algorithm which yields a linear periodic sampled-data stabilizing controller.     

Robustness of non-linear stochastic optimal control for quasi-Hamiltonian systems with parametric uncertainty

The robustness of non-linear stochastic optimal control for quasi-Hamiltonian systems with uncertain parameters is studied. Based on the independence of uncertain parameters and stochastic excitations, the non-linear stochastic optimal control for the nominal quasi-Hamiltonian system with average-value parameters is first obtained by using the stochastic averaging method and stochastic dynamical programming principle. Then, the means and standard deviations of root-mean-square responses, control effectiveness and control efficiency for the uncertain quasi-Hamiltonian system are calculated by using the stochastic averaging method and the probabilistic analysis. By introducing the sensitivity of the variation coefficients of controlled root-mean-square responses, control effectiveness and control efficiency to those of uncertain parameters, the robustness of the non-linear stochastic optimal control is evaluated. Two examples are given to illustrate the proposed control procedure and its robustness.     

Sampled-data-based LQ control of stochastic linear continuous-time systems

Sampled-data (SD) based linear quadratic (LQ) control problem of stochastic linear continuous-time (LCT) systems is discussed. Two types of systems are involved. One is time-invariant and the other is time-varying. In addition to stability analysis of the closed-loop systems, the index difference between SD-based LQ control and conventional LQ control is investigated. It is shown that when sample time ?T is small, so is the index difference. In addition, the upper bounds of the differences are also presented, which are O(?T2) and O(?T), respectively.     

A compact fixpoint semantics for term rewriting systems

This work is motivated by the fact that a “compact” semantics for term rewriting systems, which is essential for the development of effective semantics-based program manipulation tools (e.g. automatic program analyzers and debuggers), does not exist. The big-step rewriting semantics that is most commonly considered in functional programming is the set of values/normal forms that the program is able to compute for any input expression. Such a big-step semantics is unnecessarily oversized, as it contains many “semantically useless” elements that can be retrieved from a smaller set of terms. Therefore, in this article, we present a compressed, goal-independent collecting fixpoint semantics that contains the smallest set of terms that are sufficient to describe, by semantic closure, all possible rewritings. We prove soundness and completeness under ascertained conditions. The compactness of the semantics makes it suitable for applications. Actually, our semantics can be finite whereas the big-step semantics is generally not, and even when both semantics are infinite, the fixpoint computation of our semantics produces fewer elements at each step. To support this claim we report several experiments performed with a prototypical implementation.