Weak bisimulation for Probabilistic Timed Automata

We are interested in describing timed systems that exhibit probabilistic behaviour. To this purpose, we consider a model of Probabilistic Timed Automata and introduce a concept of weak bisimulation for these automata, together with an algorithm to decide it. The weak bisimulation relation is shown to be preserved when either time, or probability is abstracted away. As an application, we use weak bisimulation for Probabilistic Timed Automata to model and analyze a timing attack on the dining cryptographers protocol.     

Branching bisimulation for probabilistic systems: Characteristics and decidability

We address the concept of abstraction in the setting of probabilistic reactive systems, and study its formal underpinnings for the strictly alternating model of Hansson. In particular, we define the notion of branching bisimilarity and study its properties by studying two other equivalence relations, viz. coloured trace equivalence and branching bisimilarity using maximal probabilities. We show that both alternatives coincide with branching bisimilarity. The alternative characterisations have their own merits and focus on different aspects of branching bisimilarity. Coloured trace equivalence can be understood without knowledge of probability theory and is independent of the notion of a scheduler. Branching bisimilarity, rephrased in terms of maximal probabilities gives rise to an algorithm of polynomial complexity for deciding the equivalence. Together they give a better understanding of branching bisimilarity. Furthermore, we show that the notions of branching bisimilarity in the alternating model of Hansson and in the non-alternating model of Segala differ: branching bisimilarity in the latter setting turns out to discriminate between systems that are intuitively branching bisimilar.     

A logical duality for underspecified probabilistic systems

This paper establishes a Stone-type duality between specifications and infLMPs. An infLMP is a probabilistic process whose transitions satisfy super-additivity instead of additivity. Interestingly, its simple structure can encode a mix of probabilistic and non-deterministic behavior, which, as we show, is strongly related to another well-known such model: probabilistic automata. Our duality puts in relation the category of infLMPs and a category of abstract representations of them based on properties only. We exhibit a Galois connection between these categories and show that we have an adjunct pair of functors when restricted to LMPs only. Our duality also shows that an infLMP can be considered as a demonic representative of a system’s information. Moreover, it carries forward a view where states are less important, and events, or properties, become the main characters, as it should be in probability theory. Along the way, we show that bisimulation and simulation are naturally interpreted in this setting, and we exhibit the interesting relationship between infLMPs and the usual probabilistic modal logics. This paper is an extended version of a Concur ’09 paper [13]; in particular, the comparison of infLMPs with probabilistic automata and the Galois connection are new.     

生成诊断公式的有限状态进程等价验证

分析有限状态进程互模拟等价判定技术,探讨了诊断公式的生成问题.给出了将有限状态进程转化为带标号的迁移系统,修改了Paige和Trajan求解最粗划分的算法,使其适用于带标号的迁移系统.给出生成Hennessy-Milner逻辑描述的诊断公式的算法,当两个进程不能互模拟时,产生两个诊断公式.算法的时间复杂度为O(m log n),空间复杂度为O(m+n).     

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

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

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.     

Priority as extremal probability

We extend the stratified model of probabilistic processes to obtain a very general notion ofprocess priority. The main idea is to allow probability guards of value 0 to be associated with alternatives of a probabilistic summation expression. Such alternatives can be chosen only if the non-zero alternatives are precluded by contextual constraints. We refer to this model as one of extremal probability and to its signature asPCCS . We providePCCS with a structural operational semantics and a notionof probabilistic bisimulation, which is shown to be a congruence. Of particular interest is the abstractionPCCS ofPCCS in which all non-zero probability guards are identified.PCCS represents a customized framework for reasoning about priority, and covers all features of process algebras proposed for reasoning about priority that we know of.A preliminary version of this paper appeared inProceedings of CONCUR '90 — First International Conference on Concurrency Theory, Vol. 458 of the Springer-Verlag seriesLecture Notes in Computer Science, pp. 456–466, Aug. 1990. The research of Scott Smolka was supported in part by NSF Grants CCR-9120995, CCR-9208585 and CCR-9505562; and AFOSR Grants F49620-93-1-0250, F49620-95-1-0508 and F49620-96-1-0087.     

Decision procedures and graph reductions for bisimulation equivalences part 1

In Process Algebra, processes are often specified in a framework of bisimulation semantics. The notion of bisimulation therefore plays an important role.

In this paper some existing and new decision methods are presented for strong bisimulation, τ-bisimulation and η-bisimulation. Each of these bisimulation equivalences corresponds to a certain abstraction mechanism.

In strong bisimulation, all events in a system are treated equally whereas τ-bisimulation takes into account the silent step τ; η-bisimulation was introduced recently for an alternative silent step η that is less abstract than τ. It is shown that the problem of η-bisimulation decision can be reduced to an abstract graph partitioning problem called the Product Relational Coarsest Partition problem. Special attention is paid to computational complexity of the decision methods.

As it turns out. finite process graphs can be reduced to unique minimal normalforms under all three bisimulation semantics mentioned.

The last section demonstrates how the decision methods can be used with a particular algebraic model to enable effective verification of specifications.     

概率模型检测技术在机器人路径规划中的应用

