## 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.

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.

Original language | English |
---|---|

Title of host publication | Stochastic Model Checking |

Subtitle of host publication | Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems |

Editors | Anne Remke, Mariëlle Stoelinga |

Publisher | Springer |

Pages | 67-86 |

ISBN (Electronic) | 978-3-662-45489-3 |

ISBN (Print) | 978-3-662-45488-6 |

DOIs | |

Publication status | Published - 2014 |

Externally published | Yes |

Event | International Autumn School, ROCKS 2012 - Vahrn, Italy Duration: 22 Oct 2012 → 26 Oct 2012 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Number | 8453 |

### Other

Other | International Autumn School, ROCKS 2012 |
---|---|

Country/Territory | Italy |

City | Vahrn |

Period | 22/10/12 → 26/10/12 |