Backward Bisimulation in Markov Chain Model Checking

Equivalence relations can be used to reduce the state space of a system model, thereby permitting more efficient analysis. We study backward stochastic bisimulation in the context of model checking continuous-time Markov chains against continuous stochastic logic (CSL) properties. While there are simple CSL properties that are not preserved when reducing the state space of a continuous-time Markov chain using backward stochastic bisimulation, we show that the equivalence can nevertheless be used in the verification of a practically significant class of CSL properties. We consider an extension of these results to Markov reward models and continuous stochastic reward logic. Furthermore, we identify the logical properties for which the requirement on the equality of state-labeling sets (normally imposed on state equivalences in a model-checking context) can be omitted from the definition of the equivalence, resulting in a better state-space reduction     

随机模型检测连续时间Markov过程

功能正确和性能可满足是复杂系统可信要求非常重要的两个方面。从定性验证和定量分析相结合的角度,对复杂并发系统进行功能验证和性能分析,统一地评估系统是否可信。连续时间Markov决策过程CTMDP(Continuous time Markov decision process)能够统一刻画复杂系统的概率选择、随机时间及不确定性等重要特征。提出用CTMDP作为系统定性验证和定量分析模型,将复杂系统的功能验证和性能分析转化为CTMDP中的可达概率求解,并证明验证过程的正确性,最终借助模型检测器MRMC(Markov Reward Model Chcckcr)实现模型检测。理论分析表明,提出的针对CI'MDP模型的验证需求是必要的,验证思路和方法具有可行性。     

UML状态机的模型检验方法

模型检验是一种确保设计规范正确性的形式化自动验证技术,本文提出了对UML状态机进行模型检验的方法。文中首先对UML状态机的语法和语义进行描述,然后基于语义中的RTC步给出生状态机全局可达状态迁移图的方法,方法的核心是在当前格局下根据使能条件确定所有的最大无冲突迁移集。文章最后给出算法以验证UML状态机是否满足用计算树逻辑（CTL）公式表示的性质。     

具有公平性约束的CTL部分状态空间模型检测

检测部分状态空间是近年来出现的有效解决状态爆炸的模型检测技术，部分Kripke 结构是描述部分状态空间的形式框架。文章主要讨论一类具有公平性约束条件的CTL（计算树逻辑）模型检测问题。定义了部分公平Kripke结构和公平序，分别来表征部分公平状态空间和它们之间的序关系。并给出相应的3值CTL语意和相关定理来说明部分状态空间模型检测技术同样适用于具有公平性约束条件的CTL模型检测问题。     

Constraint Markov Chains

Notions of specification, implementation, satisfaction, and refinement, together with operators supporting stepwise design, constitute a specification theory. We construct such a theory for Markov Chains (MCs) employing a new abstraction of a Constraint MC. Constraint MCs permit rich constraints on probability distributions and thus generalize prior abstractions such as Interval MCs. Linear (polynomial) constraints suffice for closure under conjunction (respectively parallel composition). This is the first specification theory for MCs with such closure properties. We discuss its relation to simpler operators for known languages such as probabilistic process algebra. Despite the generality, all operators and relations are computable.     

Load Balancing Parallel Explicit State Model Checking

This paper first identifies some of the key concerns about the techniques and algorithms developed for parallel model checking; specifically, the inherent problem with load balancing and large queue sizes resultant in a static partition algorithm. This paper then presents a load balancing algorithm to improve the run time performance in distributed model checking, reduce maximum queue size, and reduce the number of states expanded before error discovery. The load balancing algorithm is based on generalized dimension exchange (GDE). This paper presents an empirical analysis of the GDE based load balancing algorithm on three different supercomputing architectures—distributed memory clusters, Networks of Workstations (NOW) and shared memory machines. The analysis shows increased speedup, lower maximum queue sizes and fewer total states explored before error discovery on each of the architectures. Finally, this paper presents a study of the communication overhead incurred by using the load balancing algorithm, which although significant, does not offset performance gains.     

分布式状态机的代数模型及其模型检验算法

分布式状态机（DSM）是一个分布式计算模型，特别适用于反应系统，有广泛的用途，但一般其正确性证明与模型检验的复杂性却很高，不易实用。作者曾提出了一个DSM的代数模型及其模型检验算法，复杂较低，但模型推导过程有点问题。该文加强了对DSM模型检验问题的提法，研究了解的结构特征，证明了可将DSM模型检验问题归结为不动点计算问题，并将Cleaveland和Steffen求不动点的方法用于同步模型不动点计算过程，然后将Bertsekas关于欧氏空间上的异步收敛定理推广到完备格上，从而将求解异步DSM方程不动点问题转化为求解同步方程不动点问题，证明了在适当的条件下，有vgEA＝vgES,vgES与vgEA分别是DSM同步方程与异步方程的大不同动点，该同步算法的复杂性为O（|S|log|TRAN|),S为状态集，TRAN为转移关系式集，利用本文结果，可以有效地克服了DSM进程之间的并发干扰所带来的各种困难，对分布式反应系统的可靠设计有很大的帮助。     

