Loop reduction techniques for reachability analysis of linear hybrid automata

The problem of reachability analysis of linear hybrid automata(LHA) is very difficult.This paper considers to improve the efficiency of the reachability analysis by optimizing the structures of LHA.We identify two types of loops called the flexible loops and the zero loops,and present the techniques to replace the repetitions of those loops in the behavior of LHA with finite sequences of locations and in the meantime simplify the associated constraints.The techniques work not only for the polyhedral computing based algorithms but also for the bounded model checkers.     

与线性混杂自动机等价的状态依赖空间模型

混杂系统可以由多种等价系统进行描述,本文研究用状态依赖空间模型对线性混杂自动机进行描述,线性混杂自动机是一类自治的不确定性系统,而状态依赖空间模型是含有输入的确定性系统.在状态依赖空间模型中,通过增加输入变量可以描述线性混杂自动机转换过程中的不确定性,进而将其转换成等价的状态依赖空间模型.本文所提到的等价性是指两个系统产生的轨迹是相同的.     

线性混杂自动机的非线性广义最小方差控制

研究线性混杂自动机(LHA) 模型. 线性混杂自动机在一定条件下可以转化成与之等价的状态依赖空间模型, 等价性是指两个系统所产生的轨迹是相同的. 采用非线性广义最小方差算法对状态依赖空间模型进行控制器的设计, 非线性广义最小方差控制器的设计则基于更为一般的非线性模型, 模型中可含有时滞项和外界干扰, 控制器的计算过程简单且易于实现. 仿真结果表明, 非线性广义最小方差控制算法能够有效地控制线性混杂自动机, 而且在系统存在延时、干扰以及噪声的情况下能够得到较为理想的控制效果.     

Semi-tensor product of matrices approach to reachability of finite automata with application to language recognition

This paper investigates the transition function and the reachability conditions of finite automata by using a semitensor product of matrices, which is a new powerful matrix analysis tool. The states and input symbols are first expressed in vector forms, then the transition function is described in an algebraic form. Using this algebraic representation, a sufficient and necessary condition of the reachability of any two states is proposed, based on which an algorithm is developed for discovering all the paths from one state to another. Furthermore, a mechanism is established to recognize the language acceptable by a finite automaton. Finally, illustrative examples show that the results/algorithms presented in this paper are suitable for both deterministic finite automata （DFA） and nondeterministic finite automata （NFA）.     

Robust parametric reachability for timed automata

We review the known decidability and undecidability results for reachability in parametric timed automata. Then, we present a new proof of undecidability in dense time for open timed automata that avoids equalities in clock constraints. Our result shows that the undecidability of parametric timed automata does not follow from their ability to specify punctual constraints in a dense time domain.     

BACH:线性混成系统有界可达性模型检验工具

