The Markovian behavioral equivalences defined so far treat exponentially timed internal actions like any other action. Since an exponentially timed internal action has a nonzero duration, it can be observed whenever it is executed between a pair of exponentially timed noninternal actions. However, no difference may be noted at steady state between a sequence of exponentially timed internal actions and a single exponentially timed internal action as long as their average durations coincide. We show that Milner’s construction to derive a weak bisimulation congruence for nondeterministic processes can be extended to sequential Markovian processes in a way that captures the above situation. The resulting weak Markovian bisimulation congruence admits a sound and complete axiomatization, induces an exact CTMC-level aggregation at steady state, and is decidable in polynomial time for finite-state processes having no cycles of exponentially timed internal actions.

Weak Markovian Bisimulation Congruences and Exact CTMC-Level Aggregations for Sequential Processes

Bernardo, Marco
2011

Abstract

The Markovian behavioral equivalences defined so far treat exponentially timed internal actions like any other action. Since an exponentially timed internal action has a nonzero duration, it can be observed whenever it is executed between a pair of exponentially timed noninternal actions. However, no difference may be noted at steady state between a sequence of exponentially timed internal actions and a single exponentially timed internal action as long as their average durations coincide. We show that Milner’s construction to derive a weak bisimulation congruence for nondeterministic processes can be extended to sequential Markovian processes in a way that captures the above situation. The resulting weak Markovian bisimulation congruence admits a sound and complete axiomatization, induces an exact CTMC-level aggregation at steady state, and is decidable in polynomial time for finite-state processes having no cycles of exponentially timed internal actions.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11576/2515696
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? ND
social impact