[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Wed, 14 Aug 2019 12:59:56 -0700 (PDT)*References*: <ccad7213-a26e-43e0-97bc-f55b83612c82@googlegroups.com> <fe4022c6-a1db-4241-9f0b-33cd6d17bbcb@googlegroups.com> <6d157040-12c3-491c-94fd-bf1b88c2013e@googlegroups.com> <0415754b-e45d-ac3f-d90f-a3d8cc65645b@gmail.com>

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:

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

-- - 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

advancedprobabilistic modeling language out there. Verifying probability is really,reallyhard! 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

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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/51a85e03-ae59-4f7f-b65d-c777573f108d%40googlegroups.com.

**References**:**Ideas for model-checking probabilistic consensus systems?***From:*Andrew Helwer

**[tlaplus] Re: Ideas for model-checking probabilistic consensus systems?***From:*'kaie@xxxxxxxxxxxxxxx' via tlaplus

**[tlaplus] Re: Ideas for model-checking probabilistic consensus systems?***From:*Andrew Helwer

**Re: [tlaplus] Re: Ideas for model-checking probabilistic consensus systems?***From:*Hillel Wayne

- Prev by Date:
**Re: [tlaplus] Debugging endless model checking** - Next by Date:
**Re: [tlaplus] Ability to use Vim keystrokes with TLA+ Toolbox?** - Previous by thread:
**Re: [tlaplus] Re: Ideas for model-checking probabilistic consensus systems?** - Next by thread:
**[tlaplus] Re: Ideas for model-checking probabilistic consensus systems?** - Index(es):