Consistency in Parametric Interval Probabilistic Timed Automata

TL;DR

This paper introduces Parametric Interval Probabilistic Timed Automata, a new formalism for probabilistic timed systems, and studies the decidability of their consistency problem with practical algorithms for certain cases.

Contribution

It extends existing models with parameters and intervals, providing decidability results and algorithms for consistency checking in probabilistic timed automata.

Findings

Decidability of the consistency problem for non-parametric models.

A constructive algorithm for checking consistency.

Syntactic conditions ensuring decidability in parametric cases.

Abstract

We propose a new abstract formalism for probabilistic timed systems, Parametric Interval Probabilistic Timed Automata, based on an extension of Parametric Timed Automata and Interval Markov Chains. In this context, we consider the consistency problem that amounts to deciding whether a given specification admits at least one implementation. In the context of Interval Probabilistic Timed Automata (with no timing parameters), we show that this problem is decidable and propose a constructive algorithm for its resolution. We show that the existence of timing parameter valuations ensuring consistency is undecidable in the general context, but still exhibit a syntactic condition on parameters to ensure decidability. We also propose procedures that resolve both the consistency and the consistent reachability problems when the parametric probabilistic zone graph is finite.