Under-approximation

定义 Definition

under-approximation（下近似/欠近似）：一种“保守偏小”的近似方式，用不超过真实值或真实集合的结果来近似目标；在数学里常指给出下界，在程序分析/模型检测里常指用一个更小但确定属于真实行为的集合来近似系统行为（可能漏掉一些真实情况，但包含的都是真的）。

发音 Pronunciation (IPA)

/ˌʌndər əˌprɑːksəˈmeɪʃən/

词源 Etymology

由 under-（“在……之下、不足”）+ approximation（“近似”）构成。字面意思是“向下的近似”，强调结果偏小、偏保守，常与 over-approximation（上近似/过近似）成对使用。

例句 Examples

The analysis gives an under-approximation of the program’s possible outputs.
该分析给出了对程序可能输出的下近似（只覆盖其中一部分真实输出）。

Using an under-approximation can prove that certain errors are reachable, but it may miss other real behaviors.
使用下近似可以证明某些错误确实可达，但也可能漏掉其他真实行为。

相关词 Related Words

• Over-approximation
• Approximation
• Lower Bound
• Underestimate
• Abstraction
• Soundness
• Completeness
• Refinement

文学与著作中的用例 Literary Works

• Principles of Model Checking（Baier & Katoen）——在模型检测中讨论过/欠近似与可达性分析。
• Logic in Computer Science: Modelling and Reasoning about Systems（Huth & Ryan）——涉及抽象解释与近似语义（含下近似思想）。
• Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs（Cousot & Cousot，经典论文）——静态分析中“近似（上/下）”思想的重要来源。
• The Calculus of Computation: Decision Procedures with Applications to Verification（Bradley & Manna）——形式验证语境中使用近似与可达性/反例相关概念。