FIG: Input/Output Stochastic Automata
In this section we briefly introduce Input/Output Stochastic Automata, then we introduce an example to show the IOSA model language. We finish the section explaning with more detail the particularities of this language.
Input/Output Stochastic Automata
Stochastic Automata (SA) is a model that supports sampling stochastic events from general distributions, i.e. arbitrary continuous random variables can be represented in a SA. These random variables are denoted clocks, and take positive values resulting from the sampling of their associated (continuous) distribution. As the system time advances the remaining time of the clocks decreases synchronously in equal proportion, viz. the value of all clocks decreases at the same rate. When the value of a clock becomes zero “the clock expires”, enabling the firing of events.
Formal definition of SA (see Definition 4 of [Budde17]) allows nondeterministic behaviour, which is problematic from the point of view of simulations. This issue is acknowledged by [DLM16], who derive a subset of SA closed under parallel composition called Input/Output Stochastic Automata. The result are fully probabilistic systems, viz. where nondeterminism has been ruled out in the resulting fully composed model.
In order to achieve this goal [DLM16], restrict the framework of SA and work with a partition of the actions set A, splitting them into input actions (A_I) and output actions (A_O ). Inputs synchronise with outputs, which respectively behave in a reactive and generative manner [VSS95]. This roughly means that the act of performing the transition (generating behaviour) is indicated by an output, whereas inputs listen and synchronise themselves with outputs (reacting to this behaviour).
Thus, output actions have an active role and are locally controlled. As a consequence their occurrence time is controlled by a random variable. Instead, input actions have a passive role and are externally controlled. Therefore their occurrence time can only depend on their interaction with outputs.
Example: tandem queue
To show the IOSA model syntax, we consider a tandem Jackson network consisting of two connected queues as depicted in the following figure:
Customers arrive at the first queue following a Poisson process with parameter λ. After being served by server 1 at rate μ1 they enter the second queue, where they are attended by server 2 at rate μ2. After this second service customers leave the system. Time lapses between events are exponentially distributed and independent between stations. That is, interarrival time is independent of the service times, and the time elapsing between two services in the first (resp. second) server is independent of the arrival times and of the service times in the second (resp. first) server.
1 const int c = 8; // Capacity of both queues . . . 14 module Arrivals 15 clk0: clock; // External arrivals ~ Exponential(lambda) 16 [P0!] @ clk0 > (clk0’= exponential(lambda)); 17 endmodule 18 19 module Queue1 20 q1: [0..c]; 21 clk1: clock; // Queue1 processing ~ Exponential(mu1) 22 // Packet arrival 23 [P0?] q1 == 0 > (q1’= q1+1) & (clk1’= exponential(mu1)); 24 [P0?] q1 > 0 & q1 (q1’= q1+1); 25 [P0?] q1 == c > ; 26 // Packet processing 27 [P1!] q1 == 1 @ clk1 > (q1’= q11); 28 [P1!] q1 > 1 @ clk1 > (q1’= q11) & (clk1’= exponential(mu1)); 29 endmodule . . . 43 properties 44 P( q2 > 0 U q2 == c ) //transient 45 S( q2 == c ) // steadystate 46 endproperties
Notice that the single edge of module Arrivals in line 16 is an output edge since its action label P0
is decorated with ‘!
’. Its boolean guard (between characters ‘]
’ and ‘@
’) is empty and thus equivalent to true. Moreover, this output edge is associated to the clock clk0
, which is mapped to an exponential probability density function of rate lambda.
The output action P0
from module Arrivals
synchronises with the input action P0
from module Queue1
, i.e. with any of the edges in lines 23–25. The boolean guards of those edges form a partition of the range of the integer variable q1
. Therefore, the output edge of module Arrivals is always enabled from a logical point of view, and will synchronise with exactly one of the input edges in lines 23–25. From a temporal point of view and by definition of IOSA, the output edge becomes enabled when clock clk0
expires.
Notice that the effects of an edge, i.e. the consequences of taking the edge which are described after the symbol >
, appear enclosed in parentheses and concatenated with the character &
. For instance the input edge in line 23 has two effects: incrementing by one the value of the integral variable q1
, and assigning a fresh random value to the clock variable clk1
, sampled from an exponentially distributed probability density function of rate mu1
.
Notice in particular the input edge in line 25. This edge has an empty effect, viz. a semicolon appears immediately following the symbol >
. This is interpreted as a NOP or SKIP , that is, the absence of an effect. Semantically that edge represents a packet trying to enter a fully occupied first queue, which is promptly discarded.
In the example, the property queries are included in the same file than the model description, and hence they appear enclosed in a properties... endproperties
environment. The property in line 44 is of transient type, and asks the probability of observing a saturated second queue before such queue empties. The property in line 45 is of steadystate type, and asks the time proportion that the second queue spends in a saturated state, viz. the long run probability of observing a saturation in the second queue.
The IOSA model language
IOSA model language is a modern modelling language which can represent processes in a continuous time setting where arbitrary distributions (i.e. not just the exponential) can be employed. Its constructs of syntax are very similar to those of PRISM, with the major addition of variables of type clock whose values must be sampled from stochastic distributions. An important difference w.r.t. PRIMS is that probabilistic branchings are not (yet) supported.
We next provide an exhaustive list of differences between the PRISM input language as used in out tool and the IOSA model syntax:
 at global scope only constants, properties, and modules can be defined;
 constants must be of either boolean, integral, or floating point type;

