一种动态消减时间自动机可达性搜索空间的方法

时间自动机的可达性分析算法通常采用对符号状态的枚举来遍历其状态空间。符号状态由位置与时间区域组成，时间区域用形如x-y≤（〈）n的原子公式的合取式来表示。在对时间自动机进行可达性分析的过程中，分析算法将生成大量的符号状态，往往导致对计算机内存的需求超出了可行的范围。本文给出了一个消减符号状态个数的方法。该方法通过对符号状态间的依赖关系进行分析，在不影响分析结果的前提下消去某些时间区域的原子公式，从而扩展符号状态。扩展后的符号状态包含有更加多的其它的状态，通过删除掉那些被包含的符号状态可以减少算法存储的状态个数，节省存储空间。本文最后给出了相关的案例分析，结果表明这个算法有效地减少了某些时间自动机可达性分析过程中所需的存储空间。     

实时系统的模型检验中针对共享变量的优化技术

实时系统可以使用由多个并发的时间自动机组成的时间自动机网络来建模。网络中的时间自动机通过共享变量和/或信道交互。带有不同共享变量取值的自动机网络的状态是截然不同的。因此，共享变量也是引起状态空间爆炸问题的原因之一。本文提出了在不同共享变量取值之间的兼容性关系的概念。使用这种兼容性关系，时间自动机网络的可达性分析算法就可以减少需要遍历的状态的个数。本文给出了检测符号化状态中共享变量的取值所能兼容的其它取值的算法以及进一步进行这种兼容性关系检测的增强算法。最后还给出了使用了这两种算法进行优化之后的可迭性分析算法。实验结果显示经优化的可达性分析算法的空间效率得到了显著的提高。     

自动验证并发实时系统的线性时段性质

介绍了一个就线性时段性验证实时系统正确性的工具的设计思想以及相关算法,使用时间自动机作为产时系统的描述模型,同时,为了便珩描述并发实时系统,使用带共享变量和通道的时间自动机网作为模型描述并发实时系统,在检验时间自动机网时,用户可以使用工具提供的合成程序将其合并为一个时间自动机然后进行检验,由于时间自动机的状态空间是无究的,通过引入整数状态和状态等价关系的概念,将整个状态0空间划分为有限的状态等价类空间,模型检验过程只需要通过对等价类空间的搜索就可以完成,但往往等价类空间的规模很大,超出了现在计算机的处理能力,原始搜索算法仅仅在理论上是可知地的,为了增工具的使用性,工具中使用的算法运用了一些优化技术来避免对等价类空间的穷尽搜索,使得工具在使用时具有比较好的时间和空间效率。     

构件式实时系统建模与验证研究

在复杂的实时系统开发中使用构件式设计方法已成为目前软件开发领域中的研究热点,如何有效地验证实时软件的设计是否满足给定的时间需求并降低验证过程的复杂度,是实时计算领域中的主要挑战之一.文中对构件接口模型进行时间扩展,提出了时间接口模型,并将其用于构件接口交互行为的形式化建模.在接口自动机理论的的基础上进一步提出了时间接口自动机模型用于描述时间接口交互下构件的行为及组合方法,通过消除错误状态产生组合模型来约减构件时间接口自动机模型的积,并在约减的模型上进行性质检验,降低了分析复杂度,有效地应对状态空间爆炸问题.为了说明论文建议的方法,详细讨论了一个简单的、贯穿整篇论文的示例系统.     

基于扩展RED图的概率时间自动机可达性分析

RED图可以表示一个完整的时间自动机上的状态集,包括其连续时间部分和离散部分.在它基础上实现的模型检测工具RED,在时间自动机模型检测中表现出了优良的性能.另一方面,现有的概率时间自动机模型检测工具仍然使用不同的方法来分别表示概率时间自动机状态的连续时间和离散部分.我们在复用原始RED图的数据结构的基础上,对其做出了扩展,以令其支持概率状态的表达,同时保持其性能方面的优势.我们又为此实现了一个概率时间自动机可达性分析工具原型,并将其与两个概率模型检测工具（PRISM和Modest）就概率时间自动机可达性分析作实验对比,来评估该工具原型的性能.实验结果显示,我们的集成表示概率状态空间的方式,确实提高了概率时间自动机模型检测的时间效率和延展性.     

时间自动机可达性分析算法的改进