Multiplicativity of Markov Chains with Multiaddress Routing

A broad class of network Markov processes (including open queueing networks) with multiaddress routing and one type of calls is considered. Under such routing, the same call can simultaneously arrive at several nodes. For these processes, we found necessary and sufficient conditions of multiplicativity, that is, conditions of representability of a stationary distribution as a product of factors characterizing separate nodes.     

Symbolic Bounded Model Checking of Abstract State Machines

Abstract State Machines (ASMs) allow modeling system behaviors at any desired level of abstraction, including a level with rich data types, such as sets, sequences, maps, and user-de.ned data types. The availability of high-level data types allow state elements to be represented both abstractly and faithfully at the same time. In this paper we look at symbolic analysis of ASMs. We consider ASMs over a .xed state background T that includes linear arithmetic, sets, tuples, and maps. For symbolic analysis, ASMs are translated into guarded update systems called model programs. We formulate the problem of bounded path exploration of model programs, or the problem of Bounded Model Program Checking (BMPC) as a satis.ability problem modulo T . Then we investigate the boundaries of decidable and undecidable cases for BMPC. In a general setting, BMPC is shown to be highly undecidable (Σ₁¹ -complete); and even when restricting to .nite sets the problem remains re-hard (Σ⁰₁-hard). On the other hand, BMPC is shown to be decidable for a class of basic model programs that are common in practice. We use Satis.ability Modulo Theories (SMT) for solving BMPC; an instance of the BMPC problem is mapped to a formula, the formula is satis.able modulo T if and only if the corresponding BMPC problem instance has a solution. The recent SMT advances allow us to directly analyze speci.cations using sets and maps with specialized decision procedures for expressive fragments of these theories. Our approach is extensible; background theories need in fact only be partially solved by the SMT solver; we use simulation of ASMs to support additional theories that are beyond the scope of available decision procedures.     

Interval-Valued Finite Markov Chains

The requirement that precise state and transition probabilities be available is often not realistic because of cost, technical difficulties or the uniqueness of the situation under study. Expert judgements, generic data, heterogeneous and partial information on the occurrences of events may be sources of the probability assessments. All this source information cannot produce precise probabilities of interest without having to introduce drastic assumptions often of quite an arbitrary nature. in this paper the theory of interval-valued coherent previsions is employed to generalise discrete Markov chains to interval-valued probabilities. A general procedure of interval-valued probability elicitation is analysed as well. In addition, examples are provided.     

以状态子集为中心的并行模型检测算法

以线性时序逻辑LTL（Linear Temporal Logic）模型检测算法为研究对象,提出以状态子集为中心的并行模型检测算法.针对传统单机多核算法同步开销大的缺点,新算法充分利用状态子集的稠密特性动态调度任务,从而降低同步开销,提高算法并行度.本文基于轻量级单机图计算框架Ligra,结合检测过程中状态子集的特性,设计并实现新的在线（on-the-fly）模型检测算法.与现有算法相比,在模型检测的效率上可以提升20-30%,具有高扩展性特征.     

模型检测中状态爆炸问题研究综述

模型检测已成为保证软件系统正确性和可靠性的重要手段,但随着软件功能日益强大,其规模和复杂度也越来越大,在模型检测过程中容易产生状态爆炸问题。如何解决模型检测中的状态爆炸,已成为工业界和理论界无法回避的重要课题。系统地综述模型检测领域解决状态爆炸问题的关键技术和主要方法,并提出该领域的最新研究进展与方向。     

联合吸收马尔可夫链和骨架映射的视频分割

因严重遮挡和剧烈形变等挑战长期共存,精准鲁棒的视频分割已成为计算机视觉的热点之一.构建联合吸收马尔可夫链和骨架映射的视频分割方法,经由“预分割—后优化—再提升”逐步递进地生成精准目标轮廓.在预分割阶段,基于孪生网络和区域生成网络获取目标感兴趣区域,建立这些区域内超像素的吸收马尔可夫链,计算出超像素的前景/背景标签.吸收马尔可夫链可灵活有效地感知和传播目标特征,能从复杂场景初步预分割出目标物体.后优化阶段,设计短期时空线索模型和长期时空线索模型,以获取目标的短期变化规律和长期稳定特征,进而优化超像素标签,降低相似物体和噪声带来的误差.在再提升阶段,为减少优化结果的边缘毛刺和不连贯,基于超像素标签和位置,提出前景骨架和背景骨架的自动生成算法,并构建基于编解码的骨架映射网络,以学习出像素级目标轮廓,最终得到精准视频分割结果.标准数据集的大量实验表明:所提方法优于现有主流视频分割方法,能够产生具有更高区域相似度和轮廓精准度的分割结果.     

Predicate Abstraction and Refinement for Model Checking VHDL State Machines

