STOCON is a Petri net based formalism for parallel system designs, covering both functional and stochastic behaviour.
There is a single, general, form of composition on nets. This combines the forms found in Process Algebras with those found in various existing Petri net composition schemes, to provide a composition structure which is richer than either. This composition is essentially parallel composition with interaction via both: transition synchronisation, as in a process algebra; place sharing which is the dual of transition synchronisation. These interactions are defined via a non-injective labelling of places and transitions.
Following the method of CCS, the behaviour of a composed net is derived by inference rules from the behaviour of its components. This is based on a model of behaviour which is similar to the labelled transition system (LTS) used in CCS, extended to accommodate the fact that interaction between parallel components is via both transitions and places rather than just the former. This supports the form of compositional reasoning found in CCS. Yet to be investigated is the question of the applicability to these nets of compositional reasoning using Petri net structural techniques such as place invariants.
The stochastic aspect is introduced by enhancing a transition with a delay specifier and a probabilistic choice over output places. A fundamental issue in formalisms for expressing time (e.g. timed and stochastic process algebras) is the form allowed for the delay specifiers. For a "timed formalism", oriented towards timing analysis of systems with hard real-time constraints, a delay specifier would be a constant time duration; whereas for a "stochastic formalism", oriented towards performance evaluation, a delay specifier would be a random distribution, often restricted to negative exponential. The kinds of temporal analysis applicable in these two cases are very different.
The approach taken in STOCON is to separate the two concerns of: compositionality - how a system can be constructed from components; temporality - what kinds of temporal analysis are applicable to the resulting systems. We thus allow arbitrary delay specifiers for individual transitions, and provide a general form of temporal composition in which the delay specifier for a transition which is a synchronisation of component transitions is a general expression on the delay specifiers for the components.
Another separation of concerns issue addressed is STOCON is separation between: time duration, probabilistic choice and non-deterministic choice. Fundamental to this separation is distinguishing between non-determinism and parallelism. In the usual interleaving semantics, parallel execution is (via the expansion law) absorbed into non-deterministic choice. In contrast, for STOCON, we retain in the LTS behavioural model information about parallelism which plays a fundamental role in the approach to temporal analysis.