On the Controller Synthesis for Markov Decision Process of Conflict Tolerant Specification

For an embedded control system, different requirements often need be satisfied at same time, and some of them make the system to act conflicted. Conflict tolerant specification is provided to denote this situation. In such a system, there often exist probabilistic and non-deterministic behaviors. We use Markov Decision Process (MDP) to denote these features. We study the controller synthesis for MDP over conflict tolerant specification. We extend PCTL star by adding past operator to denote the conflict tolerant specification succinctly. We use CT-PLTL to denote conflicted actions and PCTL to denote the specification for probability demand. We first synthesize a controller on a base system over CT-PLTL and then use it to prune the corresponding MDP of the system model. We use the resulting sub-MDP as the model to further synthesis a controller over PCTL. The whole controller for MDP is a conjunction of the two controllers obtained.