Discrete time generative-reactive probabilistic processes with different advancing speeds (Q1853593)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Discrete time generative-reactive probabilistic processes with different advancing speeds
scientific article

    Statements

    Discrete time generative-reactive probabilistic processes with different advancing speeds (English)
    0 references
    0 references
    0 references
    21 January 2003
    0 references
    We present a process algebra expressing probabilistic external/internal choices, multi-way synchronizations, and processes with different advancing speeds in the context of discrete time, i.e. where time is not continuous but is represented by a sequence of discrete steps as in Discrete Time Markov Chains (DTMCs). To this end, we introduce a variant of CSP that employs a probabilistic asynchronous parallel operator whose synchronization mechanism is based on a mixture of the classical generative and reactive models of probability. In particular, differently from existing discrete time process algebras, where parallel processes are executed in synchronous locksteps, the parallel operator that we adopt allows processes with different probabilistic advancing speeds (mean number of actions executed per time unit) to be modeled. Moreover, our generative-reactive synchronization mechanism makes it possible to always derive DTMCs in the case of fully specified systems. We then present a sound and complete axiomatization of probabilistic bisimulation over finite processes of our calculus, that is a smooth extension of the axiom system for a standard process algebra, thus solving the open problem of cleanly axiomatizing action restriction in the generative model. As a further result, we show that, when evaluating steady state based performance measures which are expressible by attaching rewards to actions, our approach provides an exact solution even if the advancing speeds are considered not to be probabilistic, without incurring the state space explosion problem that arises with standard synchronous approaches. We finally present a case study on multi-path routing showing the expressiveness of our calculus and that it makes it particularly easy to produce scalable specifications.
    0 references
    0 references
    process algebra
    0 references
    discrete time Markov chain
    0 references
    performance evaluation
    0 references
    probabilistic models
    0 references