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 ju

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!