4 ms·
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"
by j-pb 2y ago
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 2y agoThis 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 2y agoDid 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 2y agoNot 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.