[j-pb]

This boils down to materalizing every possible nondeterministic outcome. I wouldn't call anything that involves a power set with 2^n space complexity "relaxed" tbh ^^'. While I do agree with the general sentiment, I do still think that going with states that can be reconciled/merged is a more realistic approach, than just wildy diverging.

[User23]

This is a great submission.

The logic for taming unbounded nondeterminism has been around for decades though. As Dijkstra and Scholten admit, it’s basically just applied lattice theory.

In fact, at a glance, this paper appears to be building on that foundation. It’s not hard to see how monotonicity makes reasoning about nondeterminism considerably more manageable!

[sbazerque]

Did you read the remark at the end of my comment? In the practical cases I was exploring, that combinatorial explosion does not happen. It's relaxed in the sense that it is coordination-free.

[j-pb]

Not sure what you mean.

I'm talking about the "relaxed" P' being defined via the power set of S.

2^S= {s | s ⊆ S}

Now if all your P is only a mapping then

P'(S) = {<s, P(s)> | s ∈ S}

but then your "coordination free" P was monotonic anyways.