MathSAT驱动的混合系统可达性判定：一种工业设计的有力工具

本文主要探讨了在理论计算机科学领域中，如何利用MathSAT工具解决工业混合系统的有界可达性问题。混合系统通常结合了离散控制变量和实值物理变量，这种复杂性使得传统的系统分析变得困难，因为可能存在不可判定性。混合自动机是此类系统的一种模型，它们在实际应用中广泛存在，如工厂自动化、航空航天等。 作者们提出了一种创新的方法，通过将有界可达性判定问题转换为MathSAT问题的形式，这是一种布尔组合，包含满足性命题变量和数学约束。MathSAT是一种专门用于解决满足性问题的求解器，它可以检查特定长度路径的存在性。这种方法借鉴了基于SAT（逻辑 satisfiability）的有界模型检查技术，但其独特之处在于能够直接处理实值变量，从而避免了离散化带来的局限性。 尽管面对一般混合自动机不可判定的问题，提出的这一解决方案对于实际工程设计仍然具有重要的价值，能够在一定程度上提供有价值的信息，尤其是在对大型、复杂的工业设计进行形式验证时。这种方法得到了多个欧洲资助项目的支持，包括欧盟IST-RTN项目（HPRN-CT-2000-00102）和ESACS项目（G4RD-CT-2000-00361），以及意大利MIUR-COFIN项目（2002097822003）。 总结来说，这篇文章不仅阐述了MathSAT在混合系统有界可达性问题中的应用，还展示了其在工业实践中的潜力，以及在解决这类复杂问题时所展现出的计算优势。这种方法对于推动工业系统形式验证的进步具有重要意义。