混成自动机的模型检验问题非常困难,即使是其中相对简单的一个子类--线性混成自动机,它的可达性问题仍然是不可判定的.现有的相关工具大都使用多面体计算来判定线性混成自动机状态空间的可达集,复杂度高、效率低,无法解决实际应用规模的问题.描述了一个面向线性混成系统有界可达性模型检验工具--BACH(bounded reacha...     

Semi-tensor product of matrices approach to reachability of finite automata with application to language recognition

This paper investigates the transition function and the reachability conditions of finite automata by using a semitensor product of matrices, which is a new powerful matrix analysis tool. The states and input symbols are first expressed in vector forms, then the transition function is described in an algebraic form. Using this algebraic representation, a sufficient and necessary condition of the reachability of any two states is proposed, based on which an algorithm is developed for discovering all the paths from one state to another. Furthermore, a mechanism is established to recognize the language acceptable by a finite automaton. Finally, illustrative examples show that the results/algorithms presented in this paper are suitable for both deterministic finite automata (DFA) and nondeterministic finite automata (NFA).     

Matrix expression and reachability analysis of finite automata

In this paper,we propose a matrix-based approach for finite automata and then study the reachability conditions.Both the deterministic and nordeterministic automata are expressed in matrix forms,and th...     

T形交叉口信号配时的周期线性微分自动机建模与分析

本文将周期线性微分自动机（CLDA）理论应用于T形交叉口的信号配时问题.建立了T形交叉口排队的一类特殊形式的CLDA模型–切换服务系统.在假定车辆到达率和驶离率满足某种条件的情况下,基于该模型证明了在定相序情况下按照车辆排空后切换信号的配时策略能使车辆排队长度全局周期稳定,并给出了信号配时周期的计算公式.以北京市怀柔区富乐大街处的T形交叉口为例,针对全天候的车辆到达率和驶离率变化情况,应用本文结果进行了分时段信号配时.并使用CheckMate 3.6混杂系统工具箱进行了仿真,仿真结果进一步验证了本文结论的正确性.     

Discrete-time linear periodic systems: A note on the reachability and controllability interval length

Discrete-time linear systems with periodic coefficients of period T are considered in this paper. The reachability and controllability indices at time t for periodic systems, μ_rt and μ_ct, are defined. It is shown that the reachability [controllability] subspace at time t does coincide with the reachability [controllability] subspace over the interval (t − μ_rt,T, t) [(t, t + μ_ct.,T)] and properly includes the reachability [controllability] subspace over the interval (t −(μ_rt−1) T, t) [(t, t +(μ_cr−1)T)].     

Necessary and sufficient condition for the controllability of switching linear hybrid systems

Controllability of switching linear hybrid systems by means of algebraic conditions was discussed by Yang (Automatica 38 (2002), 1221). This paper shows that algebraic conditions complemented with an assumption on the switching function provides not only necessary but also sufficient condition for the problem. The relation of these algebraic conditions with an invariant subspace algorithm is also presented.     

When does the local controllability of the general model of 2-D linear systems imply its local reachability?

A relationship between the local controllability of the general model of two-dimensional linear systems and its local reachability is considered. Sufficient conditions are established under which the local controllability of the general model implies its local reachability.     

State estimation for linear hybrid systems with periodic jumps and unknown inputs

In order to solve the state estimation problem for linear hybrid systems with periodic jumps and unknown inputs, some hybrid observers are proposed. The proposed observers admit a Luenberger‐like structure and the synthesis is given in terms of linear matrix inequalities (LMIs). Therefore, the proposed observer designs are completely constructive and provide some input‐to‐state stability properties with respect to unknown inputs. It is worth mentioning that the structure of the hybrid observers, as well as the structure of the LMIs, depends on some observability properties of the flow and jump dynamics, respectively. Then, in order to compensate the effect of the unknown inputs, a hybrid sliding‐mode observer is added to the Luenberger‐like observer structure, providing exponential convergence to zero of the state estimation error despite certain class of unknown inputs. The existence of the hybrid observers and the unknown input hybrid observer is guaranteed if and only if the hybrid system is observable and strongly observable, respectively. Some numerical examples illustrate the feasibility of the proposed estimation approach.     

On the optimal reachability problem of weighted timed automata

We study the cost-optimal reachability problem for weighted timed automata such that positive and negative costs are allowed on edges and locations. By optimality, we mean an infimum cost as well as a supremum cost. We show that this problem is PSpace-Complete. Our proof uses techniques of linear programming, and thus exploits an important property of optimal runs: their time-transitions use a time τ which is arbitrarily close to an integer. We then propose an extension of the region graph, the weighted discrete graph, whose structure gives light on the way to solve the cost-optimal reachability problem. We also give an application of the cost-optimal reachability problem in the context of timed games. Research supported by the FRFC project “Centre Fédéré en Vérification” funded by the Belgian National Science Foundation (FNRS) under grant nr 2.4530.02.     

基于多面体包含的非线性混成系统可达性分析

针对一类非线性混成系统的可达性问题,提出了一种基于多面体包含的分析方法。首先介绍了混成系统及其可达性,讨论了如何应用多面体包含对多项式混成系统进行线性近似,并采用量词消去和非线性优化方法来构造相应的线性混成系统,然后运用验证工具SpaceEx求得原非线性混成系统的过近似可达集,并应用于验证系统的安全性。     

Towards an Efficient Path-Oriented Tool for Bounded Reachability Analysis of Linear Hybrid Systems using Linear Programming

The existing techniques for reachability analysis of linear hybrid automata do not scale well to problem sizes of practical interest. Instead of developing a tool to perform reachability check on all the paths of a linear hybrid automaton, a complementary approach is to develop an efficient path-oriented tool to check one path at a time where the length of the path being checked can be made very large and the size of the automaton can be made large enough to handle problems of practical interest. This approach of symbolic execution of paths can be used by design engineers to check important paths and thereby, increase the faith in the correctness of the system. Unlike simple testing, each path in our framework represents a dense set of possible trajectories of the system being analyzed. In this paper, we develop the linear programming based techniques towards an efficient path-oriented tool for the bounded reachability analysis of linear hybrid systems.     

线性混合系统的可观性分析

线性混合系统的控制输入(包括离散控制和连续控制)会影响混合系统的状态可观性．混合系统的可观性包括初始的离散状态和连续状态，以及离散状态的切换时间．对此．分析了系统的控制输入对线性混合系统状态(主要是离散状态)的影响，并论述这将有助于改善某些线性混合系统状态的可观性．通过分析给出了在这种情形下比较宽松的线性混合系统状态可观性条件及其秩检验条件，并给出说明性示例．     

Continuity controlled hybrid automata

We investigate the connections between the process algebra for hybrid systems of Bergstra and Middelburg and the formalism of hybrid automata of Henzinger et al. We give interpretations of hybrid automata in the process algebra for hybrid systems and compare them with the standard interpretation of hybrid automata as timed transition systems. We also relate the synchronized product operator on hybrid automata to the parallel composition operator of the process algebra. It turns out that the formalism of hybrid automata matches a fragment of the process algebra for hybrid systems closely. We present an adaptation of the formalism of hybrid automata that yields an exact match.     

On the reachability in any fixed time for positive continuous-time linear systems

This paper deals with the reachability of continuous-time linear positive systems. The reachability of such systems, which we will call here the strong reachability, amounts to the possibility of steering the state in any fixed time to any point of the positive orthant by using nonnegative control functions. The main result of this paper essentially says that the only strongly reachable positive systems are those made of decoupled scalar subsystems. Moreover, the strongly reachable set is also characterized.