用于能量博弈的符号化 BDD 与 ADD 算法
计算机科学中的逻辑
2016-11-24 v1 数据结构与算法
计算机科学与博弈论
摘要
能量博弈对有限资源（如时间或能量）的定量消耗进行建模，在反应式系统的定量模型中扮演核心角色。反应式合成会构建一个满足给定规约的控制器（若存在）。对于能量博弈，合成出的控制器不仅要满足规约的安全约束，还要满足能量博弈中表达的定量约束。Chatterjee 等人最近提出的能量博弈符号化算法，在定量值的表示上是符号化的，但在博弈状态和转移的表示上是具体的。本文提出一种在定量值和底层博弈表示两方面均为符号化的算法。我们使用两种不同的反应式博弈符号化表示——二元决策图（Binary Decision Diagrams, BDD）和代数决策图（Algebraic Decision Diagrams, ADD）——实现了该算法。我们研究了两种实现的共性与差异，并比较了它们在能量博弈规约上的运行时间。
引用
@article{arxiv.1611.07622,
title = {Symbolic BDD and ADD Algorithms for Energy Games},
author = {Shahar Maoz and Or Pistiner and Jan Oliver Ringert},
journal= {arXiv preprint arXiv:1611.07622},
year = {2016}
}
备注
In Proceedings SYNT 2016, arXiv:1611.07178