Specification and analysis of distributed object-based stochastic hybrid systems. (English) Zbl 1178.68350
Hespanha, João (ed.) et al., Hybrid systems: Computation and control. 9th international workshop, HSCC 2006, Santa Barbara, CA, USA, March 29–31, 2006. Proceedings. Berlin: Springer (ISBN 3-540-33170-0/pbk). Lecture Notes in Computer Science 3927, 460-475 (2006).
Summary: In practice, many stochastic hybrid systems are not autonomous: they are objects that communicate with other objects by exchanging messages through an asynchronous medium such as a network. Issues such as: how to compositionally specify distributed object-based stochastic hybrid systems (OBSHS), how to formally model them, and how to verify their properties seem therefore quite important. This paper addresses these issues by: (i) defining a mathematical model for such systems that can be naturally regarded as a generalized stochastic hybrid system (GSHS) in the sense of [M. L. Bujorianu and J. Lygeros, “Toward a general theory of stochastic hybrid systems”, Lect. Notes Control Inf. Sci. 337, 3–30 (2006; Zbl 1130.93048)]; (ii) proposing a formal OBSHS specification language in which system transitions are specified in a modular way by probabilistic rewrite rules; and (iii) showing how these systems can be subjected to statistical model checking analysis to verify their probabilistic temporal logic properties.
For the entire collection see [Zbl 1103.68006].
For the entire collection see [Zbl 1103.68006].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 93C30 | Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) |
