Dear all, It's time to define the future of MRMC and with this email I would like to start a debate. The flexibility of the current MRMC codebase is nearing its end (as expressed by Ivan), and for further growth, we need to take up a vision. Professor Katoen supports this and encourages external participation from interested parties. I want to highlight the following issues in this discussion: 1. We need to define a target of users in which we operate. We should be different. I think we should not try to compete against PRISM, but look further and open up different areas. This is going to be a difficult one. Related questions are: "in which research fields is stochastic model checking interesting, but absent?", "for which applications is stochastic verification desired, but absent?", "what problems/inconveniences do users experience with the current MRMC?" 2. We need to define the feature set of a new MRMC that is suitable for our target user. This is where our creativity comes :) 3. We need to define a global strategy that enables us to reach these users effectively. That is, we need to know the key figures, what their interests are, how they view tools and what they expect from tools. Also helpful is to know to which conferences they publish and what their key publications are. 4. We need to define a new architecture that can support this feature set. Also, to keep an overview in the discussion, I'll make sure that I'll make an overview of the discussion so far from time to time. Also, to define my role more clearly: within the ESA project I am working, it is my first duty to apply techniques readily available. My efforts will therefore mostly be about having bugs fixed in the MRMC 1.3 codebase. For the development of the future MRMC, a new HiWi can be hired to do the job (though this might take some time because finding a suitable one is not easy) Start brainstorming! :) Viet Yen -- http://www-i2.cs.rwth-aachen.de/~nguyen