| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
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.
Cited literature [19 references]
https://hal.inria.fr/hal-01824814
Contributor : Hal Ifip <>
Submitted on : Wednesday, June 27, 2018 - 3:55:23 PM
Last modification on : Wednesday, July 22, 2020 - 5:02:03 PM
Long-term archiving on: : Thursday, September 27, 2018 - 4:01:36 AM
Contributor : Hal Ifip <>
Submitted on : Wednesday, June 27, 2018 - 3:55:23 PM
Last modification on : Wednesday, July 22, 2020 - 5:02:03 PM
Long-term archiving on: : Thursday, September 27, 2018 - 4:01:36 AM
File
469043_1_En_7_Chapter.pdf
Files produced by the author(s)
Licence
Distributed under a Creative Commons Attribution 4.0 International License