混合系统的符号化可达性分析

定义了一种称作混合区域的形式化结构表示矩形混合系统的状态集,它实际上是由一组特殊形式的线性不等式联立表示的多面体空间.证明了混合区域对于矩形混合系统的可达性操作的封闭性.此外,用矩形混合系统近似模拟非线性混合系统,相应地解决了非线性混合系统的可达性问题.使用混合区域,可以直接计算由某个正则的混合区域开始的可达集,这样,混合系统的可达性问题主要是求解混合区域的正则型问题,而这问题是一种线性规划问题,可以使用经典的线性规划算法加以解决.     

Learning and Inferring Motion Patterns using Parametric Segmental Switching Linear Dynamic Systems

Switching Linear Dynamic System (SLDS) models are a popular technique for modeling complex nonlinear dynamic systems. An SLDS can describe complex temporal patterns more concisely and accurately than an HMM by using continuous hidden states. However, the use of SLDS models in practical applications is challenging for three reasons. First, exact inference in SLDS models is computationally intractable. Second, the geometric duration model induced in standard SLDSs limits their representational power. Third, standard SLDSs do not provide a principled way to interpret systematic variations governed by higher order parameters. The contributions in this paper address all of these three challenges. First, we present a data-driven MCMC (DD-MCMC) sampling method for approximate inference in SLDSs. We show DD-MCMC provides an efficient method for estimation and learning in SLDS models. Second, we present segmental SLDSs (S-SLDS), where the geometric distributions of the switching state durations are replaced with arbitrary duration models. Third, we extend the standard SLDS model with additional global parameters that can capture systematic temporal and spatial variations. The resulting parametric SLDS model (P-SLDS) uses EM to robustly interpret parametrized motions by incorporating additional global parameters that underly systematic variations of the overall motion. The overall development of the extensions for SLDSs provide a principled framework to interpret complex motions. The framework is applied to the honey bee dance interpretation task in the context of the on-going BioTracking project at the Georgia Institute of Technology. The experimental results suggest that the enhanced models provide an effective framework for a wide range of motion analysis applications.     

What should your speech system say?

Even as telephone based spoken language dialogue systems (SLDS) are becoming commercially available, developers can benefit from guidelines designed to help remove dialogue problems as early as possible in the design life cycle. SLDS designers generally rely on a Wizard of Oz (WOZ) simulation technique to ensure that the system's dialogue facilitates user interaction as much as possible. In a WOZ simulation, users are made to believe they are interacting with a real system, when in fact they are interacting with a hidden researcher. These researchers record, transcribe, and analyze the dialogues, and then use the results to improve the dialogue in the SLDS being developed. Using current methods, dialogue designers must be both very careful and very lucky, or interaction problems will remain during the implementation and testing stages. We have found that a sound, comprehensive set of dialogue design guidelines is an effective tool to support systematic development and evaluation during early SLDS design. We believe guidelines could significantly reduce development time by reducing the need for lengthy WOZ experimentation, controlled user testing, and field trial cycles     

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

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

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

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

Discrete-time linear periodic systems: gramian and modal criteria for reachability and controllability†

This paper deals with the reachability and controllability of periodic discrete-time systems. First, we supply two necessary and sufficient complete reachability conditions, which apply to reversible and non-reversible systems, respectively. Then, a necessary and sufficient complete controllability condition is provided. This condition, as well as the complete reachability criteria, is given in terms of the reachability gramian matrix. Equivalent modal criteria for reachability and controllability are established in the second part of the paper.     

离散广义系统模型的一般响应公式与局部能控性

利用函数的Z-变换,获得了离散广义系统模型的一般响应公式,由此得到该模型的局部可达性与局部能控性的充分必要条件.     

离散时滞广义系统的一般解与局部能控性

利用函数的Z－变换,获得了离散时滞广义系统的一般解,由此得到该系统的局部可达性与局部能控性的充分必要条件,同时给出了数值例子。     

Reachability Properties of Continuous-Time Positive Systems

In this technical note, reachability properties of continuous-time positive systems are introduced and characterized. Specifically, first it is shown that reachability and strong reachability are equivalent properties, and thus the characterization of strong reachability derived in is extended to the weaker notion of reachability. In the second part of the technical note, essential reachability is introduced, and necessary and sufficient conditions for this property to hold are provided.      

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.     

Reachability and controllability of discrete-time linear periodic systems

In this paper, we consider discrete-time linear systems with periodic coefficients. Two necessary and sufficient conditions for complete controllability and reachability are given. The conditions are stated in terms of the reachability Gramian and hold for both reversible and nonreversible systems.     

UML时间顺序图的可达性分析