模型检测时,实时系统的大多数安全属性和部分活性都可以通过可达性分析算法来验证。本文介绍了时间自动机和可达性分析算法,并对可达性分析算法中的后继算法进行了改进。     

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

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

一种基于时间自动机的域构造方法

模型检验是一种重要的形式化自动验证技术,通过状态空间搜索来保证软硬件设计的正确性。由于TCTL不是针对时间自动机,而是针对有限状态变迁系统的,从而无法使用TCTL直接对时间自动机进行模型检验。给出了一种从时间自动机到有限状态变迁系统的方法,并在不改变时间自动机的语义上,使时间自动机等价后的域状态数尽可能少,在一定程度上有效地解决了状态空间爆炸问题。     

基于场景构件式实时软件设计的一致性检验

在复杂的实时软件系统中使用构件式设计方法,已成为目前软件工程中的研究热点.如何有效地验证实时软件的设计是否满足给定的时间规约,是实时计算领域中的主要挑战之一.通过在接口自动机模型中添加时间区间标记,来扩展其对实时系统接口行为的表达能力;使用实时接口自动机网络来描述实时软件系统的构件式设计模型;使用带布尔不等式时间约束的UML顺序图表示基于场景的需求规约,对系统设计阶段实时软件构件的动态行为进行形式化分析与检验.通过对实时接口自动机网络状态空间的分析,构造了其可兼容的整型状态等价类空间的可达图,并在此基础上给出了验证算法,以检验构件式实时软件系统的设计与带时间约束的场景式规约之间的一致性.     

一种基于时间自动机的时钟等价性优化方法

提出了一种优化模型检验时间自动机的时钟等价规则,通过优化的时钟等价规则,使时间自动机等价后的域自动机状态数尽可能少,并在此基础上定义了适合于优化时钟等价规则的域自动机.优化时钟等价规则,在一定程度上有效地解决了状态空间爆炸问题.     

系统多功能状态表达式构建及其置信度研究

为研究具有多功能的系统功能状态表达式及状态评价结果的置信度,提出一种基于集对分析和量子态叠加的系统功能状态表示方法。首先论述了系统功能状态置信度;其次研究了系统单功能状态表示,使用集对分析联系数构建表达式确定分量系数,随后利用量子态叠加构建系统单功能状态表达式;最后构建了系统多功能状态表达式,从而确定系统多功能状态的量子叠加态概率幅,其平方即为该状态的系统功能状态评价结果的置信度。通过实例对所提方法进行了应用,说明了计算流程和作用。研究可提供系统多功能状态置信度的计算方法。     

State filters on fuzzy structures with internal states

The aim of this paper is the study of some properties of the state filters of a state pseudo BL-algebra \(\left( A,\sigma \right) \) and also some properties of a state pseudo BL-algebra. By introducing the concepts of simple, semisimple and local state pseudo BL-algebra relative to its state filters set, we present some characterizations of a simple, semisimple and local state pseudo BL-algebras. Also, we adjust a result from universal algebra (Chinese remainder theorem) and, by introducing the concept of a primary state filter on a state BL-algebra, we present a characterization of a local state BL-algebra. We introduce the notion of extended state filter of a state filter associated to a subset of a state pseudo BL-algebra.     

Condensed state spaces for symmetrical Coloured Petri Nets

This paper deals with state spaces. A state space is a directed graph with a node for each reachable state and an arc for each possible state change. We describe how symmetries of the modelled system can be exploited to obtain much more succinct state space analysis. The symmetries induce equivalence classes of states and equivalence classes of state changes. It is then possible to construct a condensed state space where each node represents an equivalence class of states while each arc represents an equivalence class of state changes. Such a condensed state space is often much smaller than the full state space and it is also much faster to construct. Nevertheless, it is possible to use the condensed state space to verify the same kind of behavioural properties as the full state space. hence, we do not lose analytic power.We define state spaces and condensed state spaces for a language called Coloured Petri Nets (CP-nets). This language is in widespread use for the modelling and analysis of concurrent systems. However, our techniques are general and they can be used for many other kinds of labelled transition systems. The paper does not assume that the reader is familiar with CP-nets (or Petri nets in general)—although such knowledge will, of course, be a help. The first four sections of the paper introduce the basic concepts of CP-nets. The next three sections deal with state spaces, condensed state spaces and computer tools for state space analysis. Finally, there is a short conclusion.     

