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

[tlaplus] Using formal methods to reason about probabilistic systems

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!



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.