Branching bisimulation congruence for probabilistic systems

A notion of branching bisimilarity for the alternating model of probabilistic systems, compatible with parallel composition, is defined. For a congruence result, an internal transition immediately followed by a non-trivial probability distribution is not considered inert. A weaker definition of branching bisimilarity for the same model has been given earlier. Here we show that our branching bisimulation is the coarsest congruence for parallel composition that is included in the weaker version. To support the use of the present equivalence as a reduction technique, we also show that probabilistic CTL formulae are preserved by our equivalence, and we provide a polynomial-time algorithm deciding branching bisimilarity.     

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 Congruence for Probabilistic Systems

The notion of branching bisimulation for the alternating model of probabilistic systems is not a congruence with respect to parallel composition. In this paper we first define another branching bisimulation in the more general model allowing consecutive probabilistic transitions, and we prove that it is compatible with parallel composition. We then show that our bisimulation is actually the coarsest congruence relation included in the existing branching bisimulation when restricted to the alternating model.     

State estimation and detectability of probabilistic discrete event systems

A probabilistic discrete event system (PDES) is a nondeterministic discrete event system where the probabilities of nondeterministic transitions are specified. State estimation problems of PDES are more difficult than those of non-probabilistic discrete event systems. In our previous papers, we investigated state estimation problems for non-probabilistic discrete event systems. We defined four types of detectabilities and derived necessary and sufficient conditions for checking these detectabilities. In this paper, we extend our study to state estimation problems for PDES by considering the probabilities. The first step in our approach is to convert a given PDES into a nondeterministic discrete event system and find sufficient conditions for checking probabilistic detectabilities. Next, to find necessary and sufficient conditions for checking probabilistic detectabilities, we investigate the “convergence” of event sequences in PDES. An event sequence is convergent if along this sequence, it is more and more certain that the system is in a particular state. We derive conditions for convergence and hence for detectabilities. We focus on systems with complete event observation and no state observation. For better presentation, the theoretical development is illustrated by a simplified example of nephritis diagnosis.     

Polynomial-time probabilistic observability analysis of sampled-data piecewise affine systems

This paper proposes a polynomial-time probabilistic approach to solve the observability problem of sampled-data piecewise affine systems. First, an algebraic characterization for the system to be observable is derived. Next, based on the characterization, we propose a randomized algorithm that can determine if the system is observable in a probabilistic sense or the system is not observable in a deterministic sense. Finally, it is shown with some examples, for which it is hopeless to check the observability in a deterministic way, that the proposed algorithm is very useful.     

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.     

Using probabilistic model checking for dynamic power management

Dynamic power management (DPM) refers to the use of runtime strategies in order to achieve a tradeoff between the performance and power consumption of a system and its components. We present an approach to analysing stochastic DPM strategies using probabilistic model checking as the formal framework. This is a novel application of probabilistic model checking to the area of system design. This approach allows us to obtain performance measures of strategies by automated analytical means without expensive simulations. Moreover, one can formally establish various probabilistically quantified properties pertaining to buffer sizes, delays, energy usage etc., for each derived strategy.Received November 2003Revised September 2004Accepted December 2004 by M. Leuschel and D. J. Cooke     

Cones and foci: A mechanical framework for protocol verification

We define a cones and foci proof method, which rephrases the question whether two system specifications are branching bisimilar in terms of proof obligations on relations between data objects. Compared to the original cones and foci method from Groote and Springintveld, our method is more generally applicable, because it does not require a preprocessing step to eliminate τ-loops. We prove soundness of our approach and present a set of rules to prove the reachability of focus points. Our method has been formalized and proved correct using PVS. Thus we have established a framework for mechanical protocol verification. We apply this framework to the Concurrent Alternating Bit Protocol.

---

     

On control of discrete-time state-dependent jump linear systems with probabilistic constraints: A receding horizon approach

