Testing equivalence for processes featuring both nondeterminism and probabilities is not insensitive to the moment of occurrence of nondeterministic or probabilistic choices among identical actions. Therefore, it is only partially backward compatible with testing equivalences for fully nondeterministic processes and for fully probabilistic processes. We illustrate how its backward compatibility can be extended through the joint use of coherent resolutions of nondeterminism and additional decorations for transitions, to ensure the insensitivity to the aforementioned internal choices. We also show that full backward compatibility cannot be achieved by exhibiting a counterexample with external choices too, inspired by failure semantics for fully nondeterministic processes.
Extending Backward Compatibility of Probabilistic Testing via Coherent Resolutions
Bernardo, Marco
2020
Abstract
Testing equivalence for processes featuring both nondeterminism and probabilities is not insensitive to the moment of occurrence of nondeterministic or probabilistic choices among identical actions. Therefore, it is only partially backward compatible with testing equivalences for fully nondeterministic processes and for fully probabilistic processes. We illustrate how its backward compatibility can be extended through the joint use of coherent resolutions of nondeterminism and additional decorations for transitions, to ensure the insensitivity to the aforementioned internal choices. We also show that full backward compatibility cannot be achieved by exhibiting a counterexample with external choices too, inspired by failure semantics for fully nondeterministic processes.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
