连续时间Markov决策过程互模拟等价及逻辑保持

模型检测中,Markov决策过程可以建模具有不确定性的系统,然而状态空间爆炸问题将会影响系统验证的成败与效率,互模拟等价可以用于系统状态的简约.在强互模拟关系的基础上,给出Markov决策过程模型弱互模拟等价关系的概念,导出了连续时间Markov决策过程及其内嵌离散时间Markov决策过程互模拟等价关系的内在联系;在强互模拟等价关系逻辑特征保持的基础上,给出弱互模拟等价关系下的逻辑保持性质,证明了弱互模拟等价的两个状态,同时满足除下一步算子外的连续随机逻辑公式,从而可以将原模型中的验证问题转换为简约后模型的验证问题,提高验证的效率.     

Correctness verification and performance analysis of real-time systems using stochastic preemptive time Petri nets

Time Petri nets describe the state of a timed system through a marking and a set of clocks. If clocks take values in a dense domain, state space analysis must rely on equivalence classes. These support verification of logical sequencing and quantitative timing of events, but they are hard to be enriched with a stochastic characterization of nondeterminism necessary for performance and dependability evaluation. Casting clocks into a discrete domain overcomes the limitation, but raises a number of problems deriving from the intertwined effects of concurrency and timing. We present a discrete-time variant of time Petri nets, called stochastic preemptive time Petri nets, which provides a unified solution for the above problems through the adoption of a maximal step semantics in which the logical location evolves through the concurrent firing of transition sets. We propose an analysis technique, which integrates the enumeration of a succession relation among sets of timed states with the calculus of their probability distribution. This enables a joint approach to the evaluation of performance and dependability indexes as well as to the verification of sequencing and timeliness correctness. Expressive and analysis capabilities of the model are demonstrated with reference to a real-time digital control system.     

Static analysis and dynamic steering of time-dependent systems

An enumerative technique is presented which supports reachability and timeliness analysis of time-dependent models. The technique assumes a dense model of time and uses equivalence classes to enable discrete and compact enumeration of the state space. Properties of timed reachability among states are recovered through the analysis of timing constraints embedded within equivalence classes. In particular, algorithms are given to evaluate a tight profile for the set of feasible timings of any untimed run. Runtime refinement of static profiles supports a mixed static/dynamic strategy in the development of a failure avoidance mechanism for dynamic acceptance and a guarantee of hard real-time processes     

基于状态空间等价类的有色Petri网特性验证

在有色Petri网的状态空间中,有时一些状态具有相似的行为,这些状态可以用定义在状态空间上的一致的等价关系来表达,对每个等价状态类只研究它的一个代表状态的行为,这极大地减小了有色Petri网的状态空间。但是,通常对一个给定的等价关系是否为一致的验证都是通过用户的经验人工进行的,这不但容易产生错误,而且效率低下。该文依据普通状态图和等价类状态图的标记迁移系统关系,对状态空间一致性等价定义的计算机辅助验证做了深入的讨论,给出了相应的结果。     

不确定规划中状态循环可达关系的求解方法

在不确定规划领域中, 不确定状态转移系统求规划解常常会搜索大量无用的状态和动作, 造成冗余计算。获得不确定状态转移系统的状态可达关系可以避免无用搜索、减少冗余计算, 为系统提供引导信息。以非循环可达关系为基础, 定义矩阵的计算规则, 使用系统的邻接矩阵来计算可达矩阵。同时首次提出了循环可达关系的分类、二可达关系等, 并设计了求循环可达关系的算法, 且以实例证明了算法的有效性和正确性。在不确定规划中获得状态之间的可达性关系, 在求规划解的过程中可以删除大量无用的状态动作序偶, 降低问题规模, 提高求解规划问题的效率。     

State-Density Functions over DBM Domains in the Analysis of Non-Markovian Models

Quantitative evaluation of models with generally-distributed transitions requires analysis of non-Markovian processes that may be not isomorphic to their underlying untimed models and may include any number of concurrent non-exponential timers. The analysis of stochastic Time Petri Nets copes with the problem by covering the state space with stochastic-classes, which extend Difference Bounds Matrices (DBM) with a state probability density function. We show that the state-density function accepts a continuous piecewise representation over a partition in DBM-shaped sub-domains. We then develop a closed-form symbolic calculus of state-density functions assuming that model transitions have expolynomial distributions. The calculus shows that within each sub-domain the state-density function is a multivariate expolynomial function and makes explicit how this form evolves through subsequent transitions. This enables an efficient implementation of the analysis process and provides the formal basis that supports introduction of an approximate analysis based on Bernstein Polynomials. The approximation attacks practical and theoretical limits in the applicability of stochastic state-classes, and devises a new approach to the analysis of non Markovian models, relying on approximations in the state space rather than in the structure of the model.     

