Title: Satisfiability Bounds for ω-regular Properties in Interval-valued Markov Chains,
Abstract: We derive an algorithm to compute satisfiability bounds for arbitrary
{\omega}-regular properties in an Interval-valued Markov Chain (IMC)
interpreted in the adversarial sense. IMCs generalize regular Markov Chains by
assigning a range of possible values to the transition probabilities between
states. In particular, we expand the automata-based theory of {\omega}-regular
property verification in Markov Chains to apply it to IMCs. Any
{\omega}-regular property can be represented by a Deterministic Rabin Automata
(DRA) with acceptance conditions expressed by Rabin pairs. Previous works on
Markov Chains have shown that computing the probability of satisfying a given
{\omega}-regular property reduces to a reachability problem in the product
between the Markov Chain and the corresponding DRA. We similarly define the
notion of a product between an IMC and a DRA. Then, we show that in a product
IMC, there exists a particular assignment of the transition values that
generates a largest set of non-accepting states. Subsequently, we prove that a
lower bound is found by solving a reachability problem in that refined version
of the original product IMC. We derive a similar approach for computing a
satisfiability upper bound in a product IMC with one Rabin pair. For product
IMCs with more than one Rabin pair, we establish that computing a
satisfiability upper bound is equivalent to lower-bounding the satisfiability
of the complement of the original property. A search algorithm for finding the
largest accepting and non-accepting sets of states in a product IMC is
proposed. Finally, we demonstrate our findings in a case study.