%0 Conference Proceedings
%T Parameter Synthesis Algorithms for Parametric Interval Markov Chains
%+ Laboratoire d'Informatique de Paris-Nord (LIPN)
%+ University of Twente
%A Petrucci, Laure
%A Pol, Jaco, van De
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 38th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Madrid, Spain
%Y Christel Baier
%Y Luís Caires
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-10854
%P 121-140
%8 2018-06-18
%D 2018
%R 10.1007/978-3-319-92612-4_7
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01824814/document
%2 https://inria.hal.science/hal-01824814/file/469043_1_En_7_Chapter.pdf
%L hal-01824814
%U https://inria.hal.science/hal-01824814
%~ UNIV-PARIS13
%~ CNRS
%~ LIPN
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ USPC
%~ IFIP-FORTE
%~ IFIP-DISCOTEC
%~ GALILE
%~ IFIP-LNCS-10854
%~ SORBONNE-PARIS-NORD