A trace-based model for multiparty contracts

In this article we present a model for multiparty contracts in which contract conformance is defined abstractly as a property on traces. A key feature of our model is blame assignment, which means that for a given contract, every breach is attributed to a set of parties. We show that blame assignment is compositional by defining contract conjunction and contract disjunction. Moreover, to specify real-world contracts, we introduce the contract specification language CSL with an operational semantics. We show that each CSL contract has a counterpart in our trace-based model and from the operational semantics we derive a run-time monitor. CSL overcomes limitations of previously proposed formalisms for specifying contracts by supporting: (history sensitive and conditional) commitments, parametrised contract templates, relative and absolute temporal constraints, potentially infinite contracts, and in-place arithmetic expressions. Finally, we illustrate the general applicability of CSL by formalising in CSL various contracts from different domains.     

Probabilistic symbolic model checking with PRISM: a hybrid approach

In this paper we present efficient symbolic techniques for probabilistic model checking. These have been implemented in PRISM, a tool for the analysis of probabilistic models such as discrete-time Markov chains, continuous-time Markov chains and Markov decision processes using specifications in the probabilistic temporal logics PCTL and CSL. Motivated by the success of model checkers such as SMV which use BDDs (binary decision diagrams), we have developed an implementation of PCTL and CSL model checking based on MTBDDs (multi-terminal BDDs) and BDDs. Existing work in this direction has been hindered by the generally poor performance of MTBDD-based numerical computation, which is often substantially slower than explicit methods using sparse matrices. The focus of this paper is a novel hybrid technique which combines aspects of symbolic and explicit approaches to overcome these performance problems. For typical examples, we achieve a dramatic improvement over the purely symbolic approach. In addition, thanks to the compact model representation using MTBDDs, we can verify systems an order of magnitude larger than with sparse matrices, while almost matching or even beating them for speed.     

Simultaneous coordination of order quantity and reorder point in a two-stage supply chain

In this paper, we investigate the simultaneous coordination of order quantity and reorder point in a two-stage supply chain (SC). While coordination of order quantity has received much attention in the supply chain management literature, coordination of the reorder point has been less-studied. The retailer's reorder point has a direct impact on product availability and customer service level (CSL) and therefore has a great impact on SC profitability. Our proposed model adopts a two-stage SC with stochastic demand and lead times over multiple periods. The proposed coordination model assures global optimization of order quantity–reorder point decisions. Using a pricing scheme with a discount factor, we extract conditions in which both downstream and upstream members have sufficient motivation to participate in the coordination scheme. Numerical experiments demonstrate that the proposed model can achieve channel coordination. Results of the modeling and analyses show that coordination of both reorder point and order quantity can lead to increased SC profitability as well as CSL improvement.     

Model Checking Markov Chains with Actions and State Labels

In the past, logics of several kinds have been proposed for reasoning about discrete-time or continuous-time Markov chains. Most of these logics rely on either state labels (atomic propositions) or on transition labels (actions). However, in several applications it is useful to reason about both state properties and action sequences. For this purpose, we introduce the logic as CSL which provides a powerful means to characterize execution paths of Markov chains with actions and state labels. asCSL can be regarded as an extension of the purely state-based logic CSL (continuous stochastic logic). In asCSL, path properties are characterized by regular expressions over actions and state formulas. Thus, the truth value of path formulas depends not only on the available actions in a given time interval, but also on the validity of certain state formulas in intermediate states. We compare the expressive power of CSL and asCSL and show that even the state-based fragment of asCSL is strictly more expressive than CSL if time intervals starting at zero are employed. Using an automaton-based technique, an asCSL formula and a Markov chain with actions and state labels are combined into a product Markov chain. For time intervals starting at zero, we establish a reduction of the model checking problem for asCSL to CSL model checking on this product Markov chain. The usefulness of our approach is illustrated with an elaborate model of a scalable cellular communication system, for which several properties are formalized by means of asCSL formulas and checked using the new procedure     

Model checking expected time and expected reward formulae with random time bounds

In this paper, we extend CSL (continuous stochastic logic) with an expected time and an expected reward operator, both of which are parameterized by a random terminal time. With the help of such operators we can state, for example, that the expected sojourn time in a set of goal states within some generally distributed delay is at most (at least) some time threshold. In addition, certain performance measures of systems which contain general distributions can be calculated with the aid of this extended logic. We extend the efficient model checking of CTMCs against the logic CSL developed by Katoen et al. [1] to cater for the new operator. Our method involves precomputing a family of mixed Poisson expected sojourn time coefficients for a range of random variables which includes Pareto, uniform and gamma distributions, but otherwise carries the same computational cost as calculating CSL until formulae.     

Direct observation of the electrical activity of coincidence‐site lattice boundaries in location‐controlled silicon islands using scanning spread resistance microscopy

