How to a Model checker e.g. Vereofy check a LTL formula against a Reo model or equivalent CA

[Alireza Farhadi]

Dear Members,

During reading a recently published paper from Joachim Klein (http://www.springerlink.com/content/p846123j113x0345/), I see obviously how to check LTL(IO) and BSTL formula on Reo or CA model via Vereofy. I also work on some models that Natallia Kokash sent to me that use from mcrl2 encoded of Reo model via mcrl2 tools and check mu-calculus property (I found LTL and BSTL  are more simple than mu-calculus). But I want to know how a model checker works.

I read some stuff about SAT-solver, Bounded Model Checking or Symbolic Bounded Model checking, Where I found this subjects around Vereofy in papers or reports?

Is there possible to know what form of conversion must be performed on Reo or CA models that to be used for checking against these logic formulas or even how to represent these formulas to be compatible with Reo or CA models in a Model checker.

Regards,

Alireza Farhadi

[Ziyan Maraikar]

Hi

>
> I read some stuff about SAT-solver, Bounded Model Checking or Symbolic Bounded Model checking, Where I found this subjects around Vereofy in papers or reports?

Maybe this might help: http://homepages.cwi.nl/~kemper/publications.html

[Alireza Farhadi]

Thanks A Lot Dear Ziyan.

--
You received this message because you are subscribed to the Google Groups "reo-dev" group.
To post to this group, send email to reo...@googlegroups.com.
To unsubscribe from this group, send email to reo-dev+u...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/reo-dev?hl=en.