In this article, we consider a receding horizon control of discrete-time state-dependent jump linear systems, a particular kind of stochastic switching systems, subject to possibly unbounded random disturbances and probabilistic state constraints. Due to the nature of the dynamical system and the constraints, we consider a one-step receding horizon. Using inverse cumulative distribution function, we convert the probabilistic state constraints to deterministic constraints, and obtain a tractable deterministic receding horizon control problem. We consider the receding horizon control law to have a linear state-feedback and an admissible offset term. We ensure mean square boundedness of the state variable via solving linear matrix inequalities off-line, and solve the receding horizon control problem on-line with control offset terms. We illustrate the overall approach applied on a macroeconomic system.     

Robust Kalman filtering for uncertain discrete-time systems with probabilistic parameters bounded within a polytope

We consider the problem of finite horizon discrete-time Kalman filtering for systems with parametric uncertainties. Specifically, we consider unknown but deterministic uncertainties where the uncertain parameters are assumed to lie in a convex polyhedron with uniform probability density. The condition and a procedure for the construction of a suboptimal filter that minimizes an expected error covariance over-bound are derived.     

Parametric probabilistic transition systems for system design and analysis

We develop a model of parametric probabilistic transition Systems (PPTSs), where probabilities associated with transitions may be parameters. We show how to find instances of the parameters that satisfy a given property and instances that either maximize or minimize the probability of reaching a certain state. As an application, we model a probabilistic non-repudiation protocol with a PPTS. The theory we develop allows us to find instances that maximize the probability that the protocol ends in a fair state (no participant has an advantage over the others). A preliminary version of this paper was presented at SEFM’04 [LMT04]. 05 April 2006     

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.     

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.     

Approximating and computing behavioural distances in probabilistic transition systems

In an earlier paper we presented a pseudometric on the states of a probabilistic transition system, yielding a quantitative notion of behavioural equivalence. The behavioural pseudometric was defined via the terminal coalgebra of a functor based on a metric on Borel probability measures. In the present paper we give a polynomial-time algorithm, based on linear programming, to calculate the distances between states up to a prescribed degree of accuracy.     

Modeling and verifying probabilistic Multi-Agent Systems using knowledge and social commitments

Multi-Agent Systems (MASs) have long been modeled through knowledge and social commitments independently. In this paper, we present a new method that merges the two concepts to model and verify MASs in the presence of uncertainty. To express knowledge and social commitments simultaneously in uncertain settings, we define a new multi-modal logic called Probabilistic Computation Tree Logic of Knowledge and Commitments (PCTL^kc in short) which combines two existing probabilistic logics namely, probabilistic logic of knowledge PCTLK and probabilistic logic of commitments PCTLC. To model stochastic MASs, we present a new version of interpreted systems that captures the probabilistic behavior and accounts for the communication between interacting components. Then, we introduce a new probabilistic model checking procedure to check the compliance of target systems against some desirable properties written in PCTL^kc and report the obtained verification results. Our proposed model checking technique is reduction-based and consists in transforming the problem of model checking PCTL^kc into the problem of model checking a well established logic, namely PCTL. So doing provides us with the privilege of re-using the PRISM model checker to implement the proposed model checking approach. Finally, we demonstrate the effectiveness of our approach by presenting a real case study. This framework can be considered as a step forward towards closing the gap of capturing interactions between knowledge and social commitments in stochastic agent-based systems.     

Abstraction-based verification of codiagnosability for discrete event systems

In this paper, we investigate the verification of codiagnosability for discrete event systems (DES). That is, it is desired to ascertain if the occurrence of system faults can be detected based on the information of multiple local sites that partially observe the overall DES. As an improvement of existing codiagnosability tests that resort to the original DES with a potentially computationally infeasible state space, we propose a method that employs an abstracted system model on a smaller state space for the codiagnosability verification. Furthermore, we show that this abstraction can be computed without explicitly evaluating the state space of the original model in the practical case where the DES is composed of multiple subsystems.