State transfer based on decoherence-free target state by Lyapunov-based control

We propose a Lyapunov-based control approach for state transfer based on the decoherence-free target state.The expected target state is constructed to be a decoherence-free state in a decoherence-free subspace(DFS) by an external laser fieldⅠ,so that the system state can be decoupled from the environment,and no more decoherence process will occur.With the decoherence-free target state,we design a Lyapunov-based control fieldⅡto steer the given initial state to the decoherence-free state of open quantum systems as completely as possible,and decouple the system state from the environment at the same time.In the end,it is verified that the state transfer control designed comes true on a∧-type four-level atomic system,and the system can stay on the decoherence-free target state without coupling to environment.     

On pseudo BL-algebras with internal state

The scope of this paper is to put in evidence some characteristics and properties of the operations with state filters of a pseudo BL-algebra with internal state. I define the concepts of maximal and prime state filter of a state pseudo BL-algebra, I characterize a maximal state filter and I prove a Prime state filter theorem. Also, I characterize the state-filters algebra of a state pseudo BL-algebra.     

Minimal prime state filters and state radicals on state pseudo $${ }$$-algebras

The aim of this paper is the study of some classes of state filters of a state pseudo BL-algebra. The concepts of minimal prime state filter and of state hyperarchimedean pseudo BL-algebra are introduced and a characterization of a state hyperarchimedean pseudo BL-algebra is presented. Also, we define the notion of a state radical of a state filter of a state pseudo BL-algebra, we present a characterization of a state radical and some of its properties. The algebra of state radicals of a state pseudo BL-algebra is studied.     

基于形式化规格说明的UML状态图提取

为了辅助软件开发者理解形式化规格说明,提出一种从B方法规格说明中提取UML状态图的方法。通过分析状态信息在规格说明中的表现形式,定义一系列精确的简单状态、状态迁移、复合迁移、分层状态和状态图通信等提取规则。借助状态变量表和状态迁移表,最终实现状态元素和状态关系的提取,并以此构造完整的UML状态图。实验结果验证了方法的正确性及有效性。     

Exploring the state sequence space for hidden Markov and semi-Markov chains

The knowledge of the state sequences that explain a given observed sequence for a known hidden Markovian model is the basis of various methods that may be divided into three categories: (i) enumeration of state sequences; (ii) summary of the possible state sequences in state profiles; (iii) computation of a global measure of the state sequence uncertainty. Concerning the first category, the generalized Viterbi algorithm for computing the top L most probable state sequences and the forward-backward algorithm for sampling state sequences are derived for hidden semi-Markov chains and hidden hybrid models combining Markovian and semi-Markovian states. Concerning the second category, a new type of state (and state change) profiles is proposed. The Viterbi forward-backward algorithm for computing these state profiles is derived for hidden semi-Markov chains and hidden hybrid models combining Markovian and semi-Markovian states. Concerning the third category, an algorithm for computing the entropy of the state sequence that explains an observed sequence is proposed. The complementarity and properties of these methods for exploring the state sequence space (including the classical state profiles computed by the forward-backward algorithm) are investigated and illustrated with examples.     

An Inspection Policy for Deteriorating Processes Using Delay-Time Concept

A method for determining the discrete time points of inspection for a deteriorating single-unit system under condition-based maintenance is developed. The system is in a normal state, a symptom state or a failed state. A delay-time model is utilized to describe the transition of the states. The transition time from a normal state to a symptom state and that from a symptom state to a failed state are derived assuming continuous deteriorating processes based on a reaction rate model which is categorized as a failure physics model. Failed-dangerous and failed-safe probabilities of an imperfect inspection are considered. A method for minimizing the long-run average cost per unit time is formulated. The characteristics and sensitivity of the proposed method are investigated.     

多跳远程量子态制备

多跳远程量子态制备在量子无线网络、长距离量子信息传输中有重要价值。融合多跳隐形传态和远程态制备的思想，提出一个多跳远程任意单量子态制备协议。在每一跳中都以三粒子非最大纠缠GHz态为量子信道，利用远程态制备方法，原始单量子态通过中间节点逐跳被制备，每跳恢复的态被用着下一跳被制备的态。通过对单跳和两跳制备的分析，获得了[n]跳制备后方案成功的概率。在协议中，仅涉及到Pauli算子、单粒子测量和前馈策略，因此该方案易于物理实现。