← 研踪 PaperTrailarXiv:2611.16815 · v1
Selective Chaining of Parameterised Boolean Equation Systems
首次提交 2026-11-12 21:51
版本更新 2026-11-12 21:51
雷达观测 2026-11-13 14:15
摘要
Parameterised Boolean Equations Systems (PBESs) are used to verify properties of formal industrial models. We introduce a technique called selective chaining to simplify these PBESs by unfolding specific predicate variable instances when the unfolding results in a PBES that is likely to be simpler. For determining the latter we propose a set of heuristics. We show the formal correctness of the chaining operator and provide theoretical upper bounds using relevancy graphs on the size of the verification problem after chaining. Lastly, we study the effectiveness of our heuristics, showing that selective chaining can reduce memory usage and yield significant speed-ups solving PBESs that encode model checking problems for complex industrial systems.
作者备注：Pre-print for FSEN 2027
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v1 · 2026-11-12 21:51 · 最新观测版本
Selective Chaining of Parameterised Boolean Equation Systems
Parameterised Boolean Equations Systems (PBESs) are used to verify properties of formal industrial models. We introduce a technique called selective chaining to simplify these PBESs by unfolding specific predicate variable instances when the unfolding results in a PBES that is likely to be simpler. For determining the latter we propose a set of heuristics. We show the formal correctness of the chaining operator and provide theoretical upper bounds using relevancy graphs on the size of the verification problem after chaining. Lastly, we study the effectiveness of our heuristics, showing that selective chaining can reduce memory usage and yield significant speed-ups solving PBESs that encode model checking problems for complex industrial systems.
查看此版本解读 →查看此版本原文 ↗