Abstract executions of stochastic discrete event systems

Stochastic discrete event systems play a steadily increasing role in reliability engineering and beyond in systems engineering. Designing stochastic discrete event systems presents however well-known difficulties: models are hard to debug and to validate because of the existence of infinitely many possible executions, itself due to stochastic delays, which are possibly intertwined with deterministic ones. In this article, revisiting ideas introduced in the framework of model-checking of timed and hybrid systems, we show that it is possible to abstract the time in stochastic discrete event systems. More specifically, we show that schedules of transitions can be abstracted into systems of linear inequalities and that abstract and concrete executions are bisimilar. The result presented in this article represents thus a very important step forward in quality assurance of stochastic models of complex technical systems. We illustrate the potential of the proposed approach by means of AltaRica 3.0 models.