Parameter Synthesis Algorithms for Parametric Interval Markov Chains

Laure Petrucci, Jaco van de Pol

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    2 Citations (Scopus)
    90 Downloads (Pure)

    Abstract

    This paper considers the consistency problem for Parametric Interval Markov Chains. In particular, we introduce a co-inductive definition of consistency, which improves and simplifies previous inductive definitions considerably. The equivalence of the inductive and co-inductive definitions has been formally proved in the interactive theorem prover PVS. These definitions lead to forward and backward algorithms, respectively, for synthesizing an expression for all parameters for which a given PIMC is consistent. We give new complexity results when tackling the consistency problem for IMCs (i.e. without parameters). We provide a sharper upper bound, based on the longest simple path in the IMC. The algorithms are also optimized, using different techniques (dynamic programming cache, polyhedra representation, etc.). They are evaluated on a prototype implementation. For parameter synthesis, we use Constraint Logic Programming and the PARMA library for convex polyhedra.
    Original languageEnglish
    Title of host publicationFormal Techniques for Distributed Objects, Components, and Systems
    Subtitle of host publication38th IFIP WG 6.1 International Conference, FORTE 2018, Held as Part of the 13th International Federated Conference on Distributed Computing Techniques, DisCoTec 2018, Madrid, Spain, June 18-21, 2018, Proceedings
    EditorsChristel Baier, Luis Caires
    Place of PublicationCham
    PublisherSpringer
    Pages121-140
    Number of pages20
    ISBN (Electronic)978-3-319-92612-4
    ISBN (Print)978-3-319-92611-7
    DOIs
    Publication statusPublished - Jun 2018
    Event38th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2018 - University Complutense of Madrid, Madrid, Spain
    Duration: 18 Jun 201821 Jun 2018
    Conference number: 38
    http://2018.discotec.org/index.html

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume10854
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference38th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2018
    Abbreviated titleFORTE 2018
    CountrySpain
    CityMadrid
    Period18/06/1821/06/18
    OtherHeld as Part of the 13th International Federated Conference on Distributed Computing Techniques, DisCoTec 2018
    Internet address

    Keywords

    • Parametric interval Markov chains
    • Consistency checking
    • Parameter synthesis
    • Parma polyhedra library
    • Constraint solving

    Fingerprint Dive into the research topics of 'Parameter Synthesis Algorithms for Parametric Interval Markov Chains'. Together they form a unique fingerprint.

    Cite this