Expand description
FOL → Bounded Verification IR Translation
Translates Kripke-lowered LogicExpr to a bounded timestep model. World variables (w0, w1, …) become timestep indices. Temporal accessibility predicates control the unrolling.
Structs§
- FolTranslator
- Translator from Kripke-lowered FOL to bounded timestep model.