基于广义可能性测度的可达性问题的模型检测

在广义可能性测度下,提出了广义可能性Kripke结构来描述系统的量化行为。在广义可能性Kripke结构下重新定义了线性时序逻辑的语构和语义,研究了线性时间属性的最终可达性、限制可达性、重复可达性等模型检测问题。本文所获得的结果扩大了可能性测度在模型检测中的应用范围。     

矩阵不可约的充要条件

本文利用可达性给出矩阵不可约的一个充要条件。在此基础法上,讨论可达性矩阵的性质,进而给出将一类可约矩阵化为主对角线上都为不可约子块的块上三角阵。这个方法可以在计算机上实施,实用而方便。     

初等算子的几个问题(Ⅲ)

在[1，2]中，讨论了初等算子的范数，值域，极大数值域的问题．本文继续这方面的问题的讨论．主要是有关零空间与植域的关系以及一类初等其子的值域的闭性，初等算子的范数可达性问题进行讨论．     

职称等级结构的予报和控制—以人员调入比例为控制量的情形

一些社会系统中的职称等级结构通常取决于系统成员的提升、调入和调出比例,它遵从推广的Markov模型。本文给出这一模型的基本方程及关于等级结构的可保持性、可达性等概念,讨论在控制量——人员调入比例——有上限时确定控制序列,使系统从初始结构最快地达到(或接近)期望结构的方法。最后在系统总人数有固定增长率的情况下给出计算实例。     

一类时变仿射非线性系统的动态状态反馈线性化的条件

本文用微分几何方法讨论了一类时变仿射非线性系统（即ｎ＝ｍ＋１）的动态状态反馈线性化与系统的线性近似的关系，得出了系统可动态状态反馈线性化的条件。     

与年龄相关的随机分数阶种群系统温和解的存在性、唯一性

本文研究了一类与年龄相关的随机分数阶种群动态系统.利用不动点定理、随机分析和算子半群理论,讨论了与年龄相关的随机分数阶种群系统温和解的存在性、唯一性.本文是随机整数阶种群系统的推广.     

一类非线性微分代数系统的零动态

控制系统的零动态是系统一种内部动态品质,其行为与系统的许多性质相联系,如系统的稳定性,反馈镇定与输出跟踪等.针对一类非线性微分代数系统,提出了输出零子流形和零动态的概念.利用M-导数方法,探讨了此类系统的输出零子流形的性质,并给出了此类系统的输出零子流形和零动态算法,也讨论了该算法的一些性质.最后,给出一个例子说明如何利用系统的零动态来讨论系统的反馈稳定化问题.     

关于非线性自回归模型的几何遍历性

本文讨论带噪声的动态系统，即非线性自由回归模型，若原系统不具有任何压缩性质，但是它的某种拓扑共轭变换后的系统满足一定的压缩性质，本文指出，当噪声适当小时，相应的带噪声的动态系统将有唯一的平稳解，而且是几何遍历的。     

一类串联动态修复系统的适定性

本文讨论了一类串联动态修复系统的数学模型 ,用泛函分析中 C0 半群的方法证明了该系统的非负解的存在唯一性 ,并且进一步在一定条件下给出了其解是半稳定的     

带有同步变迁的有界Petri网系统的建模及可达性分析

由于存在可达标识集的爆炸性问题,大型Petri网系统的建模及可达性分析等问题的研究存在难度.文章利用矩阵的半张量积工具,研究了带有同步变迁的有界Petri网系统的建模及可达性问题.一方面,由于该类Petri网系统可以看作是由若干个子Petri网系统组成,所以可以用半张量积工具表述得到整个Petri网系统的矩阵表示.另一方面,在得出的矩阵表示的基础上,研究了两个标识之间可达性的充要判据,并给出了求可达变迁序列的算法.最后,文章用实例验证了该算法的正确性.所提出的方法在一定程度上解决了状态空间爆炸问题,并易于计算机实现.     

Reachability realization and stabilizability of switched linear discrete-time systems

In this paper, the reachability realization of a switched linear discrete-time system, which is a collection of linear time-invariant discrete-time systems along with some maps for “switching” among them, is addressed. The main contribution of this paper is to prove that for a switched linear discrete-time system, there exists a basic switching sequence such that the reachable (controllable) state set of this basic switching sequence is equal to the reachable (controllable) state set of the system. Hence, the reachability (controllability) can be realized by using only one switching sequence. We also discuss the stabilizability of switched systems, and obtain a sufficient condition for stabilizability. Two numeric examples are given to illustrate the results.     

On weak and strong reachability and controllability of infinite-dimensional linear systems

The notions of reachability and controllability generalize to infinite-dimensional systems in two different ways. We show that the strong notions are equivalent to finite-time reachability and controllability. For discrete systems in Hilbert space, we get simple relations generalizing the Kalman conditions. In the case of a continuous system in Hilbert space, weak reachability is equivalent to the weak reachability of a related discrete system via the Cayley transform.This research was partially supported by the Batsheva de Rothschild Fund for the Advancement of Science and Technology.     

State constrained reachability for stochastic hybrid systems

