形式化方法驱动的模型选择：动力系统建模中的结构排序与验证

本文主要探讨了在理论计算机科学领域中使用形式化方法进行模型选择的问题，发表于《理论计算机科学电子笔记》第350期（2020年），57-71页。研究者Matej Hajnal和Samuel Pastva来自捷克布尔诺马萨里克大学的信息学院，他们针对动力系统领域中如何从一系列潜在模型中挑选最合适的模型，提出了创新的解决方案。 传统的模型选择往往依赖于模型在时间序列数据中的表现，但这可能不足以全面反映系统的动态特性。作者将注意力转向了时序逻辑，这种形式化的框架能够提供更多的全局约束，不仅限于选择单个模式，而是涉及到模型排序的问题。他们提出了几种模型排序关系，这些关系根据给定的属性规格来比较模型，以便更好地评估它们的适配度。 为了实现这一目标，论文采用了模型检查和参数综合的方法，并对这些技术进行了适应，以形成一个全面且严谨的方法论。这种方法的目的是确保在全球范围内得出精确的结果，从而指导实际的模型选择过程。作者还提到了将这种方法应用于监管网络的定性模型上的实践，这表明其在实际问题中的可行性。 论文的关键点包括模型检验，即验证模型是否满足特定的行为规范；参数综合，即通过调整参数优化模型以匹配观测数据；以及模型选择，即确定最符合系统特性的模型。此外，FFL（Flux Balance Analysis，代谢通路分析）可能是文中提到的一个工具或概念，它在生物模型的构建和分析中扮演重要角色。 该研究工作得到了捷克科学基金会（Grant No. 18-00178S）和捷克国家基础设施资助（Grant No. LM2015055）的支持，同时也强调了论文是基于开放获取许可（CC BY-NC-ND 4.0）发表的，可以在www.sciencedirect.com和www.elsevier.com/locate/entcs网站获取全文。这一研究对于生物学和系统建模领域的研究者来说，提供了有价值的方法论和实证案例，有助于简化模型选择过程，提高复杂系统理解的效率。