Abstract— Scanning spread resistance microscopy (SSRM) was used to investigate the electrical activity of coincidence‐site lattice (CSL) boundaries in location‐controlled silicon islands fabricated using the μ‐Czochralski (μ‐CZ) process. Using SSRM, the electrical activity of random and Σ3 and Σ9 CSL boundaries, which are determined by electron backscattered diffraction (EBSD) analysis, were observed. Quantitative evaluation of the microscopic current mapping by SSRM revealed that Σ3 and Σ9 CSL boundaries, of which most of them are coherent, have much less electrical activity than the random grain boundaries. Some of the Σ3 and Σ9 CLS boundaries seemed to be incoherent, while the number of such incoherent CSL boundaries are very much limited according to previous TEM investigation and showed increased activities; however, their activities are still lower than that of the random boundaries.     

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     

Model Checking Timed and Stochastic Properties with CSL^{TA}

Markov chains are a well-known stochastic process that provide a balance between being able to adequately model the system's behavior and being able to afford the cost of the model solution. The definition of stochastic temporal logics like continuous stochastic logic (CSL) and its variant asCSL, and of their model-checking algorithms, allows a unified approach to the verification of systems, allowing the mix of performance evaluation and probabilistic verification. In this paper we present the stochastic logic CSLTA, which is more expressive than CSL and asCSL, and in which properties can be specified using automata (more precisely, timed automata with a single clock). The extension with respect to expressiveness allows the specification of properties referring to the probability of a finite sequence of timed events. A typical example is the responsiveness property "with probability at least 0.75, a message sent at time 0 by a system A will be received before time 5 by system B and the acknowledgment will be back at A before time 7", a property that cannot be expressed in either CSL or asCSL. We also present a model-checking algorithm for CSLTA.     

面向汉语作为第二语言学习的个性化语法纠错

语法纠错任务旨在通过自然语言处理技术自动检测并纠正文本中的语序、拼写等语法错误.当前许多针对汉语的语法纠错方法已取得较好的效果,但往往忽略了学习者的个性化特征,如二语等级、母语背景等.因此,该文面向汉语作为第二语言的学习者,提出个性化语法纠错,对不同特征的学习者所犯的错误分别进行纠正,并构建了不同领域汉语学习者的数据集...     

Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes

In a recent paper Baier et al. [Lecture Notes in Computer Science, Springer-Verlag, 2000, p. 358] analyzed a new way of model-checking formulas of a logic for continuous-time processes—called continuous stochastic logic (henceforth CSL)—against continuous-time Markov chains—henceforth CTMCs. One of the important results of that paper was the proof that if two CTMCs were bisimilar then they would satisfy exactly the same formulas of CSL. This raises the converse question—does satisfaction of the same collection of CSL formulas imply bisimilarity? In other words, given two CTMCs which are known to satisfy exactly the same formulas of CSL does it have to be the case that they are bisimilar? We prove that the answer to the question just raised is “yes”. In fact we prove a significant extension, namely that a subset of CSL suffices even for systems where the state space may be a continuum. Along the way we prove a result to the effect that the set of Zeno paths has measure zero provided that the transition rates are bounded.     

基于词根的中国手语识别方法

迄今为止，手语识别面临的最大问题是如何解决词汇集易扩充的连续识别，提出一种大词汇量连续中国手语识别方法，将词根作为识别基元，由于基元的数目是有限的，因此基于HMM的手语信号的训练和识别变得比较容易处理，可以实现更大词汇量的识别。除此之外，所提方法还有利于实现手势语和手指语的混合识别。从中国手语中共整理现2400多个词根，为每个词根建一个并行的HMM模型，对各数据流的HMM模型进行聚集，确定出手识别的基元。根据这些基元对手妫刻苦骊，并建立了树状搜索网络，使用状态垄点上高斯密度函数聚类、语言模型和N－Best方法提高系统的速度和精度。对5119个手语词做了实验，连续语句的识别率可在90％以上。     

基于SRN/HMM的非特定人连续手语识别系统

手语识别是通过计算机提供一种有效而准确的机制将手语翻译成文本或语音。目前最新发展水平的手语识别系统在实际应用中应解决非特定人连续手语问题。提出一种将连续手语识别分解成各弧立词识别的分治方法，用于非特定人连续手语识别。把精简循环网（simple recurrent network,简称SRN）作为连续手语的段边界检测器，把SRN分段结果作为隐马可夫模型（hidden Markov models,简称HMM）框架中的状态输入，在HMM框架里使用网格Viterbi算法搜索出一条最佳手语词路径。实验结果表明，该方法的识别效果比单纯使用HMM要好。     

Numerical vs. statistical probabilistic model checking

Numerical analysis based on uniformisation and statistical techniques based on sampling and simulation are two distinct approaches for transient analysis of stochastic systems. We compare the two solution techniques when applied to the verification of time-bounded until formulae in the temporal stochastic logic CSL, both theoretically and through empirical evaluation on a set of case studies. Our study differs from most previous comparisons of numerical and statistical approaches in that CSL model checking is a hypothesis-testing problem rather than a parameter-estimation problem. We can therefore rely on highly efficient sequential acceptance sampling tests, which enables statistical solution techniques to quickly return a result with some uncertainty. We also propose a novel combination of the two solution techniques for verifying CSL queries with nested probabilistic operators.     

