On-the-fly verification of discrete event simulations by means of simulation purposes: Extended version

Abstract

Discrete event simulations can be used to analyze natural and artificial phenomena. To this end, one provides models whose behaviors are characterized by discrete events in a discrete timeline. By running such a simulation, one can then observe its properties. This suggests the possibility of applying on-the-fly verification procedures during simulations. In this work we propose a method by which this can be accomplished. It consists of modeling the simulation as a transition system (implicitly), and the property to be verified as another transition system (explicitly). The latter we call a simulation purpose and it is used both to verify the success of the property and to guide the simulation. Algorithmically, this corresponds to building a synchronous product of these two transitions systems on-the-fly and using it to operate a simulator. By the end of such an algorithm, it may deliver either a conclusive or inconclusive verdict. If conclusive, it becomes known whether the simulation model satisfies the simulation purpose. If inconclusive, it is possible to adjust certain parameters and try again. The precise nature of simulation purposes, as well as the corresponding satisfiability relations and verification algorithms, are largely determined by methodological considerations important for the analysis of simulations, whose computational characteristics we compare with empirical scientific procedures. We provide a number of ways in which such a satisfiability relation can be defined formally, the related algorithms, and mathematical proofs of soundness, completeness and complexities. Two application examples are given to illustrate the approach.