Re: [tlaplus] Is Dempster Shaffer/Probabilistic Reasoning possible in TLA plus

I don't know what Dempster Shaffer reasoning is, but for formalizing & model-checking probabilistic properties of state machines I wrote an introductory blog post you might like, which covers Discrete-Time Markov Chains (DTMCs) and Markov Decision Processes (MDPs): How do you reason about a probabilistic distributed system?

The premier probabilistic model-checking platform is currently PRISM. The FizBee specification language also checks DTMC properties. TLA+ itself does not easily check these properties. For info on TLA+ capabilities in this domain, see the talk Obtaining Statistical Properties via TLC Simulation from the 2022 TLA+ Conference by Jack Vanlighty and Markus A. Kuppe.

You might be interested in how these systems actually formalize and check probabilistic properties over state machines, in which case the best introduction I've found is Model Checking Meets Probability: A Gentle Introduction by Joost-Pieter Katoen. This covers DTMCs and MDPs, and also Continuous-Time Markov Chains (CTMCs). CTMCs are often used in queuing theory analyses, with varying probability distributions generating arrival rates. One densely theoretical resource for this topic I've read is the textbook Performance Modeling and Design of Computer Systems: Queueing Theory in Action by Mor Harchol-Balter. This author also has published a newer textbook called Introduction to Probability for Computing which might be more approachable; I don't know, I haven't read it.

Andrew Helwer

On Fri, Aug 29, 2025 at 7:06 AM Matthew Thompson <thompsonson@xxxxxxxxx> wrote:

Hello group,

I am new to formal methods and TLA plus, I have followed Leslie Lamport's excellent and beautifully idiosyncratic tutorial, I now think what I am trying to achieve is not actually possible with TLA plus.

My objective is to learn if probabilistic reasoning or similar can be done with formal methods. Would anybody be able to provide me information where I can learn from the ground up how to do this?

Please excuse this email if it is out of scope of this group.

Many thanks,
Matthew Thompson

--
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 visit https://groups.google.com/d/msgid/tlaplus/9ab49cd2-773a-43eb-8d3d-17dd54d426f0n%40googlegroups.com.