Input/Output Stochastic Automata with Urgency: Confluence and weak determinism
Pedro R. D'Argenio, Ra\'ul E. Monti

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Distributed systems and fault tolerance
