On the Robustness of Temporal Properties for Stochastic Models
Stochastic models such as Continuous-Time Markov Chains (CTMC) and Stochastic Hybrid Automata (SHA) are powerful formalisms to model and to reason about the dynamics of biological systems, due to their ability to capture the stochasticity inherent in biological processes. A classical question in for...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2013-08-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1309.0866v1 |
| _version_ | 1819211344710205440 |
|---|---|
| author | Ezio Bartocci Luca Bortolussi Laura Nenzi Guido Sanguinetti |
| author_facet | Ezio Bartocci Luca Bortolussi Laura Nenzi Guido Sanguinetti |
| author_sort | Ezio Bartocci |
| collection | DOAJ |
| description | Stochastic models such as Continuous-Time Markov Chains (CTMC) and Stochastic Hybrid Automata (SHA) are powerful formalisms to model and to reason about the dynamics of biological systems, due to their ability to capture the stochasticity inherent in biological processes. A classical question in formal modelling with clear relevance to biological modelling is the model checking problem. i.e. calculate the probability that a behaviour, expressed for instance in terms of a certain temporal logic formula, may occur in a given stochastic process. However, one may not only be interested in the notion of satisfiability, but also in the capacity of a system to mantain a particular emergent behaviour unaffected by the perturbations, caused e.g. from extrinsic noise, or by possible small changes in the model parameters. To address this issue, researchers from the verification community have recently proposed several notions of robustness for temporal logic providing suitable definitions of distance between a trajectory of a (deterministic) dynamical system and the boundaries of the set of trajectories satisfying the property of interest. The contributions of this paper are twofold. First, we extend the notion of robustness to stochastic systems, showing that this naturally leads to a distribution of robustness scores. By discussing two examples, we show how to approximate the distribution of the robustness score and its key indicators: the average robustness and the conditional average robustness. Secondly, we show how to combine these indicators with the satisfaction probability to address the system design problem, where the goal is to optimize some control parameters of a stochastic model in order to best maximize robustness of the desired specifications. |
| first_indexed | 2024-12-23T06:25:35Z |
| format | Article |
| id | doaj.art-690836aefe1d4595855e977f9027dc21 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-23T06:25:35Z |
| publishDate | 2013-08-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-690836aefe1d4595855e977f9027dc212022-12-21T17:57:05ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802013-08-01125Proc. HSB 201331910.4204/EPTCS.125.1On the Robustness of Temporal Properties for Stochastic ModelsEzio BartocciLuca BortolussiLaura NenziGuido SanguinettiStochastic models such as Continuous-Time Markov Chains (CTMC) and Stochastic Hybrid Automata (SHA) are powerful formalisms to model and to reason about the dynamics of biological systems, due to their ability to capture the stochasticity inherent in biological processes. A classical question in formal modelling with clear relevance to biological modelling is the model checking problem. i.e. calculate the probability that a behaviour, expressed for instance in terms of a certain temporal logic formula, may occur in a given stochastic process. However, one may not only be interested in the notion of satisfiability, but also in the capacity of a system to mantain a particular emergent behaviour unaffected by the perturbations, caused e.g. from extrinsic noise, or by possible small changes in the model parameters. To address this issue, researchers from the verification community have recently proposed several notions of robustness for temporal logic providing suitable definitions of distance between a trajectory of a (deterministic) dynamical system and the boundaries of the set of trajectories satisfying the property of interest. The contributions of this paper are twofold. First, we extend the notion of robustness to stochastic systems, showing that this naturally leads to a distribution of robustness scores. By discussing two examples, we show how to approximate the distribution of the robustness score and its key indicators: the average robustness and the conditional average robustness. Secondly, we show how to combine these indicators with the satisfaction probability to address the system design problem, where the goal is to optimize some control parameters of a stochastic model in order to best maximize robustness of the desired specifications.http://arxiv.org/pdf/1309.0866v1 |
| spellingShingle | Ezio Bartocci Luca Bortolussi Laura Nenzi Guido Sanguinetti On the Robustness of Temporal Properties for Stochastic Models Electronic Proceedings in Theoretical Computer Science |
| title | On the Robustness of Temporal Properties for Stochastic Models |
| title_full | On the Robustness of Temporal Properties for Stochastic Models |
| title_fullStr | On the Robustness of Temporal Properties for Stochastic Models |
| title_full_unstemmed | On the Robustness of Temporal Properties for Stochastic Models |
| title_short | On the Robustness of Temporal Properties for Stochastic Models |
| title_sort | on the robustness of temporal properties for stochastic models |
| url | http://arxiv.org/pdf/1309.0866v1 |
| work_keys_str_mv | AT eziobartocci ontherobustnessoftemporalpropertiesforstochasticmodels AT lucabortolussi ontherobustnessoftemporalpropertiesforstochasticmodels AT lauranenzi ontherobustnessoftemporalpropertiesforstochasticmodels AT guidosanguinetti ontherobustnessoftemporalpropertiesforstochasticmodels |