对于实时系统来说,UML顺序图描述了对象之间的交互。对象之间的交互展现了系统行为的场景。本文中,我们针对描述多场景的UML顺序图组合中的可达性问题进行研究。尽管这个问题可以转换为相应的时间自动机,然后进行处理,但其转化为之后,状态空间巨大,解决的开销比较大,效率不高。针对部分可达性问题,本文采用更为高效的基于线性规划的解决方案,其思想如下:首先遍历所有到达给定节点的简单路径片断来验证可达性,随后遍历到达给定节点的并且包含所有循环至多一次的路径片断来验证可达性。由于我们并没有遍历所有路径片断,因此用本文的方法判定给定节点的可达性的时候,结果会有三种:可达,不可达和不确定。由于有些循环与可达性是无关的,我们进一步通过识别哪些循环与可达性无关,对算法进行改进。     

On the reachability problem for 5-dimensional vector addition systems

The reachability sets for vector addition systems of dimension less than or equal to five are shown to be effectively computable semilinear sets. Thus reachability, equivalence and containment are decidable up to dimension 5. An example of a non-semilinear reachability set is given for dimension 6.     

Reachability and controllability of switched linear discrete-timesystems

This paper investigates the reachability and controllability issues for switched linear discrete-time systems. Geometric characterization of controllability is presented. For reversible systems, the controllable sets and the reachable sets are identified in Wonham's geometric approach, and verifiable conditions for reachability and controllability are also presented     

A new perspective on criteria and algorithms for reachability of discrete-time switched linear systems

The paper presents a unified perspective on geometric and algebraic criteria for reachability and controllability of controlled switched linear discrete-time systems. Direct connections between geometric and algebraic criteria are established as well as that between the subspace based controllability/reachability algorithm and Kalman-type algebraic rank criteria. Also the existing geometric criteria is simplified and new algebraic conditions on controllability and reachability are given.     

On the polynomial dynamic system approach to software development

1IntroductionReactivesystemsareregardedessentialintheareaofcomputerscience[1].Quiteafewapproacheshavebeenproposedtodevelopreactivesystems,includingthestatemateapproach[2],thetemporal-logicapproach[3],thesynchronousapproach[4],amongoth-ers[5,6].Usually,thepropertiesofthereactivesoftwareunderdevelopmentarecheckedaposteriori(aftersoftwaredesignorevensoftwareimplementation)usingpropertyveri-ficationand/orsimulationtechniquessuchasthetemporal-logicapproach[7]andtheSmoochesapproach[5].However,thisi…     

Reachability conditions for switched linear singular systems

The reachability problem of switched linear singular systems is investigated in this note. By using the geometric approach and the admissible control set introduced, a necessary condition and a sufficient condition on complete reachability are presented. The conditions are the same as those of the conventional (nonsingular) switched linear systems and normal (nonswitching) singular systems given in previous papers when the systems degenerate to normal singular systems and conventional switched systems, respectively.     

Reachability of Patterned Conditional Pushdown Systems

Conditional pushdown systems (CPDSs) extend pushdown systems by associating each transition rule with a regular language over the stack alphabet. The goal is to model program verification problems that need to examine the runtime call stack of programs. Examples include security property checking of programs with stack inspection, compatibility checking of HTML5 parser specifications, etc. Esparza et al. proved that the reachability problem of CPDSs is EXPTIME-complete, which prevents the existence of an algorithm tractable for all instances in general. Driven by the practical applications of CPDSs, we study the reachability of patterned CPDS (pCPDS) that is a practically important subclass of CPDS, in which each transition rule carries a regular expression obeying certain patterns. First, we present new saturation algorithms for solving state and configuration reachability of pCPDSs. The algorithms exhibit the exponential-time complexity in the size of atomic patterns in the worst case. Next, we show that the reachability of pCPDSs carrying simple patterns is solvable in fixed-parameter polynomial time and space. This answers the question on whether there exist tractable reachability analysis algorithms of CPDSs tailored for those practical instances that admit efficient solutions such as stack inspection without exception handling. We have evaluated the proposed approach, and our experiments show that the pattern-driven algorithm steadily scales on pCPDSs with simple patterns.

     

On the analysis of nonlinear nilpotent switched systems using the Hall–Sussmann system

We consider an open problem on the stability of nonlinear nilpotent switched systems posed by Daniel Liberzon. Partial solutions to this problem were obtained as corollaries of global nice reachability results for nilpotent control systems. The global structure is crucial in establishing stability. We show that a nice reachability analysis may be reduced to the reachability analysis of a specific canonical system, the nilpotent Hall–Sussmann system. Furthermore, local nice reachability properties for this specific system imply global nice reachability for general nilpotent systems. We derive several new results revealing the elegant Lie-algebraic structure of the nilpotent Hall–Sussmann system.     

Reachability analysis of constrained switched linear systems

In this note, we investigate the reachability of switched linear systems with switching/input constraints. We prove that, under a mild assumption of the feasible switching signals, the reachability set is the reachable subspace of the unconstrained system. We also address the local reachability for switched linear systems with input constraints and present a complete criterion for a general class of switched linear systems.