并发时间自动机检验算法中的空间压缩技术

本项目的研究内容为在验证并发时间自动机算法中的空间压缩技术，主要包括偏充技术和约束消除技术，偏序技术通过忽略不相关转换之间的顺序来避免对空间的无谓分割。约束消除技术通过静态和动态分析技术来消除无用的约束。这些技术将推动实时系统自动验证技术走向实际应用，提高计算机系统的可靠性。本研究将促进理论研究成果走向应用。