Scholarlink

Ordered binary decision diagrams (OBDDs) are a fundamental data structure for the manipulation of Boolean functions, with strong applications to finite-state symbolic model checking. OBDDs allow for efficient algorithms using top-down dynamic programming. From an automata-theoretic perspective, OBDDs essentially are minimal deterministic finite automata recognizing languages whose words have a fixed length (the arity of the Boolean function). We introduce weakly acyclic diagrams (WADs), a generalization of OBDDs that maintains their algorithmic advantages, but can also represent infinite languages. We develop the theory of WADs and show that they can be used for symbolic model checking of various models of infinite-state systems.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Weakly Acyclic Diagrams: A Data Structure for Infinite-State Symbolic Verification

  • 会议论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年

查看全文
  • Michael Blondin,
  • Michaël Cadilhac,
  • Xin-Yi Cui,
  • Philipp Czerner,
  • Javier Esparza,
  • Jakob Schulz

摘要

Ordered binary decision diagrams (OBDDs) are a fundamental data structure for the manipulation of Boolean functions, with strong applications to finite-state symbolic model checking. OBDDs allow for efficient algorithms using top-down dynamic programming. From an automata-theoretic perspective, OBDDs essentially are minimal deterministic finite automata recognizing languages whose words have a fixed length (the arity of the Boolean function). We introduce weakly acyclic diagrams (WADs), a generalization of OBDDs that maintains their algorithmic advantages, but can also represent infinite languages. We develop the theory of WADs and show that they can be used for symbolic model checking of various models of infinite-state systems.