Predicate Abstraction
Definition
Predicate abstraction maps a rich state space into a finite logical abstraction defined by a chosen set of predicates.
Why It Matters
It can make verification tractable while retaining the distinctions that matter for a target property.
Formalism / Key Objects
- predicates over original states
- abstract states defined by truth assignments to those predicates
- abstraction and refinement loops
Connections
- Often paired with Formal Methods workflows for verification.
- Can support safety analysis in Safe Multi-Agent Reinforcement Learning.
- Often relates to Invariant Synthesis and counterexample-guided refinement.
Common Confusions
- Predicate abstraction is only as useful as the predicates chosen.
- An abstraction that is too coarse can produce spurious counterexamples.