Parameter Synthesis Algorithms for Parametric Interval Markov Chains

Laure Petrucci; Jaco van de Pol

doi:10.1007/978-3-319-92612-4_7

Parameter Synthesis Algorithms for Parametric Interval Markov Chains

Laure Petrucci, Jaco van de Pol

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

5 Citations (Scopus)

163 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 language	English
Title of host publication	Formal Techniques for Distributed Objects, Components, and Systems
Subtitle of host publication	38th 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
Editors	Christel Baier, Luis Caires
Place of Publication	Cham
Publisher	Springer
Pages	121-140
Number of pages	20
ISBN (Electronic)	978-3-319-92612-4
ISBN (Print)	978-3-319-92611-7
DOIs	https://doi.org/10.1007/978-3-319-92612-4_7
Publication status	Published - Jun 2018
Event	38th 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 2018 → 21 Jun 2018 Conference number: 38 http://2018.discotec.org/index.html

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	10854
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	38th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2018
Abbreviated title	FORTE 2018
Country/Territory	Spain
City	Madrid
Period	18/06/18 → 21/06/18
Other	Held as Part of the 13th International Federated Conference on Distributed Computing Techniques, DisCoTec 2018
Internet address	http://2018.discotec.org/index.html

Keywords

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

Access to Document

10.1007/978-3-319-92612-4_7

Petrucci2018parameterAccepted author version, 377 KB

Cite this

Petrucci, L., & van de Pol, J. (2018). Parameter Synthesis Algorithms for Parametric Interval Markov Chains. In C. Baier, & L. Caires (Eds.), Formal Techniques for Distributed Objects, Components, and Systems: 38th 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 (pp. 121-140). (Lecture Notes in Computer Science; Vol. 10854). Springer. https://doi.org/10.1007/978-3-319-92612-4_7

Petrucci, Laure ; van de Pol, Jaco. / Parameter Synthesis Algorithms for Parametric Interval Markov Chains. Formal Techniques for Distributed Objects, Components, and Systems: 38th 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. editor / Christel Baier ; Luis Caires. Cham : Springer, 2018. pp. 121-140 (Lecture Notes in Computer Science).

@inproceedings{786bd7f632a047beb6b4432bf69b5ed9,

title = "Parameter Synthesis Algorithms for Parametric Interval Markov Chains",

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.",

keywords = "Parametric interval Markov chains, Consistency checking, Parameter synthesis, Parma polyhedra library, Constraint solving",

author = "Laure Petrucci and {van de Pol}, Jaco",

year = "2018",

month = jun,

doi = "10.1007/978-3-319-92612-4_7",

language = "English",

isbn = "978-3-319-92611-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "121--140",

editor = "Christel Baier and Luis Caires",

booktitle = "Formal Techniques for Distributed Objects, Components, and Systems",

address = "Germany",

note = "38th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2018, FORTE 2018 ; Conference date: 18-06-2018 Through 21-06-2018",

url = "http://2018.discotec.org/index.html",

}

Petrucci, L & van de Pol, J 2018, Parameter Synthesis Algorithms for Parametric Interval Markov Chains. in C Baier & L Caires (eds), Formal Techniques for Distributed Objects, Components, and Systems: 38th 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. Lecture Notes in Computer Science, vol. 10854, Springer, Cham, pp. 121-140, 38th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2018, Madrid, Spain, 18/06/18. https://doi.org/10.1007/978-3-319-92612-4_7

Parameter Synthesis Algorithms for Parametric Interval Markov Chains. / Petrucci, Laure; van de Pol, Jaco.
Formal Techniques for Distributed Objects, Components, and Systems: 38th 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. ed. / Christel Baier; Luis Caires. Cham: Springer, 2018. p. 121-140 (Lecture Notes in Computer Science; Vol. 10854).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Parameter Synthesis Algorithms for Parametric Interval Markov Chains

AU - Petrucci, Laure

AU - van de Pol, Jaco

N1 - Conference code: 38

PY - 2018/6

Y1 - 2018/6

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

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

KW - Parametric interval Markov chains

KW - Consistency checking

KW - Parameter synthesis

KW - Parma polyhedra library

KW - Constraint solving

UR - http://www.scopus.com/inward/record.url?scp=85048248477&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-92612-4_7

DO - 10.1007/978-3-319-92612-4_7

M3 - Conference contribution

SN - 978-3-319-92611-7

T3 - Lecture Notes in Computer Science

SP - 121

EP - 140

BT - Formal Techniques for Distributed Objects, Components, and Systems

A2 - Baier, Christel

A2 - Caires, Luis

PB - Springer

CY - Cham

T2 - 38th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2018

Y2 - 18 June 2018 through 21 June 2018

ER -

Petrucci L, van de Pol J. Parameter Synthesis Algorithms for Parametric Interval Markov Chains. In Baier C, Caires L, editors, Formal Techniques for Distributed Objects, Components, and Systems: 38th 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. Cham: Springer. 2018. p. 121-140. (Lecture Notes in Computer Science). doi: 10.1007/978-3-319-92612-4_7

Parameter Synthesis Algorithms for Parametric Interval Markov Chains

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this