Equivalence Computing On Stochastic Processes Algebra

Stochastic processes algebras (SPA) are concurrent system models with both functional specification and performance evaluation. It is a process algebra where action occurrences may be subject to a delay that is determined by a random variable. SPA may formally be used to specify the behavior as well as evaluate the performance of a system. A huge class of resource-sharing systems -such as large-scale computers, client-server architectures, networks -can accurately be described by using such stochastic specificationformalisms. Markovian process algebras are stochastic process algebras where delays are governed by exponential distributions, which have been widely used in the SPA. In this thesis, we investigate the operational semantics , notions of equivalence in stochastic process algebra , and the algorithms of computing equivalence for different types of Markovian process algebras. We focus on the following three topics:1. The bisimulations and proorders computing on Markovian chain algebra. In Markovian chain algebra, a process is delayed for an exponentially distributed time. Continuous time Markovian chain (CTMC) algebra is the earliest performance evaluation models of concurrency systems that are used . By analysing states transition of Markov chain, we can give the performance description of concurrency systems. On a CTMC algebra model, bisimulation equivalence is defined based on the translating rate between states, which is coincides with lumpability, an elementary notion for the aggregation of Markov chains, so we give a partition refinement algorithmic for equivalence classes which is action-based lumpability equivalence, and give the complexity analysing of our algorithms.2. The bisimulations and proorders computing on Interactive Markov chain (IMC) algebra. Interactive Markov chains , which combine classical process algebra models with continuous-time Markov chains orthogonally, are Stochastic processes algebras models. In this thesis, we investigate the algorithms of bisimu- lation equivalence computing on IMC. The main ideas of our algorithms are partition refinement sates of systems by using action and probability transitions, respectively, until the fixed-points of successively finer relations are reached. Based on the weak simulation definition of CTMC models, we give the strong (weak) simulation equivalence definition and computing algorithms for them on IMC. The center points of our algorithms are ,by resolving a liner equations system, removing all state pairs which have no simulation relation in systems.3. The bisimulations and proorders computing on general stochastic processes algebra (SPA). An general stochastic processes algebra contains action transitions of processes algebra and Markovian action transitions, which action is transitioned after a delay determined by an exponential distribution random variable. The main characterization of SPA is how to compute the resulting rateφ(λ,μ, P, Q) in case of synchronisation of Markovian action transitions. The SPA models differs from the definition ofφfunction . In this thesis, we investigate (bi)simulation equivalence the notations on SPA modes whereφ(λ,μ) =λμand gives the deciding algorithms for them. These deciding algorithms are modifying algorithms from those of IMCs, i.e. we have to separate time-convergent from time-divergent states, and decide bi(simullation) for every Markovian action transition .