磨矿破碎过程粒度分布的分布式参数蒙特卡洛动力学模拟及加速方法

本文针对磨矿破碎过程,提出一种分布式参数蒙特卡洛动力学方法的粒度分布预测模型和模拟算法.该算法采用了分段思想,将磨机沿着轴向分为若干个虚拟的子磨机;根据破裂、前向和后向移动三类微观事件定义了倾向函数和系统状态矩阵,并设计了分布式算法的调度策略.此外,针对蒙特卡洛动力学算法效率低的问题,提出了基于τ-leap的磨矿过程分布式参数蒙特卡洛模拟加速算法.为了解决分布式参数更新过程中状态不一致的问题,创新性地提出了一种基于缓冲区的同步方法.通过对仿真案例的分析表明,本文提出的分布式参数蒙特卡洛动力学算法具有较高的精度,提出的基于τ-leap的加速算法能够显著提高计算效率,同时保持较好的精度.     

Formal verification of concurrent programs with read-write locks

Read-write locking is an important mechanism to improve concurrent granularity, but it is difficult to reason about the safety of concurrent programs with read-write locks. Concurrent separation logic (CSL) provides a simple but powerful technique for locally reasoning about concurrent programs with mutual exclusive locks. Unfortunately, CSL cannot be directly applied to reasoning about concurrent programs with read-write locks due to the different concurrent control mechanisms.This paper focuses on extending CSL and presenting a proof-carrying code (PCC) system for reasoning about concurrent programs with read-write locks. We extend the heap model with a writing permission set, denoted as logical heap, then define “strong separation” and “weak separation” over logical heap. Following CSL’s local-reasoning idea, we develop a novel program logic to enforce weak separations of heap between different threads and provide verification of concurrent programs with read-write locks.     

基于物理拓扑的P2P网络模型

对等网络的拓扑失配会引起不必要的网络流量,不仅加重了物理网络的负担,而且加大了节点间资源搜索的平均时延。提出一种基于物理拓扑信息的P2P网络模型CSL。CSL模型是以自治系统之间的物理连接构成Center层,以节点的网络地址构成Super层,由普通节点形成Leaf层的三层模型,并采用相应的算法维护网络的运行。通过实验表明,CSL模型在资源搜索时可以明显降低系统的平均时延。针对拓扑失配问题提出的CSL模型可以很好的工作,特别是节点规模较大时在减轻网络负担和降低资源搜索的平均时延方面表现更好。     

On log-tape isomorphisms of complete sets

In this paper we study log n-tape computable reductions between sets and investigate conditions under which log n-tape reductions between sets can be extended to log n-tape computable isomorphisms of these sets. As an application of these results we obtain easy to check necessary and sufficient conditions that sets complete under log n-tape reductions in NL, CSL, P, NP, PTAPE, etc. are log n-tape isomorphic to the previously known complete sets in the respective classes. As a matter of fact, all the “known” complete sets for NL, CSL, P, NP, PTAPE, etc. are now easily seen to be, respectively, log n-tape isomorphic. These results strengthen and extend substantially the previously known results about polynomial time computable reductions and isomorphisms of NP and PTAPE complete sets. Furthermore, we show that any set complete in CSL, PTAPE, etc. must be dense and therefore, for example, cannot be over a single letter alphabet.     

Formal verification of concurrent programs with read-write locks

Read-write locking is an important mechanism to improve concurrent granularity, but it is difficult to reason about the safety of concurrent programs with read-write locks. Concurrent separation logic (CSL) provides a simple but powerful technique for locally reasoning about concurrent programs with mutual exclusive locks. Unfortunately, CSL cannot be directly applied to reasoning about concurrent programs with read-write locks due to the different concurrent control mechanisms. This paper focuses on extending CSL and presenting a proof-carrying code (PCC) system for reasoning about concurrent programs with read-write locks. We extend the heap model with a writing permission set, denoted as logical heap, then define “strong separation” and “weak separation” over logical heap. Following CSL’s local-reasoning idea, we develop a novel program logic to enforce weak separations of heap between different threads and provide verification of concurrent programs with read-write locks.     

一种可信子空间标志方法*

在D-S证据理论的基础上,给出了可信子空间的定义及能够发现所有可信子空间的贪心算法CSL(creditable subspace labeling)。该方法迭代地发现原始特征空间的信任子空间集Cs。用户根据应用领域的需求, 对Cs中的每个可信子空间调用传统聚类算法发现聚类结果。实验结果表明,CSL具有正确发现原始特征空间的真实子空间的能力,为传统聚类算法处理高维数据空间聚类问题提供了一种新的途径。