Comment by hwayne

I couldn't tell you the historical connections, but they "feel" related to me. This comment got me speculating about how to explain this connection; disclaimer I'm writing completely this off the cuff.

First off, NFAs and Nondet Turing Machines (NTM) would be "deterministic" with the OP definition I gave, since they always give the same decision for the same input. Their nondeterminism is a capability they have, an aspect of their process that helps reach a decision. If we need to distinguish "deterministic result" and "deterministic process", I've seen the term Observationally Deterministic used to exclusively mean the former.

A critical theorem in automata theory is that NFAs and NTMs are no more powerful than DFAs or TMs: the former cannot recognize any languages the latter cannot. This is why nondeterministic algorithms (ie, algorithms with a deterministic capability) cannot "solve more problems" than deterministic algorithms, just (probably) solve them faster (NP vs P).

(Interestingly, nondeterministic pushdown automata ARE more powerful than regular PDAs. Only NPDAs can recognize all context-free languages.)

So what does it mean for "nondeterminism" to be a capability of the process? I see the "automata/computation" and the "formal methods" as being the same idea, except with opposite outcomes. When deciding to see if a problem is in NP, we allow the algorithm to make nondeterministic choices, and accept the construction if any choice leads to valid outcome. When deciding to see if a system is satisfies required properties, we allow the model to make nondeterministic choices, and reject if any lead to an invalid outcome.

(Even more handwavy part: I've heard the terms "angelic" and "demonic" choice to distinguish the two. I think from the perspective of complexity, FM's demonic nondeterminism kinda looks like angelic choice in the co-complexity class. From the perspective of FM, complexity's angelic nondeterminism kinda looks like checking a reachability property, as opposed to a safety or liveness property.)

In either case, both are essentially abstractions over concrete implementation details. Just as I cannot physically implement "nondeterministically enter state A, B, or C", I cannot implement "nondeterministically match the regex `A|B|C`". I have to instead find a deterministic implementation, like "try to match A, and if that fails, backtrack and match B, etc."