
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.
Specification and verification (program logics, model checking, etc.), Markov chains, Process algebra, Specification theory, Compositional reasoning, Markov Chains, Markov chains (discrete-time Markov processes on discrete state spaces), closure properties, 004, [INFO.INFO-OH] Computer Science [cs]/Other [cs.OH], specification theory, Abstraction, process algebra
Specification and verification (program logics, model checking, etc.), Markov chains, Process algebra, Specification theory, Compositional reasoning, Markov Chains, Markov chains (discrete-time Markov processes on discrete state spaces), closure properties, 004, [INFO.INFO-OH] Computer Science [cs]/Other [cs.OH], specification theory, Abstraction, process algebra
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 35 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
