On the Semantic Foundations of Probabilistic Synchronous Reactive Programs

Christel BaierChristel Baier, Edmund M. ClarkeEdmund M. Clarke, Vasiliki Hartonas-GarmhausenVasiliki Hartonas-Garmhausen

DOI Link

Christel Baier, Edmund M. Clarke, Vasiliki Hartonas-Garmhausen
On the Semantic Foundations of Probabilistic Synchronous Reactive Programs
Electron. Notes Theor. Comput. Sci., 22:3--28, 1999

Details
Bibtex

KurzfassungAbstract
In this paper we consider synchronous parallel programs that are composed by sequential randomized processes 1,…, k which communicate via shared variables. First, we give an operational semantics for the sequential components i on the basis of a transition relation defined in the classical SOS-style à la Plotkin [Plo81] which we use to specify the behaviour of by a Markov chain whose transitions stand for the cumulative effect of the activities of the components 1,…k within one time step. Second, we provide a denotational semantics for that also models by a Markov chain. It is based on a (denotational) least fixed point semantics for the sequential components which formalizes the input/output behaviour of the sequential components within one time step. While the operational (declarative) semantics might be the one that a designer (who provides the input for the tool) has in mind, the denotational (procedural) semantics is the one that a compiler might use. We establish a consistency result stating that the Markov chains induced by the operational and denotational semantics are bisimilar in the sense of [LS91].
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{BCH1999,
  author  = {Christel Baier and Edmund M. Clarke and Vasiliki
             Hartonas-Garmhausen},
  title   = {On the Semantic Foundations of Probabilistic Synchronous Reactive
             Programs},
  journal = {Electron. Notes Theor. Comput. Sci.},
  volume  = {22},
  year    = {1999},
  pages   = {3--28},
  doi     = {10.1016/S1571-0661(05)80594-8}
}