The Angels and Demons of Nondeterminism

The article contrasts demonic nondeterminism, where systems make worst-case choices to verify properties on all paths, with angelic nondeterminism, where they make best-case choices to verify properties on any path. Angelic nondeterminism underpins complexity class NP and serves as an abstraction in declarative languages.