<p>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. </p>

CC BY-SA 3.0
2013-12-19T09:59:37.753Z
Perhaps some clarification would help. Can you give a link to relevant papers on Continuous Stochastic Logic?
cody
CC BY-SA 3.0
2013-12-19T12:47:05.360Z
Ok I looked up CSL and found this: http://www-i2.informatik.rwth-aachen.de/i2/fileadmin/user_upload/documents/Advanced_Model_Checking/amc_lec22.pdf. 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
CC BY-SA 3.0
2013-12-20T09:21:38.740Z
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
CC BY-SA 3.0
2013-12-20T11:30:41.593Z
It seems like this tool takes CSL formulas as input and performs model checking on them: http://en.wikipedia.org/wiki/Markov_Reward_Model_Checker_%28MRMC%29. See also page 31 of this: http://www.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
CC BY-SA 3.0
2013-12-20T12:59:38.637Z
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
CC BY-SA 3.0
2013-12-20T16:01:28.617Z
I'm still confused to what you mean by "accept the given CSL". Do you mean prove that the formula is valid?
cody
<lo.logic><model-checking>
Given a CSL formula, how can we generate an automaton that accepts the formula?
Brainy
# Given a CSL formula, how can we generate an automaton that accepts the formula?

(Asked by: username_0 on 2013-12-18)

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.

**Tags:** lo.logic, model-checking
> **Comments:**
> **username_1**: Perhaps some clarification would help. Can you give a link to relevant papers on Continuous Stochastic Logic?  
> **username_1**: Ok I looked up CSL and found this: http://www-i2.informatik.rwth-aachen.de/i2/fileadmin/user_upload/documents/Advanced_Model_Checking/amc_lec22.pdf. 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.  
> **username_0**: 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.  
> **username_1**: It seems like this tool takes CSL formulas as input and performs model checking on them: http://en.wikipedia.org/wiki/Markov_Reward_Model_Checker_%28MRMC%29. See also page 31 of this: http://www.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).  
> **username_0**: 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.  
> **username_1**: I'm still confused to what you mean by "accept the given CSL". Do you mean prove that the formula is valid?  

---

## 0 answers

