DiPS : A Tool for Data-Informed Parameter Synthesis for Markov Chains from Multiple-Property Specifications

Hajnal, Matej; Šafránek, David; Petrov, Tatjana

DiPS : A Tool for Data-Informed Parameter Synthesis for Markov Chains from Multiple-Property Specifications

Dateien

Zu diesem Dokument gibt es keine Dateien.

Datum

2021

Autor:innen

Hajnal, Matej

Šafránek, David

Petrov, Tatjana

DOI (zitierfähiger Link)

https://doi.org/10.1007/978-3-030-91825-5_5

Sammlungen

Informatik und Informationswissenschaft
Exzellenzcluster "Centre for the Advanced Study of Collective Behaviour"

Publikationstyp

Beitrag zu einem Konferenzband

Publikationsstatus

Published

Erschienen in

BALLARINI, Paolo, ed., Hind CASTEL, ed., Ioannis DIMITRIOU, ed. and others. Performance Engineering and Stochastic Modeling : 17th European Workshop, EPEW 2021, and 26th International Conference, ASMTA 2021, Virtual Event, December 9–10 and December 13–14, 2021, Proceedings. Cham: Springer, 2021, pp. 79-95. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-030-91824-8. Available under: doi: 10.1007/978-3-030-91825-5_5

Zusammenfassung

We present a tool for inferring the parameters of a Discrete-time Markov chain (DTMC) with respect to properties written in probabilistic temporal logic (PCTL) informed by data observations. The tool combines, in a modular and user-friendly way, the existing methods and tools for parameter synthesis of DTMCs. On top of this, the tool implements several hybrid methods for the exploration of the parameter space based on utilising the intermediate results of parametric model checking – the symbolic representation of properties’ satisfaction in the form of rational functions. These methods are combined to support three different parameter exploration methods: (i) optimisation, (ii) parameter synthesis, (iii) Bayesian parameter inference. Each of the available methods makes a different trade-off between scalability and inference quality, which can be chosen by the user depending on the application context. In this paper, we present the implementation, the main features of the tool, and we evaluate its performance on several benchmarks.

Fachgebiet (DDC)

004 Informatik

Konferenz

EPEW: European Workshop on Performance Engineering; ASMTA: International Conference on Analytical and Stochastic Modeling Techniques and Applications, 9. Dez. 2021 - 14. Dez. 2021, virtual event

Zitieren

ISO 690

HAJNAL, Matej, David ŠAFRÁNEK, Tatjana PETROV, 2021. DiPS : A Tool for Data-Informed Parameter Synthesis for Markov Chains from Multiple-Property Specifications. EPEW: European Workshop on Performance Engineering; ASMTA: International Conference on Analytical and Stochastic Modeling Techniques and Applications. virtual event, 9. Dez. 2021 - 14. Dez. 2021. In: BALLARINI, Paolo, ed., Hind CASTEL, ed., Ioannis DIMITRIOU, ed. and others. Performance Engineering and Stochastic Modeling : 17th European Workshop, EPEW 2021, and 26th International Conference, ASMTA 2021, Virtual Event, December 9–10 and December 13–14, 2021, Proceedings. Cham: Springer, 2021, pp. 79-95. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-030-91824-8. Available under: doi: 10.1007/978-3-030-91825-5_5

BibTex

@inproceedings{Hajnal2021DataI-56906,
  year={2021},
  doi={10.1007/978-3-030-91825-5_5},
  title={DiPS : A Tool for Data-Informed Parameter Synthesis for Markov Chains from Multiple-Property Specifications},
  number={13104},
  isbn={978-3-030-91824-8},
  issn={0302-9743},
  publisher={Springer},
  address={Cham},
  series={Lecture Notes in Computer Science},
  booktitle={Performance Engineering and Stochastic Modeling : 17th European Workshop, EPEW 2021, and 26th International Conference, ASMTA 2021, Virtual Event, December 9–10 and December 13–14, 2021, Proceedings},
  pages={79--95},
  editor={Ballarini, Paolo and Castel, Hind and Dimitriou, Ioannis},
  author={Hajnal, Matej and Šafránek, David and Petrov, Tatjana}
}

RDF

<rdf:RDF
    xmlns:dcterms="http://purl.org/dc/terms/"
    xmlns:dc="http://purl.org/dc/elements/1.1/"
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:bibo="http://purl.org/ontology/bibo/"
    xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
    xmlns:foaf="http://xmlns.com/foaf/0.1/"
    xmlns:void="http://rdfs.org/ns/void#"
    xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > 
  <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/56906">
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:contributor>Šafránek, David</dc:contributor>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/56906"/>
    <dcterms:title>DiPS : A Tool for Data-Informed Parameter Synthesis for Markov Chains from Multiple-Property Specifications</dcterms:title>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2022-03-17T11:23:26Z</dcterms:available>
    <dc:rights>terms-of-use</dc:rights>
    <dcterms:abstract xml:lang="eng">We present a tool for inferring the parameters of a Discrete-time Markov chain (DTMC) with respect to properties written in probabilistic temporal logic (PCTL) informed by data observations. The tool combines, in a modular and user-friendly way, the existing methods and tools for parameter synthesis of DTMCs. On top of this, the tool implements several hybrid methods for the exploration of the parameter space based on utilising the intermediate results of parametric model checking – the symbolic representation of properties’ satisfaction in the form of rational functions. These methods are combined to support three different parameter exploration methods: (i) optimisation, (ii) parameter synthesis, (iii) Bayesian parameter inference. Each of the available methods makes a different trade-off between scalability and inference quality, which can be chosen by the user depending on the application context. In this paper, we present the implementation, the main features of the tool, and we evaluate its performance on several benchmarks.</dcterms:abstract>
    <dc:creator>Hajnal, Matej</dc:creator>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/43615"/>
    <dcterms:issued>2021</dcterms:issued>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:creator>Šafránek, David</dc:creator>
    <dc:creator>Petrov, Tatjana</dc:creator>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/43615"/>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2022-03-17T11:23:26Z</dc:date>
    <dc:language>eng</dc:language>
    <dc:contributor>Hajnal, Matej</dc:contributor>
    <dc:contributor>Petrov, Tatjana</dc:contributor>
  </rdf:Description>
</rdf:RDF>

Universitätsbibliographie

Ja