Transient analysis of non-Markovian models using stochastic state classes

The method of stochastic state classes approaches the analysis of Generalised Semi Markov Processes (GSMPs) through the symbolic derivation of probability density functions over supports described by Difference Bounds Matrix (DBM) zones. This makes steady state analysis viable, provided that at least one regeneration point is visited by every cyclic behaviour of the model.We extend the approach providing a way to derive transient probabilities. To this end, stochastic state classes are extended with a supplementary timer that enables the symbolic derivation of the distribution of time at which a class can be entered. The approach is amenable to efficient implementation when model timings are given by expolynomial distributions, and it can be applied to perform transient analysis of GSMPs within any given time bound. In the special case of models underlying a Markov Regenerative Process (MRGP), the method can also be applied to the symbolic derivation of local and global kernels, which in turn provide transient probabilities through numerical integration of generalised renewal equations. Since much of the complexity of this analysis is due to the local kernel, we propose a selective derivation of its entries depending on the specific transient measure targeted by the analysis.     

Checking timed automata for linear duration properties

It is proved in this paper that checking a timed automaton M with respect to a linear duration property D can be done by investigating only the integral timed states of M,An equivalence relation is introduced in this paper to divide the infinite number of integral timed states into finite number of equivalence classes.Based on this,a method is proposed for checking whether M satisfies D.In some cases,the number of equivalence classes is too large for a computer to mainpulate,A technique for reducing the search-space for checking linear duration propoerty is also described.This technique is more suitable for the case in this paper than those in the literature because most of those techniques are designed for reachablility analysis.     

基于随机Petri网的可重构核心单元分析

利用随机Petri网对可重构核心单元进行建模,对其可达性、有界性、安全性等结构特性进行逻辑正确性验证,并对其稳态概率、变迁概率、吞吐量等性能特性进行数量化求解。在好、中、差3种速率情况下讨论动态重构对计算任务完成时间的影响,分析结果表明,可重构核心单元的动态重构响应越及时,其任务处理时间就越少。     

数字设计中基于图的状态等价类集生成算法

在完全确定状态的时序电路、状态机等数字系统设计中,确定全部状态等价类,是进行最优状态化简的前提.结合图论理论提出一种等价类集生成算法,首先建立等价类与图中连通分支的联系,然后给出了通过化简图的邻接矩阵而得到等价类集的方法.算法易于编程实现,适合那些状态完全确定的包含几十、上百甚至更多初始状态的大规模数字系统设计.     

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).     

正则语言的一个特征

Myhill-Nerode定理利用等价关系描述了正则语言的一个重要特征,它是有限自动机理论中的一个经典、优美的结果。为了将Myhill-Nerode定理推广到更一般的情形,引入了有限自动机M上的状态转移半群和Σ*上的M-半群,讨论了其若干性质。在此基础上,将Myhill-Nerode定理中的等价关系一般化,给出了正则语言的一个新的特征定理,Myhill-Nerode定理成为该定理的一个推论。讨论了正则语言的最一般的特征,提出了有待进一步研究的问题。     

A general definition of stochastic automata

A new class of stochastic automata is defined. Its elements, called dependent automata, are characterized by a partition on the set of states such that the transition between the blocks is defined deterministicly. The definitions of isomorphism and equivalence are adapted. Some relations with other classes of stochastic automata and subclasses of dependent automata are defined.     

A game-based abstraction-refinement framework for Markov decision processes

In the field of model checking, abstraction refinement has proved to be an extremely successful methodology for combating the state-space explosion problem. However, little practical progress has been made in the setting of probabilistic verification. In this paper we present a novel abstraction-refinement framework for Markov decision processes (MDPs), which are widely used for modelling and verifying systems that exhibit both probabilistic and nondeterministic behaviour. Our framework comprises an abstraction approach based on stochastic two-player games, two refinement methods and an efficient algorithm for an abstraction-refinement loop. The key idea behind the abstraction approach is to maintain a separation between nondeterminism present in the original MDP and nondeterminism introduced during the abstraction process, each type being represented by a different player in the game. Crucially, this allows lower and upper bounds to be computed for the values of reachability properties of the MDP. These give a quantitative measure of the quality of the abstraction and form the basis of the corresponding refinement methods. We describe a prototype implementation of our framework and present experimental results demonstrating automatic generation of compact, yet precise, abstractions for a large selection of real-world case studies.     

Finite state automata resulting from temporal information maximization and a temporal learning rule

