Randomized formal systems for specifying discrete stochastic models

This paper presents a method, based on the mathematical concept of formal systems, for writing high-level specifications of discrete stochastic models. This method is completely formal, suitable for information processing by computer and generally applicable. Moreover, it unifies analytic and statistical techniques. Concepts and notions are developed informally by means of four examples from the field of Petri nets and queueing systems. Processing algorithms (generating state-transition graphs, computing Markovian transition probabilities and simulating the specified models) are outlined. Basically, this method yields a “constructive” approach to discrete stochastic modelling.