[tlaplus] Using formal methods to reason about probabilistic systems

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

A long while back I posted a hilariously uninformed idea about using TLA+ to check systems that use probability: https://groups.google.com/g/tlaplus/c/ZDe9ogog6mE/m/GmBVdr-8DQAJ

After a lot of reading & learning, I've summarized how you actually can do this - not with TLA+ currently, but with PRISM. Includes some very interesting material on the subtle distinction between nondeterminism and probability. Who knows, maybe MDPs could be integrated into TLA+ some day far from now. I hope you enjoy!

https://ahelwer.ca/post/2020-04-15-probabilistic-distsys/

Andrew

-- 
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/bffea34d-f1ea-41a2-b209-ac7f32cb5bc3n%40googlegroups.com.