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

Thanks for these links 🙏🏼

I've read you're article and some of the Prism tutorials. My initial read is of bits being used in a Frequentist view of probability, it'll take me a bit more time to absorb and get to the dynamic/belief probabilistic aspects.

I thought I'd share more info on why I was asking about Dempster-Shafer; Dempster introduced and Shafer refined belief and plausibility functions, which are represented in the range [0,1] (which itself represents no knowledge).

It was an advancement on Shortliffe's Certainty Factor in Expert Systems - specifically the MYCIN system. To be fair this looked like a nice development to help solve the "Penguin's can't fly" monotonic problem - apparently a significant part of what killed expert systems back in the day and took Certainty Factors down with it.

Here's an extract from Norvig's Paradigms of Artificial Intelligence Programming.

https://github.com/norvig/paip-lisp/blob/9cea73837e439d331fe78d7b585e994c7113aac2/docs/chapter16.md#169-alternatives-to-certainty-factors

"Before MYCIN, most reasoning with uncertainty was done using probability theory. The laws of probability-in particular, Bayes's law-provide a well-founded mathematical formalism that is not subject to the inconsistencies of certainty factors. Indeed, probability theory can be shown to be the only formalism that leads to rational behavior, in the sense that if you have to make a series of bets on some uncertain events, combining information with probability theory will give you the highest expected value for your bets. Despite this, probability theory was largely set aside in the mid-1970s. The argument made by Shortliffe and Buchanan (1975) was that probability theory required too many conditional probabilities, and that people were not good at estimating these. They argued that certainty factors were intuitively easier to deal with. Other researchers of the time shared this view. Shafer, with later refinements by Dempster, created a theory of belief functions that, like certainty factors, represented a combination of the belief for and against an event. Instead of representing an event by a single probability or certainty, Dempster-Shafer theory maintains two numbers, which are analogous to the lower and upper bound on the probability. Instead of a single number like .5, Dempster-Shafer theory would have an interval like [.4,.6] to represent a range of probabilities. A complete lack of knowledge would be represented by the range [0,1]. A great deal of effort in the late 1970s and early 1980s was invested in these and other nonprobabilistic theories. Another example is Zadeh's fuzzy set theory, which is also based on intervals."

And a vid that nicely shows how it is different from Probability Theory - the car being *either* black or brown and that is not included in the mass of a car being *only* black or brown really helped me understand further: https://youtu.be/51ssBAp_i5Y?si=aZEybAL5EOGrUqLD

Matt

On Fri, 29 Aug 2025, 17:27 Andrew Helwer, <andrew.helwer@xxxxxxxxx> wrote:

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.

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/KB-c_dyxlVE/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUX_srwawP7E%2BPCVBu9ks9yVdGMAKtF%3D2iOZAQrvNwXpjQ%40mail.gmail.com.