# Given a CSL formula, how can we generate an automaton that accepts the formula?

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.

• Perhaps some clarification would help. Can you give a link to relevant papers on Continuous Stochastic Logic? – cody Dec 19 '13 at 9:59
• Ok I looked up CSL and found this: www-i2.informatik.rwth-aachen.de/i2/fileadmin/user_upload/…. I'm still confused about your question though: given a formula $\psi$ of CSL, are you asking for an automaton that accepts the language $\{<\psi>\}$? The language of CSL doesn't seem to have anything special about it, and any basic parsing technique will suffice in this case. – cody Dec 19 '13 at 12:47
• I suppose not, because if it is that simple, there should be some algorithms by now. If some algorithms already exists, I am not aware of them and hence this question. – Brainy Dec 20 '13 at 9:21
• It seems like this tool takes CSL formulas as input and performs model checking on them: en.wikipedia.org/wiki/Markov_Reward_Model_Checker_%28MRMC%29. See also page 31 of this: mrmc-tool.org/downloads/MRMC/Specs/MRMC_Manual_1.5.pdf. Being able to take a CSL formula as input means that they are parseable which I believe is your question. If you are asking about verifying CLS formulas, then that is a whole other matter (also addressed by the above links). – cody Dec 20 '13 at 11:30
• You are right, but in Model checking given a model and a CSL formula it only performs transient analysis on the model and outputs whether our given formula is satisfied or not, but it don't explicitly create any automaton which accepts the given CSL. – Brainy Dec 20 '13 at 12:59