非決定性の天使と悪魔

非決定性には「悪魔的非決定性」（常に最悪の選択をする）と「天使的非決定性」（常に最善の選択をする）の2種類がある。前者は形式手法で安全性検証に使われ、後者は計算複雑性理論やプログラミング言語で広く用いられる。NP問題は天使的非決定性を持つ多項式時間アルゴリズムで解ける問題として定義される。