properties can be specified either in a dedicated file, or in the model file but enclosed in a
properties ... endproperties
environment; 
property queries are specified one per line and are either of type
 transient, following the formatP( !stop U rare )
, or
 rate (i.e. steadystate), following the formatS( rare )
,
wherestop
andrare
are booleanvalued expressions representing the stopping and rare event conditions respectively; 
variables can only appear within a module body, viz. enclosed in a
module ... endmodule
environment;  variables must be of either boolean, (ranged) integral, or clock type;
 each clock variable must be mapped to exactly one continuous probability function, and can only be assigned randomly chosen values, resulting from a sampling of such function;

nonempty labels in the edges of a module must be decorated either with
?
to signify that it is an input action (and thus an “input edge”), or with!
to signify that it is an output action (resp. “output edge”);  an empty label indicates a nonsynchronizing output edge;
 an empty boolean guard in an edge is interpreted as true ;

a semicolon immediately following symbol
>
is interpreted as NOP (Not OPeration); 
besides a boolean guard, output edges must declare one clock name between the character
@
and the symbol>
, which links that clock variable to the concrete output transitions represented by the edge.
IOSA models with commited actions
Suppose we want to model two components A and B where A, after a clock expires, sends a message to B and B instantaneously responses it with another output action. This situation cannot be modeled with IOSA model language because every output execution should follow a clock expiration. In order to deal with this limitation, IOSAC is introduced.
IOSAC extends Stochastic Automata by introducing the possibility of taking instantaneous actions, i.e. actions which do not depend on the expiration of clocks. These actions are called committed actions and are also splitted into input (??) and output (!!) actions with the intended meaning explained for noncommitted actions.
In this context, nondeterminism is also problem for simulations. Then, the same restrictions used over IOSA models will ensure that, almost surely, two noncommitted outputs are not enabled at the same time in a IOSAC model. In addition, for committed actions, an extra condition is required: if two committed action can be executed in a state, then these actions has to be confluent.
Following ideas from Milner [Milner89] we say that a IOSAC is confluent with respect to committed actions a and b if the occurrence of one of them does not prevent the other one from occurring in the future. More precisely, an IOSAC I is confluent with respect to (committed) actions a and b in A if for every state s in S we can complete the following diagram:
Note that we are asking to converge in a single state, which is somehow stronger than Milner’s strong confluence, where convergence takes place on bisimilar but potentially distinct states. A IOSAC model is confluent if it is confluent for all pair of commited action in the model.
The confluent condition is added because it ensures that confluent IOSAs are deterministic up to weak bisimulation. This condition can be checked by FIG automatically. See FIG documentation.
To use committed actions in a model, just decorate a label action with !!
or ??
instead of !
or ?
.
References:
 [Budde17]
 C.E. Budde. "Automation of Importance Splitting Techniques for Rare Event Simulation", PhD Thesis, Universidad Nacional de Córdoba, 2017.
 [DLM16]
 P.R. D’Argenio, M.D. Lee, and R.E. Monti. "Input/Output Stochastic Automata  Compositionality and Determinism". In FORMATS 2016, volume 9884 of LNCS, pages 53–68. Springer, Springer, 2016. DOI.
 [Milner89]
 R. Milner. “Communication and Concurrency”. PrenticeHall, Inc., 1989.
 [VSS95]
 R.J. van Glabbeek, S.A. Smolka, and B. Steffen. Reactive, generative, and stratified models of probabilistic processes. Information and Computation, 121(1):59 – 80, 1995. DOI.