Re: [tlaplus] Re: Best way to handle a probabilistic data structure.

["A. Jesse Jiryu Davis" <jesse@xxxxxxxxxxxxxxx>]

Thomas, if you're interested in the actual probabilities (i.e. what percent of the time do you get false positives?) then I agree with Andrew's answer. If, on the other hand, you don't care about the probabilities, and you just want to specify a system that works correctly in the face of false positives, you might do something like this:

\* Some action that relies on the Bloom filter

Search(value) ==

  \* Either the correct result or a false positive

  \E bloomResult \in { (value \in mySet), TRUE} :

    \* Do something with the result

    latestResult' = bloomResult

This spec explores both the correct-result and false-positive paths.

On Fri, Oct 18, 2024 at 1:16 PM Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:

If you want to analyze the actual probability properties of something like this, you may be more interested in PRISM. It supports modeling both Discrete-Time Markov Chains (DTMCs) which have a probabilistic state transition out of every state, and a mixed nondeterminism/probabilistic transition model called a Markov Decision Process (MDP). I wrote about the differences between these two models here: https://ahelwer.ca/post/2020-09-11-probabilistic-distsys/

If you are more interested in exploring this problem with TLA+ I recommend taking a look at this spec authored by Markus Kuppe and Ron Pressler: https://github.com/tlaplus/Examples/tree/master/specifications/KnuthYao

Andrew Helwer

On Friday, October 18, 2024 at 12:17:05 PM UTC-4 thomas...@xxxxxxxxx wrote:

I just realized that this might be a malformed question; it probably makes sense to express this in the "next-state" level instead of the operator level.

On Friday, October 18, 2024 at 11:31:46 AM UTC-4 thomas...@xxxxxxxxx wrote:

I wanted to simulate something like a Bloom Filter. For those unaware, a Bloom Filter is kind of like a set, but when looking up a value in a set, there's a risk of a false positive, but never a risk of a false negative.

I'm not terribly concerned with the actual implementation of this, so I just wanted to make an operator like "IsInFilter(value, filter)", where filter is actually just a set, and if value is in the set it might return TRUE or FALSE, but if it's not in the set it always returns FALSE.

I'm having a little trouble expressing the non-determinism with this.  My initial implementation was something like this:


IsInSet(value, mySet) ==
    \E result \in {TRUE, FALSE} :
        (value \in mySet => result) /\ (value \notin mySet => FALSE)

But I think the existential quantifier in this case is tautological.  Does anyone have any ideas on the best way of handling this?

--
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/5f6efaa9-10bd-48a6-aa00-be4975d75741n%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/CAFRUCtZQfDXjgBVopau0chr0szj9JHb_8j-fyPU-oGqH9JYxEA%40mail.gmail.com.