在机器人路径规划的实际应用中,针对机器人移动行为可能会受到外界环境影响的难题,提出了一种采用概率模型检测技术进行路径规划的新方法。首先,分析环境中的主要影响因素,将机器人的移动行为看作一个不确定事件,构建马尔可夫决策过程(MDP)模型。然后,采用概率计算树逻辑(PCTL)公式描述模型属性,表达机器人复杂多样的目标任务。最后,运用PRISM平台对模型进行分析和验证,得到满足属性的全局优化路径和定量数据。仿真结果表明,上述方法不仅能够保障机器人在障碍物环境中无碰撞移动,而且可以避开环境相对复杂的区域,保证机器人以最大概率完成任务。对比试验证明上述方法的正确性和有效性。     

A distributed algorithm for strong bisimulation reduction of state spaces

It is a known problem that state spaces can grow very large, which makes operating on them (including reducing them) difficult because of operational memory shortage. In an attempt to extend the size of the state spaces that can be dealt with, we designed and implemented a bisimulation reduction algorithm for distributed memory settings using message passing communication. By using message passing, the same implementation can be used on both clusters of workstations and large shared memory machines. The algorithm performs reduction of large labeled transition systems modulo strong bisimulation. We justify its correctness and termination and provide an evaluation of the worst-case time and message complexity and some performance data from a prototype implementation. Both theory and practice show that the algorithm scales up with the number of workstations.     

Computable processes and bisimulation equivalence

A process is calledcomputable if it can be modelled by a transition system that has a recursive structure—implying finite branching. The equivalence relation between transition systems considered is strong bisimulation equivalence. The transition systems studied in this paper can be associated to processes specified in common specification languages such as CCS, LOTOS, ACP and PSF. As a means for defining transition systems up to bisimulation equivalence, the specification languageCRL is used. Two simple fragments of,CRL are singled out, yielding universal expressivity with respect to recursive and primitive recursive transition systems. For both these domains the following properties are classified in the arithmetical hierarchy:bisimilarity, perpetuity (both ₁ ⁰ ),regularity (having a bisimilar, finite representation, ₂ ⁰ ),acyclic regularity ( ₁ ⁰ ), anddeadlock freedom (distinguishing deadlock from successful termination, ₁ ⁰ ). Finally, it is shown that in the domain of primitive recursive transition systems over a fixed, finite label set, a genuine hierarchy in bisimilarity can be defined by the complexity of the witnessing relations, which extends r.e. bisimilarity. Hence, primitive recursive transition systems already form an interesting class.     

Partial Order Reduction for Probabilistic Branching Time

In the past, partial order reduction has been used successfully to combat the state explosion problem in the context of model checking for non-probabilistic systems. For both linear time and branching time specifications, methods have been developed to apply partial order reduction in the context of model checking. Only recently, results were published that give criteria on applying partial order reduction for verifying quantitative linear time properties for probabilistic systems. This paper presents partial order reduction criteria for Markov decision processes and branching time properties, such as formulas of probabilistic computation tree logic. Moreover, we provide a comparison of the results established so far about reduction conditions for Markov decision processes.     

Safe reasoning with Logic LTS

Previous work has introduced the setting of Logic Labelled Transition Systems, called Logic LTS or LLTS for short, together with a variant of ready simulation as its fully-abstract refinement preorder, which allows one to compose operational specifications using a CSP-style parallel operator and the propositional connectives conjunction and disjunction.In this article, we show how a temporal logic for specifying safety properties may be embedded into LLTS so that (a) the temporal operators are compositional for ready simulation; (b) ready simulation, when restricted to pairs of processes and formulas, coincides with the logic’s satisfaction relation; (c) ready simulation, when restricted to formulas, is entailment.The utility of this setting as a semantic foundation for mixed operational and temporal-logic specification languages is demonstrated by means of a simple example. We also adopt the concept of may- and must-transitions from modal transition systems for notational convenience, and investigate the relation between modal refinement on modal transition systems and ready simulation on LLTS.     

On the specification of modal systems: A comparison of three frameworks

This paper studies the relationships between three notions of behavioural preorder that have been proposed in the literature: refinement over modal transition systems, and the covariant–contravariant simulation and the partial bisimulation preorders over labelled transition systems. It is shown that there are mutual translations between modal transition systems and labelled transition systems that preserve, and reflect, refinement and the covariant–contravariant simulation preorder. The translations are also shown to preserve the modal properties that can be expressed in the logics that characterize those preorders. A translation from labelled transition systems modulo the partial bisimulation preorder into the same model modulo the covariant–contravariant simulation preorder is also offered, together with some evidence that the former model is less expressive than the latter. In order to gain more insight into the relationships between modal transition systems modulo refinement and labelled transition systems modulo the covariant–contravariant simulation preorder, their connections are also phrased and studied in the context of institutions.     

Compositional reasoning for weighted Markov decision processes

Weighted Markov decision processes (MDPs) have long been used to model quantitative aspects of systems in the presence of uncertainty. However, much of the literature on such MDPs takes a monolithic approach, by modelling a system as a particular MDP; properties of the system are then inferred by analysis of that particular MDP. In contrast in this paper we develop compositional methods for reasoning about weighted MDPs, as a possible basis for compositional reasoning about their quantitative behaviour. In particular we approach these systems from a process algebraic point of view. For these we define a coinductive simulation-based behavioural preorder which is compositional in the sense that it is preserved by structural operators for constructing weighted MDPs from components.     

A logical foundation for the semantic Web

World Wide Web (WWW) has been one of important channels from which people acquire information and services, but most web pages are only used by humans at pre-sent, and these pages cannot be processed and understood automatically by computers. The semantic Web is an essential reformation of Web. The main objective of the seman-tic Web is to enrich Web with semantics and make Web be understood by computers, in order to communicate and cooperate between people and computer. The key of the se-…