In this paper we present an automatic combination of abstraction-refinement by which we translate a VHDL model describing a state system to an initial equivalent abstract system described by SMV to explore its state space to verify CTL properties. We present the method implemented to compute automatically abstractions using decision procedures. This method can handle different kinds of infinite state systems including systems composed of concurrent components and it can be extended for more complex VHDL concepts. Abstract models may admit spurious counterexamples (false negative results) which are executions at the abstract level with no corresponding executions at the concrete level. We devise a new algorithm which analyzes such counterexamples and refine the abstract model correspondingly by eliminating gradually the false negative results. We illustrate our approach on an example and we confirm its effectiveness on a large design.     

Markov Chains and Markov Decision Processes in Isabelle/HOL

This paper presents an extensive formalization of Markov chains (MCs) and Markov decision processes (MDPs), with discrete time and (possibly infinite) discrete state-spaces. The formalization takes a coalgebraic view on the transition systems representing MCs and constructs their trace spaces. On these trace spaces properties like fairness, reachability, and stationary distributions are formalized. Similar to MCs, MDPs are represented as transition systems with a construction for trace spaces. These trace spaces provide maximal and minimal expectation over all possible non-deterministic decisions. As applications we provide a certifier for finite reachability problems and we relate the denotational semantics and operational semantics of the probabilistic guarded command language. A distinctive feature of our formalization is the order-theoretic and coalgebraic view on our concepts: we view transition systems as coalgebras, we view traces as coinductive streams, we provide iterative computation rules for expectations, and we define many properties on traces as least or greatest fixed points.     

An Elementary Derivation of the Large Deviation Rate Function for Finite State Markov Chains

Large deviation theory is a branch of probability theory that is devoted to a study of the “rate” at which empirical estimates of various quantities converge to their true values. The object of study in this paper is the rate at which estimates of the doublet frequencies of a Markov chain over a finite alphabet converge to their true values. In the case where the Markov process is actually an independent and identically distributed (i.i.d.) process, the rate function turns out to be the relative entropy (or Kullback‐Leibler divergence) between the true and the estimated probability vectors. This result is a special case of a very general result known as Sanov's theorem and dates back to 1957. Moreover, since the introduction of the “method of types” by Csiszar and his co‐workers during the 1980s, the Proof of this version of Sanov's theorem has been “elementary,” using some combinatorial arguments. However, when the i.i.d. process is replaced by a Markov process, the available Proofs are far more complex. The main objective of this paper is therefore to present a first‐principles derivation of the LDP for finite state Markov chains, using only simple combinatorial arguments (e.g. the method of types), thus gathering in one place various arguments and estimates that are scattered over the literature. The approach presented here extends naturally to multi‐step Markov chains.     

Consistency and refinement for Interval Markov Chains

Interval Markov Chains (IMC), or Markov Chains with probability intervals in the transition matrix, are the base of a classic specification theory for probabilistic systems [18]. The standard semantics of IMCs assigns to a specification the set of all Markov Chains that satisfy its interval constraints. The theory then provides operators for deciding emptiness of conjunction and refinement (entailment) for such specifications.In this paper, we study complexity of several problems for IMCs, that stem from compositional modeling methodologies. In particular, we close the complexity gap for thorough refinement of two IMCs and for deciding the existence of a common implementation for an unbounded number of IMCs, showing that these problems are EXPTIME-complete.We discuss suitable notions of determinism for specifications, and show that for deterministic IMCs the syntactic refinement operators are complete with respect to model inclusion. Finally, we show that deciding consistency (emptiness) for an IMC is polynomial and that existence of common implementation can be established in polynomial time for any constant number of IMCs.     

Exogenous量子马尔可夫链及其可达性分析

为了刻画开放量子系统的量子属性,扩展现有的量子马尔可夫链是有必要的.通过构建Exogenous量子算子逻辑,定义了Exogenous量子马尔可夫链.作为新型量子马尔可夫链,重点研究了4种可达性公式,给出可达性公式可满足性问题的求解,并分析了它们的可判定性问题.作为应用,实例说明广义量子Loop程序的终止问题可以归结为Exogenous量子马尔可夫链的最终可达性,进而通过检测量子公式可满足性来判定程序的终止问题.     

模型检测规划中的状态之间的可达关系研究

当前,对基于模型检测规划研究的算法中存在大量的冗余计算,一些不可能参与构成解的状态动作序偶被反复筛选.文中给出了一种在不确定规划领域求规划解的新思路:在求规划解之前,找到不确定状态转移系统的状态之间的可达关系,从而根据状态之间的可达关系进行约简.提出了不确定状态转移系统的超图、超图的邻接矩阵和可达矩阵等概念,设计了用超图的邻接矩阵求不确定状态转移系统中状态之间可达关系的方法.利用不确定状态转移系统的超图、超图的邻接矩阵和状态之间的可达关系获得了关于弱规划解、强规划解和强循环规划解的一些重要性质.这些性质是关于一些状态动作序偶是否不可能参与构成弱规划解、强规划解和强循环规划解的结论.通过这些性质可以将大量的状态动作序偶直接去掉,从而大幅度简化求规划解的过程,提高求规划解效率.