Input/Output Stochastic Automata with Urgency: Confluence and weak determinism

TL;DR

This paper extends input/output stochastic automata with urgency, increasing modularity but introducing non-determinism, and shows conditions under which models remain weakly deterministic despite non-confluence.

Contribution

It introduces urgent actions into IOSA, enhancing compositional modeling, and establishes conditions for confluence and weak determinism in these extended models.

Findings

Confluent models are weakly deterministic despite non-determinism.

Sufficient conditions for confluence in networks of IOSAs.

Extension improves modularity and compositionality.

Abstract

In a previous work, we introduced an input/output variant of stochastic automata (IOSA) that, once the model is closed (i.e., all synchronizations are resolved), the resulting automaton is fully stochastic, that is, it does not contain non-deterministic choices. However, such variant is not sufficiently versatile for compositional modelling. In this article, we extend IOSA with urgent actions. This extension greatly increases the modularization of the models, allowing to take better advantage on compositionality than its predecessor. However, this extension introduces non-determinism even in closed models. We first show that confluent models are weakly deterministic in the sense that, regardless the resolution of the non-determinism, the stochastic behaviour is the same. In addition, we provide sufficient conditions to ensure that a network of interacting IOSAs is confluent without the need to obtain the composed IOSA.