QDDC到符号自动机翻译：非确定性与确定性接受器的应用

本文主要探讨了量化离散持续时间演算QDDC的符号自动机翻译及其在模型检查中的应用。QDDC是一种特殊的时态逻辑，旨在描述具有离散和连续成分的系统行为。作者Laure Gonnord、Nicolas Halbwachs和Pascal Raymond合作，将P. Pandya提出的QDDC理论转化为一种形式，即使用带有计数器的符号接受器，这种接受器基于同步编程语言Lustre编写。 翻译过程中，他们强调了QDDC中的关键结构对非确定性接受器的需求，因为这些结构可以通过有限数量的计数器得以实现和表达。通过这种方式，他们能够将QDDC的逻辑片段有效地识别和转换成符号自动机的形式，这有助于利用现有的模型检查器和抽象解释器来验证QDDC所表述的属性。 然而，他们的研究还涉及了一个更严格的子集，其中仅需要确定性接受器。这是因为在某些情况下，确定性策略可能更为适合，特别是在处理实际程序验证时，非确定性可能会引入额外的复杂性和不确定性。 该工作的目标不仅是提升时态逻辑可判定性的理解，还在于将理论上的概念转化为实践工具，使得程序验证更加有效和精确。通过将QDDC与同步观测器（即接受器）相结合，他们提供了一种方法来分析程序的动态行为，从而确保其符合指定的时间约束和逻辑条件。 这篇论文贡献了将量化离散持续时间演算QDDC的理论框架与实际程序验证技术相结合的新视角，这对于理解和设计复杂系统的实时行为验证具有重要意义。通过将QDDC模型转换为符号自动机，并利用同步编程语言和模型检查器，研究人员能够更高效地分析程序的正确性和性能。