Title: Abstract executions of stochastic discrete event systems

Authors: Michel Batteux; Tatiana Prosvirnova; Antoine B. Rauzy

Addresses: IRT SystemX, 2 Boulevard Thomas Gobert, 91120 Palaiseau, France ' ONERA/DTIS, Université de Toulouse, F-31055 Toulouse, France ' Norwegian University of Science and Technology, Department of Mechanical and Industrial Engineering, Richard Birkelands vei 2B (Office P307), 7491 Trondheim, Norway

Abstract: 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.

Keywords: stochastic discrete event systems; timed and hybrid automata; abstract intepretation; AltaRica 3.0.

DOI: 10.1504/IJCCBS.2022.121363

International Journal of Critical Computer-Based Systems, 2022 Vol.10 No.3, pp.202 - 226

Received: 04 Mar 2021
Accepted: 06 Jun 2021
Published online: 07 Mar 2022 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article