Constraint Markov chains (Q554215)

The article introduces constraint Markov chains as a new tool for specification. They are a generalization of interval Markov chains. Interval Markov chains extend Markov chains by labeling transitions with intervals, implying that each transition probability needs to be within the according interval. In constraint Markov chains these intervals are replaced by arbitrary constraints. This increases flexibility at the cost of increased complexity. The authors discuss operations on such constraint Markov chains including refinement, parallel composition, conjunction, and tests for consistency and satisfaction. They provide clear and proven statements concentrating on closure properties and complexity of algorithms for these operations. While interval Markov chains are not even closed under conjunction, constraint Markov chains with linear constraints are. Moreover, constraint Markov chains with polynomial constraints are proven be to sufficient for closure for conjunction and parallel composition. Special cases like deterministic constraint Markov chains and connections to probabilistic automata are discussed. The article is to a large degree self-contained. The presentation is clear and precise. Many small examples make the material accessible.