# Reachability in Parametric Interval Markov Chains using Constraints

## TL;DR

This paper introduces a formalism called parametric Interval Markov Chains (pIMCs) that incorporate parameterized probability intervals, analyzes their semantics, and develops constraint-based methods for parameter synthesis, supported by a prototype implementation.

## Contribution

It extends Markov Chain models with parametric probability intervals, compares semantics, and provides constraint-based solutions for reachability and consistency problems.

## Key findings

- Semantics for IMCs are shown to agree on reachability probabilities.
- Constraint encodings effectively solve parameter synthesis problems.
- Prototype implementation demonstrates promising results.

## Abstract

Parametric Interval Markov Chains (pIMCs) are a specification formalism that extend Markov Chains (MCs) and Interval Markov Chains (IMCs) by taking into account imprecision in the transition probability values: transitions in pIMCs are labeled with parametric intervals of probabilities. In this work, we study the difference between pIMCs and other Markov Chain abstractions models and investigate the two usual semantics for IMCs: once-and-for-all and at-every-step. In particular, we prove that both semantics agree on the maximal/minimal reachability probabilities of a given IMC. We then investigate solutions to several parameter synthesis problems in the context of pIMCs -- consistency, qualitative reachability and quantitative reachability -- that rely on constraint encodings. Finally, we propose a prototype implementation of our constraint encodings with promising results.