一种正式的作物建模方法：利用有限状态自动机进行代码自动生成和网格模拟

《Computers and Electronics in Agriculture》：A formal approach to crop modeling: Automatic code generation and grid simulation using finite state automata

　　•TOMGRO 是使用 DTHA 编写的正式模型，由三个独立的自动机组成。•源代码是使用 ESCET 自动生成的，并且其可扩展性已经过测试。•在不同微气候条件下模拟了植物生长过程。•通过使用 DTHA 形式主义，我们能够轻松地设置和自动模拟复杂的复种植物场景。

引言
自20世纪80年代以来，作物建模一直是农学研究中的一个重要课题，其根源可以追溯到20世纪60年代（参见Wit (1965)）。随着时间的推移，针对不同作物提出了各种模型及其变体，以提高生产和质量，同时优化农环境管理（Hajirad 等，2025），并考虑了经济约束、田间试验中的产量变化（Roja 等，2023）以及更严格的消费者保护法规（REG 1107/09/CE）。在这些背景下，监测作物生长并预测疾病或不良情况对于在满足质量和数量目标的同时保护关键资源至关重要。为了获得可靠的预测结果，必须根据目标环境对模型进行适当的校准和评估，并用通过传感器收集的真实世界数据或通过专门定制和精细调整的气候模型生成的数据来喂养模型。然后可以利用这些预测结果触发手动或自动的操作来影响环境，例如调整人工气候控制或激活灌溉以支持植物生长。这种循环在工业环境中被称为数字孪生（DT）（Barricelli 等，2019）。数字孪生是一个给定系统的数字副本，它与系统同步发展，现实世界和虚拟世界互相连接并交换信息和指令：现实系统通过传感器将数据发送给模型；模型随后随着现实系统的发展而演变，并通过执行器对系统进行干预，以促进朝着特定目标的条件和发展方向发展。数字孪生的概念大约十年前在工业自动化领域流行起来，然后迅速传播到其他研究领域（Liu 等，2019；Bhatti 等，2021；Qi 和 Tao，2018），最近又扩展到农业领域（Purcell 和 Neubauer，2023）。然而，由于这些系统各个组件之间的相互作用更为复杂，因此在农业中正确应用数字孪生解决方案需要额外的努力。在下文中，我们强调了将数字孪生框架扩展到农业中的两个关键挑战。

首先，根据数字孪生的范式，模型应该随着时间的推移不断改进，以与实际植物相符，但其高度复杂性可能会阻碍这一过程。此外，由于活植物对轻微的环境异质性的反应不同，一个合适的数字孪生解决方案应该理想地模拟每株植物，或者至少是一组具有相同气候和土壤条件的植物。为此，评估环境中的气候变异性变得至关重要；然而，在建模过程中通常忽略了这一方面，因为传统的气候和生长模型，尤其是在中等至低技术水平下，依赖于点时间（或点空间）读数来估计总体情况，假设它们代表整个品种的平均值。Xu 等人（2022）和 Brentarolli 等人（2024）的研究表明，即使是在受保护的环境中，如温室中，气候异质性仍然存在并且必须加以解决。一旦有足够的空间数据，就可以将其用作输入到数字孪生模型中，以估计植物生长的空间分布，例如 Shelia 等人（2019）和 Alderman（2021）的研究，他们通过扩展模拟模型 DSSAT2 来支持输入数据的网格，从而将空间变异性引入作物建模中。然而，在这两种情况下，并发性都是在模拟器级别进行的，而不是在建模级别进行的，因此限制了模型的独立性。

其次，由于植物的生物性质，模型往往非常复杂，使得手动验证和属性检查变得困难。这种复杂性也使得它们的实现具有挑战性，需要额外的测试和验证来保证其正确性和与原始模型的等效性。软件的可移植性也可能成为一个问题，可能会影响模型的可用性。一个直接的解决方案是在需要时以所需的格式或编程语言（从模型描述）重新实现程序；然而，这类模型大多由一组方程描述，通常分阶段描述，配以系统行为的自然语言描述和关系图（也称为 Forrester 图，Forrester，1961），这些图表示系统状态变量之间的流动和相关性（Zadoks，1971）。然而，这使得这些描述容易产生歧义解释，从而导致实现错误。另一种选择是，一些模型可能已经带有可用于模拟的实现模块，但这严重限制了用户采用特定框架的能力，或者提供了无法适应的黑盒模型（Donatelli 和 Rizzoli，2008）。出于这些原因，一些研究人员提出了与平台无关的框架，旨在提高农学模型的通用性和可重用性。其中，Villa 等人（2006）和 Midingoyi 等人（2021）都使用 XML 开发了一种通用语言来描述模型：Villa 等人认为 XML 模型可以自动转换为模拟代码，从而消除了可能引入解释错误的人为因素，而 Midingoyi 等人开发了一个建模框架，该框架通过集中式的基于过程的模型（PBM）组件仓库将模型组件存储在标准格式中，以便在不同的作物建模平台之间访问和重用。最后，Donatelli 和 Rizzoli（2008）提出了一种更像编程的方法，使用类、接口和 API 来创建和连接模型的组件。