We extend Linkser's Infomax principle for feedforward neural networks to a measure for stochastic interdependence that captures spatial and temporal signal properties in recurrent systems. This measure, stochastic interaction, quantifies the Kullback-Leibler divergence of a Markov chain from a product of split chains for the single unit processes. For unconstrained Markov chains, the maximization of stochastic interaction, also called Temporal Infomax, has been previously shown to result in almost deterministic dynamics. This letter considers Temporal Infomax on constrained Markov chains, where some of the units are clamped to prescribed stochastic processes providing input to the system. Temporal Infomax in that case leads to finite state automata, either completely deterministic or weakly nondeterministic. Transitions between internal states of these systems are almost perfectly predictable given the complete current state and the input, but the activity of each single unit alone is virtually random. The results are demonstrated by means of computer simulations and confirmed analytically. It is furthermore shown numerically that Temporal Infomax leads to a high information flow from the input to internal units and that a simple temporal learning rule can approximately achieve the optimization of temporal interaction. We relate these results to experimental data concerning the correlation dynamics and functional connectivities observed in multiple electrode recordings.     

Control of Nondeterministic Discrete Event Systems for Simulation Equivalence

This paper studies supervisory control of discrete event systems subject to specifications modeled as nondeterministic automata. The control is exercised so that the controlled system is simulation equivalent to the (nondeterministic) specification. Properties expressed in the universal fragment of the branching-time logic can equivalently be expressed as simulation equivalence specifications. This makes the simulation equivalence a natural choice for behavioral equivalence in many applications and it has found wide applicability in abstraction-based approaches to verification. While simulation equivalence is more general than language equivalence, we show that existence as well as synthesis of both the target and range control problems remain polynomially solvable. Our development shows that the simulation relation is a preorder over automata, with the union and the synchronization of the automata serving as an infimal upperbound and a supremal lowerbound, respectively. For the special case when the plant is deterministic, the notion of state-controllable-similar is introduced as a necessary and sufficient condition for the existence of similarity enforcing supervisor. We also present conditions for the existence of a similarity enforcing supervisor that is deterministic.     

一种基于MapReduce的OpenFlow网络属性并行验证算法

针对OpenFlow网络中流表配置错误引起转发回路、路由黑洞和访问控制规则失效等问题,提出一种并行的基于MapReduce的OpenFlow网络属性验证算法。通过在Map阶段划分规则等价类,在Reduce阶段为规则等价类构建基于交换机端口谓词的网络转发图并分析可达性,实现对网络属性的并行验证。同时,通过采用原子谓词将传统可达性分析中的规则匹配域多维集合运算转换为整数集合运算,以进一步提高可达性分析效率。此外,基于原子谓词的谓词表达方式可消除交换机端口谓词集合中的冗余项,降低存储开销。最后,通过理论分析和仿真实验验证了算法的正确性及在时间和存储开销方面的优越性。     

车辆安全跟驰模式预测的形式化建模方法

由于传统车辆跟驰建模预测方法无法遍历车辆所有可能的系统输入与运行状态的不确定性, 因而不足以从理论上保证对周边车辆安全跟驰行为预测的完整性与可信性. 为此提出车辆安全跟驰模式预测的形式化建模方法. 该方法利用随机可达集的遍历表现特征实现对周边车辆行为预测的不确定性表述, 并通过马尔科夫链逼近可达集的方式表达系统行为状态变化的随机性, 从而完成对周边车辆跟驰行为状态变化的精确概率预估. 为了表达跟驰情形中车辆之间的行为关联影响以及提高在线计算效率, 离线构建了关联车辆在状态及控制输入之间的安全关联矩阵, 描述周边车辆的安全跟驰控制输入选择规律, 并综合相关车辆的当前状态信息, 达到对周边车辆安全跟驰行为的在线分析与预估. 数值验证不仅表明提出的建模方法完备地表述了周边车辆所有的安全跟驰行为及过程, 显著提高了预测的精确度, 也论证了该方法对车辆跟驰控制策略建模分析与安全验证的有效性.     

Equivalence of dynamical systems by bisimulation

A general notion of bisimulation is defined for linear input-state-output systems, using analogies with the theory of concurrent processes. A characterization of bisimulation and an algorithm for computing the maximal bisimulation relation is derived using geometric control theory. Bisimulation is shown to be a notion which unifies the concepts of state-space equivalence and state-space reduction, and which allows to study equivalence of systems with nonminimal state-space dimension. The notion of bisimulation is especially powerful for "nondeterministic" dynamical systems, and leads in this case to a notion of equivalence which is finer than equality of external behavior. For abstractions of systems it is shown how the results specialize to previously obtained results by other authors. Extensions of the main results to the nonlinear case are provided.