2012
Reconciling real and stochastic time: the need for probabilistic refinement
Publication
Publication
Formal Aspects of Computing , Volume 24 p. 497- 518
We conservatively extend an ACP-style discrete-time process theory with
discrete stochastic delays. The semantics of the timed delays relies on time
additivity and time determinism, which are properties that enable us to merge
subsequent timed delays and to impose their synchronous expiration. Stochastic
delays, however, interact with respect to a so-called race condition that
determines the set of delays that expire first, which is guided by an
(implicit) probabilistic choice. The race condition precludes the property of
time additivity as the merger of stochastic delays alters this probabilistic
behavior. To this end, we resolve the race condition using
conditionally-distributed unit delays. We give a sound and ground-complete
axiomatization of the process theory comprising the standard set of ACP-style
operators. In this generalized setting, the alternative composition is no
longer associative, so we have to resort to special normal forms that
explicitly resolve the underlying race condition. Our treatment succeeds in
the initial challenge to conservatively extend standard time with stochastic
time. However, the `dissection' of the stochastic delays to
conditionally-distributed unit delays comes at a price, as we can no longer
relate the resolved race condition to the original stochastic delays. We seek
a solution in the field of probabilistic refinements that enable the
interchange of probabilistic and nondeterministic choices.
Additional Metadata | |
---|---|
, | |
Springer | |
Formal Aspects of Computing | |
Organisation | Directie |
Markovski, J., D'Argenio, P. R., Baeten, J., & de Vink, E. (2012). Reconciling real and stochastic time: the need for probabilistic refinement. Formal Aspects of Computing, 24, 497–518. |