在工业领域，制造系统经常使用正式模型来描述，例如混合自动机（Alur 等，1993），或离散化变体，如有限状态机和自动机（FSM 或 FSA）（Strelec 等，2022）以及佩特里网（Latorre-Biel 等，2018），这些都非常适合应用数字孪生解决方案。这些形式主义基于精确的语法，允许人类和机器对其行为进行无歧义的解释，并提供了许多自动化操作，这得益于超过六十年的规范、分析、合成和属性检查研究。特别是，这些形式主义支持基于组件的设计，通过定义同步和并行组合来实现，允许在运行时模拟不同子模型的组合而无需合并它们，或构建它们的单体静态版本。相关的许多研究属于监督控制（Ramadge 和 Wonham，1989）的范畴，该研究解决了合成控制器的问题，如果存在控制器的话，该控制器可以限制系统的行为以满足给定要求。许多软件库支持使用离散和混合自动机进行建模。其中，我们提到了 ESCET（Fokkink 等，2023）、Supremica（Akesson 等，2006）、MDESpos（Meira-Góes 等，2023）、UPPAAL（Larsen 等，1995）和 Ariadne（Benvenuti 等，2014）；IEEE 控制系统协会的仓库提供了详尽的列表，以及 Reniers 和 van de Mortel-Fronczak（2018）的综述论文。

本文提出了一种基于正式模型的新型作物建模方法，旨在解决上述问题。特别是，我们介绍了自动机形式主义，它涵盖了多个抽象和复杂性层次，并允许在同一框架内创建从简单到复杂的模型，上述提到的自动工具可用于对这些模型进行属性检查。要检查的属性包括可达性，它计算系统演化过程中可达到的所有状态集合；吸引性，它确定系统是否自然地收敛到特定状态；不变性，它评估系统是否仅在有限的状态集合内演化而永远不会离开该集合；可行性，它确定系统的状态是否可以无限期地保持在“可行性集合”内，意味着总是存在一种可能的演化路径通向该集合内的状态；活跃性和安全性，它们确定是否最终可以达到某个目标状态（也表述为“好事将会发生”）以及系统是否永远不会进入不希望的状态（也表述为“永远不会发生坏事”）。关于这一主题的深入讨论，请参考 Abate 等人（2009）、Benvenuti 等人（2014）或 Nuzzo 等人（2015）的研究。

自动机非常适合表示作物模型，因为这些模型通常根据植物的动态将生命周期划分为不同的阶段，或将方程分成不同的情况来描述在变化条件下的不同行为（如 Zhu 等人（2024））。在这两种情况下，这些转换自然地映射到自动机上，每个状态的变化都代表了系统演化的转变，无论是从分析角度还是逻辑角度。在所有自动机类别中，我们选择了 Stauner（2002）提出的离散时间混合自动机（DTHA）形式主义，因为它能够将生长阶段和方程情况轻松映射到状态，并且仅限于离散时间动态，因为许多传统的作物模型都是如此，因为它们遵循离散演化或需要离散时间输入，因此在时间上是离散的。这样的模型示例包括用于番茄的 TOMGRO（Jones 等人，1991）、用于玉米的 CSM-CERES-Maize（Birhan 等人，2025）以及一些版本的 VegSyst（Gallardo 等人，2016），这些模型都将生长划分为不同的阶段，并具有相关的方程，并根据输入要求在离散步骤上工作。这些模型可以很容易地表示为 DTHA，而无需重新考虑底层方程，因为唯一需要的任务是识别和分离植物模型的各种状态。然而，值得注意的是，对于那些 DTHA 不够充分的更通用植物模型，仍然可以使用更具表达力的混合自动机（HA）形式主义进行建模，DTHA 只是 HA 的一个小子集。HA 在生物学领域的应用并不是全新的，参见 Casagrande 等人（2008）和 Alfieri 等人（2011）的研究；相反，HA 在农学中的应用尚未被报道。

具体来说，我们使用 Jones（Jones 等人，1999）提出的著名番茄作物模型 TOMGRO 作为案例研究，将其完全形式化为 DTHA，并强调模块化。结果，我们定义了三个独立的自动机来实现不同的子模型，其组合行为与原始系统相同。接下来，使用 ESCET 工具，我们通过组合多个相同的自动机实例来描述多种植物场景，每个实例代表一株番茄植物，仅基于设置的正式描述。最后，使用 ESCET 的功能，我们自动生成了一个可执行程序来实现我们的群体场景，从而确保了正确性。请注意，只要农业文献中有相关模型的可用性，并使用任何支持从 DTHA 形式主义生成代码的其他工具，就可以对不同类型的作物进行相同的操作。

