...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Innovations in Systems and Software Engineering >Optimal compression of combinatorial state spaces
【24h】

Optimal compression of combinatorial state spaces

机译：组合状态空间的最佳压缩

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Efficiently deciding reachability for model checking problems requires storing the entire state space. We provide an information theoretical lower bound for these storage requirements using only the assumption of locality in the model checking input. The theory shows that a set of n vectors with k slots can be compressed to a single slot plus O(log_2(k)) overhead. Using a binary tree in combination with a compact hash table, we then analytically show that this compression can be attained in practice, without compromising fast query times for state vector lookups. Our implementation of this Compact Tree can compress n > 2~(32) state vectors of arbitrary length k {much less than} n down to 32 bits per vector. This compression is lossless. Experiments with over 350 inputs in five different model checking formalisms confirm that the lower bound is reached in practice in a majority of cases, confirming the combinatorial nature of state spaces.
机译：有效地确定模型检查问题的可达性需要存储整个状态空间。 我们只使用模型检查输入中的局部性的假设为这些存储要求提供了一个信息的理论下限。 该理论表明，具有k个槽的一组N载体可以被压缩到单个槽加上O（log_2（k））开销。 使用二叉树与紧凑散列表组合使用，然后我们分析显示，可以在实践中实现这种压缩，而不会影响状态矢量查找的快速查询时间。 我们的这种紧凑型树的实现可以压缩n> 2〜（32）任意长度K的状态矢量{远低于} n为每vector的32位。 这种压缩是无损的。 在五种不同模型中有超过350个输入的实验检查形式主义确认，在大多数情况下，在实践中达到了下限，确认了状态空间的组合性质。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号