非确定性的天使与恶魔

本文探讨了形式化方法中的两种非确定性：恶魔式非确定性假设系统总是做出最坏选择，用于验证所有路径都满足属性；天使式非确定性假设系统总是做出最佳选择，用于验证存在满足属性的路径。后者在复杂性分析和编程语言中更为常见，如NP问题的定义就基于天使式非确定性。