总之，本文提出了以下贡献：
- 一种使用 DTHA 的新型作物建模方法，讨论了采用这种形式主义的好处。
- 重新制定了简化的 TOMGRO 模型，将其表示为具有有限差分方程的离散事件系统，分解为三个可以组合以获得完整模型的独立自动机。
- 一种用于构建在异质条件下生长的植物群体模型的方法，并自动推导实现它们的源代码。
- 一个用例场景，用于评估所提出解决方案的时间可扩展性。

本文的结构如下。第2节介绍了 TOMGRO 番茄植物模型、DTHA 自动机形式主义、自动机的同步和组合形式主义以及 ESCET 库。第3节通过组合三个自动机重新制定了传统的 TOMGRO 模型，并描述了从组合的自动机自动生成模拟植物群体生长的可执行程序所需的所有步骤。第4节和第5节展示了植物群体网格模拟的结果，并特别讨论了代码生成性能和模拟时间。最后，第6节得出了结论并指出了未来工作的方向。该模型将番茄生长过程划分为十个不同的阶段或年龄类别，并为每个阶段分配了相应的变量以跟踪其发展情况（Keulen和Dayan，1993年）：叶片数量、茎节数量、果实数量、叶片干重、茎节干重、果实干重。模型适应性和形式化方面，所提出的DTHA实现了简化的TOMGRO模型。然而，为了充分利用自动机的组合特性，我们将模型拆分为其核心组成部分，并为每个组成部分分别开发了专用的自动机，从而避免了使用单个自动机描述整个系统时可能导致的状态空间爆炸问题。将模型转换为基于离散变量的形式的第一步是重新编写代码，这使得后续转换更加直接。

第三节中描述的完整流程在图6中进行了示意，该流程被实现为一个单一的执行脚本，按顺序执行各个步骤，仅需输入网格尺寸即可。此外，该脚本还监控计算资源的使用情况，特别是代码生成和仿真时间，以提供对所提方法可扩展性的定量评估。这一解决方案通过模拟不同种植数量的植物场景（9株、25株、100株）进行了测试。

我们能够对生长在异质微气候条件下的多株植物实例进行建模和仿真，因为我们的模型被形式化为DTHA（离散时间混合自动机），这是HA（混合自动机）的一种特殊情况。在实际应用中，我们主要使用了ESCET提供的模板功能和自动代码生成工具来实现模型的构建和仿真。我们的方法能够轻松地适应TOMGRO模型，并将其转换为DTHA形式，因为我们的形式化方法本身就支持这种转换。

本文提出了一种自动化作物模型开发的方法，应用了计算机科学和系统工程的方法论，使用离散时间混合自动机（DTHA）对TOMGRO番茄作物模型进行了形式化处理，认为这种形式化方式能够清晰且独立于具体实现方式地表示作物动态。利用这种方法，我们开发了包含多株植物实例的大规模模型，并能够考虑不同的气候输入条件。

对于未来的研究工作，建议将所提出的方法扩展到其他作物模型，目标是构建一个可用的形式化模型库，并在此基础上合成能够根据气候和土壤变量优化作物生长的控制器。进一步的扩展方向包括将植物模型与病原体或昆虫模型相结合，研究它们之间的相互作用，并制定保护作物的策略。最后，另一个研究目标是改进模型的准确性。

作者贡献声明：
Elia Brentarolli：负责撰写初稿、验证和软件开发。
Davide Quaglia：负责撰写、审稿和编辑、调研及概念化。
Luca Benvenuti：负责撰写、审稿和编辑、监督及方法论指导。
Tiziano Villa：负责撰写、审稿和编辑、监督、项目管理和方法论指导。
Daniele Massa：负责撰写、审稿和编辑、数据整理。
Piero Battista：负责撰写、审稿和编辑、数据整理。
Bernardo Rapi：负责撰写、审稿和编辑、数据整理。

伦理声明：
作者声明本研究不涉及人类或动物的实验。

利益冲突声明：
作者声明不存在可能影响本文研究结果的已知财务利益或个人关系。

致谢：
本研究得到了Veneto地区政府在PR FESR 2021–2027计划Action 1.1.1项目下的资助，该项目属于“AGRIFUTURE”计划的一部分，旨在支持Veneto地区农业食品企业的竞争力发展（项目编号：ID 24279_001587_04499230235）。Tiziano Villa还得到了INdAM - GNCS项目（项目编号：CUP: E53C25002010001）的部分资助。资助方未对研究过程产生任何影响。

作者列表：
Elia Brentarolli | Davide Quaglia | Luca Benvenuti | Tiziano Villa | Daniele Massa | Piero Battista | Bernardo Rapi | Luca Incrocci