Many control problems can be formulated as driving a system to reach some target states while avoiding some unwanted states. We study this problem for systems with regime change operating in uncertain environments. Nowadays, it is a common practice to model such systems in the framework of stochastic hybrid system models. In this casting, the problem is formalized as a mathematical problem named state constrained stochastic reachability analysis. In the state constrained stochastic reachability analysis, this probability is computed by imposing a constraint on the system to avoid the unwanted states. The scope of this paper is twofold. First we define and investigate the state constrained reachability analysis in an abstract mathematical setting. We define the problem for a general model of stochastic hybrid systems, and we show that the reach probabilities can be computed as solutions of an elliptic integro-differential equation. Moreover, we extend the problem by considering randomized targets. We approach this extension using stochastic dynamic programming. The second scope is to define a developmental setting in which the state constrained reachability analysis becomes more tractable. This framework is based on multilayer modelling of a stochastic system using hierarchical viewpoints. Viewpoints represent a method originated from software engineering, where a system is described by multiple models created from different perspectives. Using viewpoints, the reach probabilities can be easily computed, or even symbolically calculated. The reach probabilities computed in one viewpoint can be used in another viewpoint for improving the system control. We illustrate this technique for trajectory design.     

Output controllability and optimal output control of positive fractional order linear discrete system with multiple delays in state, input and output

The article concerns output controllability and optimal output control of positive fractional order discrete linear systems with multiple delays in state, input and output. Necessary and sufficient conditions for output reachability (output controllability from zero initial conditions) and null output controllability (output controllability to zero final output) are given and proven. We also prove that the positive system is output controllable if it is output reachable and null output controllable with the output reachability index is equal or less than the null output controllability index. Sufficient conditions for the solvability of the optimal output control problem are given. Numerical examples are presented to illustrate the theoretical results.     

Some remarks on Boolean control systems: Controllability domains and realization theory

We construct a theory of realizations and controllability domains for linear stationary systems in the category of finitely generated free semimodules over a Boolean semiring. We show that the classical realization theorems cannot be generalized to this case, and we prove some incomplete analogs of these theorems. We analyze the structure of controllability domains and the reachability and observability characteristics. In particular, we define a geometric object representing the reachability properties of a system, namely, the generalized reachability topology on the state space.     

Falsification of hybrid systems with symbolic reachability analysis and trajectory splicing

The falsification of a hybrid system aims at finding trajectories that violate a given safety property. This is a challenging problem, and the practical applicability of current falsification algorithms still suffers from their high time complexity. In contrast to falsification, verification algorithms aim at providing guarantees that no such trajectories exist. Recent symbolic reachability techniques are capable of efficiently computing linear constraints that enclose all trajectories of the system with reasonable precision. In this paper, we leverage the power of symbolic reachability algorithms to improve the scalability of falsification techniques. Recent approaches to falsification reduce the problem to a nonlinear optimization problem. We propose to reduce the search space of the optimization problem by adding linear state constraints obtained with a reachability algorithm. An empirical study of how varying abstractions during symbolic reachability analysis affect the performance of solving a falsification problem is presented. In addition, for solving a falsification problem, we propose an alternating minimization algorithm that solves a linear programming problem and a non-linear programming problem in alternation finitely many times. We showcase the efficacy of our algorithms on a number of standard hybrid systems benchmarks demonstrating the performance increase and number of falsifyable instances.     

Performance Optimization of a Class of Discrete Event Dynamic Systems Using Calculus of Variations Techniques

We explore an approach involving the use of calculus of variations techniques for discrete event dynamic system (DEDS) performance optimization problems. The approach is motivated by the observation that such problems can be described by separable cost functions and recursive dynamics of the same form as that used to describe conventional discrete-time continuous-variable optimal control problems. Three important difficulties are that DEDS are generally stochastic, their dynamics typically involve max and min operations, which are not everywhere differentiable, and the state variables are often discrete. We demonstrate how to overcome these difficulties by applying the approach to a transportation problem, modeled as a polling system, where we are able to derive an explicit and intuitive analytic expression for an optimal control policy.     

Computing reachable sets for uncertain nonlinear monotone systems

We address nonlinear reachability computation for uncertain monotone systems, those for which flows preserve a suitable partial orderings on initial conditions. In a previous work Ramdani (2008) [22], we introduced a nonlinear hybridization approach to nonlinear continuous reachability computation. By analysing the signs of off-diagonal elements of system’s Jacobian matrix, a hybrid automaton can be obtained, which yields component-wise bounds for the reachable sets. One shortcoming of the method is induced by the need to use whole sets for addressing mode switching. In this paper, we improve this method and show that for the broad class of monotone dynamical systems, component-wise bounds can be obtained for the reachable set in a separate manner. As a consequence, mode switching no longer needs to use whole solution sets. We give examples which show the potentials of the new approach.     

Time-constrained temporal logic control of multi-affine systems

In this paper, we consider the problem of controlling a dynamical system such that its trajectories satisfy a temporal logic property in a given amount of time. We focus on multi-affine systems and specifications given as syntactically co-safe linear temporal logic formulas over rectangular regions in the state space. The proposed algorithm is based on estimating the time bounds for facet reachability problems and solving a time optimal reachability problem on the product between a weighted transition system and an automaton that enforces the satisfaction of the specification. A random optimization algorithm is used to iteratively improve the solution.     

Reachability and Observability Concepts for Stochastic Systems

We define observability and reachability and introduce the corresponding Gramians for a Levy driven linear system like Benner, Damm in [3] which focused on the case of Wiener noise. We additionally show that the sets of observable and reachable states are characterized by these Gramians. This is analogous to deterministic systems, where observability and reachability concepts are described in Sections 4.2.1 and 4.2.2 in Antoulas [1]. (© 2013 Wiley-VCH Verlag GmbH & Co. KGaA, Weinheim)