Re: [tlaplus] Re: Ideas for model-checking probabilistic consensus systems?

After talking it out with Hillel this morning I now see probabilistic model checking is waaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaay more difficult than I assumed in my post. For example:

Every nondeterministic state transition must have a probability associated with it; the only question is whether that probability is uniform
When there are multiple paths to reach the same state, the probability of reaching that state is the sum of the probabilities of those paths

I had assumed probabilistic model checking looked like basic safety checking, but it looks a lot more similar to liveness checking. Interested in seeing the algorithms behind PRISM and such, though.

Andrew

On Wednesday, August 14, 2019 at 7:41:52 AM UTC-7, Hillel Wayne wrote:

I did some research on this and PRISM is actually the most advanced probabilistic modeling language out there. Verifying probability is really, really hard! For your use case you're probs best off writing a python script to autogen PRISM specs for you. You might be able to use the PRISM preprocessor, but that's still in beta: http://www.prismmodelchecker.org/prismpp/

Alernatively you might want to try using one of the experimental extensions to PRISM, like ProFeat: https://wwwtcs.inf.tu-dresden.de/ALGI/PUB/ProFeat/

On 8/14/19 9:14 AM, Andrew Helwer wrote:

Per Hillel's post on PRISM (https://www.hillelwayne.com/post/prism/) it doesn't do sets/tuples/etc., you have to hardcode every element in the model; are there other modeling languages which don't have this restriction?

On Tuesday, August 13, 2019 at 7:05:18 PM UTC-7, Kai wrote:

Rather than waiting for a non-trivial extension to TLA and the toolbox, you may want to explore existing tools that target probabilistic systems, e.g., PRISM. The literature on it should have poiters to formalisms and tools in the area.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6d157040-12c3-491c-94fd-bf1b88c2013e%40googlegroups.com.