The description of complex systems involving physical or biological components usually requires to model complex continuous behavior induced by variables such as time, distance, speed, temperature, alkalinity of a solution, etc. Often, such variables can be quantified probabilistically to better understand the behavior of the complex systems. For example, the arrival time of events may be considered a Poisson process or the weight of an individual may be assumed to be distributed according to a log-normal distribution. However, it is also common that the uncertainty on how these variables behave makes us prefer to leave out the choice of a particular probability and rather model it as a purely non-deterministic decision, as it is the case when a system is intended to be deployed in a variety of very different computer or network architectures. Therefore, the semantics of these systems needs to be represented by a variant of probabilistic automata that involves continuous domains on the state space and the transition relation. In this paper, we provide a survey on the theory of such kind of models. We present the theory of the so-called labeled Markov processes (LMP) and its extension with internal non-determinism (NLMP).We show that in these complex domains, the bisimulation relation can be understood in different manners.We show the relation between the different bisimulations and try to understand their expressiveness through examples. We also study variants of Hennessy-Milner logic that provides logical characterizations of some of these bisimulations.

A Theory for the Semantics of Stochastic and Non-deterministic Continuous Systems / Budde, Carlos E.; D'Argenio, Pedro R.; P., Sanchez Terraf; N., Wolovick. - ELETTRONICO. - 8453:(2014), pp. 67-86. (Intervento presentato al convegno International Autumn School on Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems, ROCKS 2012 tenutosi a Vahrn, Italy nel October 22-26, 2012) [10.1007/978-3-662-45489-3_3].

A Theory for the Semantics of Stochastic and Non-deterministic Continuous Systems

Carlos E. Budde;
2014-01-01

Abstract

The description of complex systems involving physical or biological components usually requires to model complex continuous behavior induced by variables such as time, distance, speed, temperature, alkalinity of a solution, etc. Often, such variables can be quantified probabilistically to better understand the behavior of the complex systems. For example, the arrival time of events may be considered a Poisson process or the weight of an individual may be assumed to be distributed according to a log-normal distribution. However, it is also common that the uncertainty on how these variables behave makes us prefer to leave out the choice of a particular probability and rather model it as a purely non-deterministic decision, as it is the case when a system is intended to be deployed in a variety of very different computer or network architectures. Therefore, the semantics of these systems needs to be represented by a variant of probabilistic automata that involves continuous domains on the state space and the transition relation. In this paper, we provide a survey on the theory of such kind of models. We present the theory of the so-called labeled Markov processes (LMP) and its extension with internal non-determinism (NLMP).We show that in these complex domains, the bisimulation relation can be understood in different manners.We show the relation between the different bisimulations and try to understand their expressiveness through examples. We also study variants of Hennessy-Milner logic that provides logical characterizations of some of these bisimulations.
2014
Proceedings of the International Autumn School on Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems, ROCKS 2012
Germany
Springer-Verlag Berlin Heidelberg
978-3-662-45488-6
978-3-662-45489-3
Budde, Carlos E.; D'Argenio, Pedro R.; P., Sanchez Terraf; N., Wolovick
A Theory for the Semantics of Stochastic and Non-deterministic Continuous Systems / Budde, Carlos E.; D'Argenio, Pedro R.; P., Sanchez Terraf; N., Wolovick. - ELETTRONICO. - 8453:(2014), pp. 67-86. (Intervento presentato al convegno International Autumn School on Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems, ROCKS 2012 tenutosi a Vahrn, Italy nel October 22-26, 2012) [10.1007/978-3-662-45489-3_3].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/314689
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact