@inbook{3f80ea649f804bd68b0b057536044ba9,
title = "A process-algebraic language for probabilistic I/O automata",
abstract = "We present a process-algebraic language for Probabilistic I/O Automata (PIOA). To ensure that PIOA specifications given in our language satisfy the {"}input-enabled{"} property, which requires that all input actions be enabled in every state of a PIOA, we augment the language with a set of type inference rules. We also equip our language with a formal operational semantics defined by a set of transition rules. We present a number of results whose thrust is to establish that the typing and transition rules are sensible and interact properly. The central connection between types and transition systems is that if a term is well-typed, then in fact the associated transition system is input-enabled. We also consider two notions of equivalence for our language, weighted bisimulation equivalence and PIOA behavioral equivalence. We show that both equivalences are substitutive with respect to the operators of the language, and note that weighted bisimulation equivalence is a strict refinement of behavioral equivalence.",
keywords = "Continuous-time Markov chains, Process equivalences, Stochastic process algebras, Typing systems and algorithms",
author = "Stark, \{Eugene W.\} and Rance Cleaveland and Smolka, \{Scott A.\}",
year = "2003",
doi = "10.1007/978-3-540-45187-7\_13",
language = "English",
isbn = "3540407537",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "193--207",
editor = "Roberto Amadio and Denis Lugiez",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
}