Formal Synthesis of Control Policies for Continuous Time Markov Processes From Time-Bounded Temporal Logic Specifications

We consider the control synthesis problem for continuous-time Markov decision processes (CTMDPs), whose expected behaviors are measured by the satisfaction of Continuous Stochastic Logic (CSL) formulas. We present an extension of the CSL for CTMDPs involving sequential task specifications with continuous time constraints on the execution of those tasks. We then exploit model checking and time-bounded reachability algorithms to solve the CSL control synthesis problem. To illustrate the feasibility and effectiveness of our approach, we apply our methods to generate the optimal rate constants of a coupled set of biochemical reactions.