历史驱动的准静态调度中的状态空间压缩
1. 引言
近年来，基于形式化方法的设计方法论被大力推广，用于应对电子系统设计日益增长的复杂性。然而，传统的形式化验证方法，如模型检查或可达性分析，存在需要大量计算资源的问题。为了解决嵌入式、反应式系统软件合成中的状态空间爆炸问题，本文提出了两种互补的调度压缩技术。第一种技术通过大步骤调度，将多个转换的触发组合起来，以更粗粒度的方式探索可达性空间；第二种技术则使用基于历史的动态标准，修剪对应用领域无关紧要的状态空间。
2. 相关工作
在解决状态爆炸问题方面，已经有多种方法被提出：
-对称性检测：这种方法虽有研究，但计算复杂度与图的大小呈指数关系，存在一定局限性。
-规约理论：通过对系统规范进行可控的简化来解决问题，但所建模的情况相对简单。
-偏序方法：如在形式验证器 SPIN 中成功应用的持久集理论，适用于只依赖系统最终状态而非遍历状态历史的属性验证，但不适用于本文的情况；展开理论主要针对安全 Petri 网，而本文应用的是无界网。
-隐式枚举方法：如二进制决策图（BDDs）或区间决策图（IDDs），旨在高效存储状态空间，但构建图耗时且性能高度依赖具体问题。
-哈希表：因其简单高效，被本文用作存储已到达状态的方法。
3. 问题定义
本文处理的软件合成问题涉及由并发进程组成的系统规范。每个进程可能有输入和输出端口，用于与其他进程或环境进行通信
