The problem is same as the title, given a Continous Stochastic Logic(CSL) formula how can we create a machine which accepts the formula? Any intuitive ideas or references will be appreciated. 
Given a CSL formula, how can we generate an automaton that accepts the formula?
lo.logic;model checking