Detail publikace

Precise Parameter Synthesis for Stochastic Petri Nets with Interval Rate Parameters

ČEŠKA, M. ČEŠKA, M. PAOLETTI, N.

Originální název

Precise Parameter Synthesis for Stochastic Petri Nets with Interval Rate Parameters

Anglický název

Precise Parameter Synthesis for Stochastic Petri Nets with Interval Rate Parameters

Jazyk

en

Originální abstrakt

We consider the problem of synthesising parameters affecting transition rates and probabilities in generalised Stochastic Petri Nets (GSPNs). Given a time-bounded property expressed as a probabilisitic temporal logic formula, our method allows computing the parameters values for which the probability of satisfying the property meets a given bound, or is optimised. We develop algorithms based on reducing the parameter synthesis problem for GSPNs to the corresponding problem for continuous-time Markov Chains (CTMCs), for which we can leverage existing synthesis algorithms, while retaining the modelling capabilities and expressive power of GSPNs. We evaluate the usefulness of our approach by synthesising parameters for two case studies.

Anglický abstrakt

We consider the problem of synthesising parameters affecting transition rates and probabilities in generalised Stochastic Petri Nets (GSPNs). Given a time-bounded property expressed as a probabilisitic temporal logic formula, our method allows computing the parameters values for which the probability of satisfying the property meets a given bound, or is optimised. We develop algorithms based on reducing the parameter synthesis problem for GSPNs to the corresponding problem for continuous-time Markov Chains (CTMCs), for which we can leverage existing synthesis algorithms, while retaining the modelling capabilities and expressive power of GSPNs. We evaluate the usefulness of our approach by synthesising parameters for two case studies.

Dokumenty

BibTex


@inproceedings{BUT146256,
  author="Milan {Češka} and Milan {Češka} and Nicola {Paoletti}",
  title="Precise Parameter Synthesis for Stochastic Petri Nets with Interval Rate Parameters",
  annote="We consider the problem of synthesising parameters affecting transition rates and
probabilities in generalised Stochastic Petri Nets (GSPNs). Given a time-bounded
property expressed as a probabilisitic temporal logic formula, our method allows
computing the parameters values for which the probability of satisfying the
property meets a given bound, or is optimised. We develop algorithms based on
reducing the parameter synthesis problem for GSPNs to the corresponding problem
for continuous-time Markov Chains (CTMCs), for which we can leverage existing
synthesis algorithms, while retaining the modelling capabilities and expressive
power of GSPNs. We evaluate the usefulness of our approach by synthesising
parameters for two case studies.",
  address="Springer Verlag",
  booktitle="Proceedings of 16th International Conference on Computer Aided Systems Theory",
  chapter="146256",
  doi="10.1007/978-3-319-74727-9_5",
  edition="LNCS volume 10672",
  howpublished="print",
  institution="Springer Verlag",
  year="2017",
  month="february",
  pages="38--46",
  publisher="Springer Verlag",
  type="conference paper"
}