一种针对LTL的最优凝结算法 [ X, F ] 和 LTL [ X, G ]

《Artificial Intelligence》：An optimal pastification algorithm for LTL [ X , F ] and LTL [ X , G ]

　　亚历山德罗·阿塔莱|卢卡·盖亚蒂|尼古拉·吉甘特|亚历西奥·曼苏蒂|安德里亚·马祖洛|安杰洛·蒙塔纳里
博尔扎诺自由大学，Piazza Università, 1, 博尔扎诺, 39100, 意大利

**摘要**
我们研究了线性时序逻辑（LTL）的一个片段，该片段包含了“明天”（X）和“最终”（F）这两种时态模态，并为该片段中的“过去化”问题提出了一种单指数时间复杂度的算法。“过去化”问题是指对于给定的LTL公式，构造一个仅使用过去时态运算符的等价公式。尽管在完整的LTL以及所考虑的片段中，最著名的算法其时间复杂度为三指数级别，但我们的方法实现了这一片段的最优时间复杂度。

所提出的算法分为两个主要阶段：
(i) 首先将输入公式转换为定制的规范形式；
(ii) 然后从规范形式派生的树状结构中合成一个纯过去时态的公式。经过少量调整，该算法可以扩展到处理包含“明天”和“全局”时态模态的LTL片段。

我们在时序推理工具BLACK中实现了该算法，并报告了对其性能的实验评估结果。

**1. 引言**
线性时序逻辑（LTL）[2]通过引入未来时态模态，扩展了命题逻辑，从而能够处理具有最小元素的无限离散线性结构。结合其包含过去时态模态的扩展LTL+P [3]及其有限变体LTLf [4]（其中公式在有限轨迹上解释），线性时序逻辑已被证明是许多领域（包括形式验证、自动推理和知识表示）中的重要工具。在本文中，我们关注LTL+P的纯过去时态片段，记为pLTL [3],[5]。这个片段被定义为排除所有未来时态模态的LTL+P公式集合。由于仅包含过去时态模态，pLTL的公式自然可以在有限轨迹上解释。

近年来，由于pLTL具有良好的理论和算法特性，它再次受到了关注。
在表达能力方面，pLTL与LTLf [3]等价，尽管其中一个可能比另一个更简洁（反之亦然）[6],[7]。此外，pLTL与LTL的安全性和安全性片段密切相关[8]。前者，记为SafetyLTL，描述的是“永远不会发生坏事”的性质；后者，记为coSafetyLTL，描述的是“最终会发生好事”的性质。SafetyLTL包含所有处于否定规范形式且时态模态为普遍性（ tomorrow (X)）、全局性（G）和释放（R）的LTL公式。SafetyLTL（或coSafetyLTL）的关键特点是，一个无限轨迹的有限前缀就足以确定整个轨迹是否是该公式的模型。这使得这两个片段可以转换为pLTL框架。

设F(pLTL)为定义如下形式的公式集：F(α)，其中F表示“最终”模态（“未来某个时间点存在”），α是pLTL公式。F(pLTL)中的公式表明存在某个未来时间点，使得该时间点之前的轨迹满足α。已经证明F(pLTL)在表达能力上与coSafetyLTL等价[8]。同样，G(pLTL)中的公式表明存在某个未来时间点，使得该时间点之后的轨迹满足α。在这些公式中，全局性模态G强制无限轨迹的每个前缀都必须满足α。

在算法属性方面，pLTL公式可以编译为单指数大小的确定性有限自动机（DFA）[5],[9]。这与完整的LTLf不同，后者可能具有双指数大小的DFA。这种“单指数差距”在监控、规划和反应式合成问题中依然存在[10],[11],[12]。例如，最近有研究表明pLTL规范的反应式合成问题是EXPTIME完全的[13]，而在LTL和LTLf中该问题是EXPTIME完全的[14],[15]。

鉴于pLTL的表达能力和算法特性，将coSafetyLTL、SafetyLTL和LTLf片段转换为F(pLTL)、G(pLTL)和pLTL等价片段的研究正受到越来越多的关注。这种转换属于一种称为“过去化”的过程。可以用最多两个嵌套时态模态的LTLf公式表示的规划模式可以轻松地“过去化”为规模为原始公式多项式的公式。这些模式包括所有可以在DECLARE [16],[17]中表示的模式，以及PDDL [11]中的轨迹约束。对于仅包含“明天”时态模态的LTL片段[18],[19]（以下记为LTL[X]），也有类似的多项式时间转换方法。

除了上述两个例子外，设计最优的过去化过程通常是一项非常具有挑战性的任务。目前已知的最佳算法将coSafetyLTL、SafetyLTL和LTLf公式转换得到的纯过去时态公式，其大小仍然是输入公式的三指数级别[5]。这一结果与前述的计算问题复杂度中的“单指数差距”相矛盾；从这种差距可以合理推测存在一种能够生成指数大小公式的过去化过程。这也与已知的coSafetyLTL和SafetyLTL过去化的最低界限相匹配，即单指数级别[7]。

目前，对于这些逻辑的自然片段，尚不存在其他替代的过去化算法。因此，一旦输入公式超出已知多项式大小转换的有限片段范围，就必须使用通用的三指数过程。

**我们的贡献**
在本文中，我们主要关注LTL[X,F]（仅包含“明天”（X）和“最终”（F）时态模态的LTL片段）以及F(pLTL[Y,Y?,O]（允许使用“昨天”（Y）、“弱昨天”（wY）和“曾经”（O）时态模态的F(pLTL)片段）。LTL[X,F]和F(pLTL[Y,Y?,O]片段属于LTL或LTL+P的安全性片段，因为它们只能表达安全性性质。此外，我们还研究了这些片段的“通用”对应形式，即LTL[X,G]（仅包含“明天”（X）和“总是”（G）时态模态的LTL片段），以及G(pLTL[Y,Y?,H]（只允许使用“昨天”（Y）、“弱昨天”（wY）和“历史上”（H）时态模态的F(pLTL)片段）。所谓“对应形式”，是指一种语言在LTL[X,F]（或F(pLTL[Y,Y?,O]）中可表达当且仅当其补语言在LTL[X,G]（或G(pLTL[Y,Y?,H]）中可表达）。LTL[X,G]和G(pLTL[Y,Y?,H]片段属于安全性片段，因为它们只能表达安全性性质。

我们为LTL[X,F]到F(pLTL[Y,Y?,O]的转换设计了一种单指数时间的过去化算法，该算法将前者片段的公式转换为后者的等价公式。
该过程主要包括两个主要步骤：
1. 将输入的LTL[X,F]公式?转换为适当定义的规范形式，其大小在最坏情况下为?的大小的指数级。这一步涉及基于逻辑恒等式的重写规则的自下而上的应用。
2. 对于任何处于规范形式的公式，构建一个依赖树，表示F模态作用下子公式之间的时间关系。从这个树中提取一个F(pLTL)公式，该公式与原始公式等价，且其大小最多为前一步所得公式大小的二次方。
作为输出的F(pLTL[Y,Y?,O]公式处于否定规范形式，并且不包含“直到”（U）的过去对应模态S。S的缺失与[7]中的结果一致，表明F(pLTL[Y,Y?,O)在表达能力上与LTL[X,F]等价。由于F和G模态的对偶性，可以很容易地从所提出的算法中获得LTL[X,G]到G(pLTL[Y,Y?,H]的单指数过去化过程。

算法的运行时间为2O(n)，其中n是输入公式的大小。在[20]中表明，LTL[X,F]在表达能力上可能比F(pLTL[Y,Y?,O]更简洁。更准确地说，存在无限多个公式序列?1,?2,...，对于每个k≥1，公式?k的大小为k，并且只能使用大小为2Ω(k)的公式在F(pLTL[Y,Y?,O]中表示。这意味着过去化问题有一个2Ω(n)的上界，从而证明了所提算法的最优性。

我们在时序推理工具BLACK [21],[22]中实现了该算法。由于算法主要基于恒等式驱动，实现代码仅约500行。我们提供了实验评估，比较了输入公式与BLACK生成的相应F(pLTL)公式在公式大小和时态模态数量等不同参数方面的性能。

本文是对[1]的大幅修订和扩展版本，[1]最初发表在KR 2023会议论文集中。除了提供所有结果的完整证明（这些证明在会议论文中未包含外，本文还对原始算法进行了简化，并对其复杂性进行了更详细的分析，证明了上述的2O(n)运行时间上界（会议论文仅建立了2O(n2)的上界）。鉴于[20]中最近给出的2Ω(n)下界（该下界在会议论文发表之后才出现），对复杂性进行分析的细化对于证明算法的最优性至关重要。

**论文大纲**
第2节回顾了相关先前的工作和过去化问题。第3节介绍了LTL所需的背景知识。第4节介绍了将LTL公式转换为规范形式的过程及其计算复杂性分析。第5节介绍了依赖树的概念，并详细说明了转换为纯过去时态公式的方法。第6节完成了整个过程的复杂性分析，证明了其最优性。第7节报告了实现的实验评估结果。最后，第8节讨论了未来研究的可能方向。

**2. 相关工作**
2.1. LTL[X,F]及相关片段
在[23, Theorem 3.7]中，Sistla和Clarke证明LTL[X,F]的可满足性问题（即检查公式的语言是否为空）是NP完全的，而Markey在[24, Theorem 28]中证明了LTL[X,G]的相同问题是PSPACE完全的。
在表达能力方面，[7]研究了LTL[X,F]和F(pLTL[Y,Y?,O])以及相应的LTL[X,G]和G(pLTL[Y,Y?,H])的确切表达能力。特别是，LTL[X,F]和F(pLTL[Y,Y?,O])被证明在表达能力上是等价的，意味着一个语言如果能由前者片段的公式定义，则也能由后者片段的公式定义；LTL[X,G]和G(pLTL[Y,Y?,H]也是如此。此外，还证明在LTL[X,F]中可表达的语言恰好是那些在伪停顿下封闭的语言，即每个单词都包含有限数量的位置，如果在这些位置之外插入任意符号，得到的单词仍然属于该语言。最后，可以在LTL[X,F]中定义的语言严格包含在LTL中可定义的安全性语言集合中：存在一些在LTL[X,F]中可定义但在LTL[X,G]中无法定义的安全性（或安全性）性质[7]。

关于这些片段的简洁性，如引言中已经提到的，在[7]中证明LTL[X,F]在表达能力上可能比F(pLTL[Y,Y?,O]更简洁；而在[20]中又证明了相反的情况，这意味着LTL[X,F]和F(pLTL[Y,Y?,O]在简洁性方面是不可比较的（简洁性的正式定义将在第6节给出）。此外，同样的不可比较性结果也适用于LTL[X,G]和G(pLTL[Y,Y?,H]片段。正如我们在引言中指出的，上述讨论的结果，加上本文建立的单指数化LTL[X,F]到F(pLTL[Y,Y?,O])的机制，表明LTL[X,F]相对于F(pLTL[Y,Y?,O])的简洁性的指数界限是紧的，即至少存在这样一种语言：(i)它可以用LTL[X,F]的公式来定义；(ii)任何定义它的F(pLTL[Y,Y?,O]的公式其复杂度最多也是指数的。同样的结论也适用于逻辑LTL[X,G]和G(pLTL[Y,Y?,H])。

2.2. 凝固化、可分性与回到未来
在[25, Theorem 2.1]中证明了LTL+P和LTL的表达等价性，这表明过去的时间模态可以被消除，转而使用仅关注未来的逻辑。这一结果与本文考虑的凝固化过程的方向相反。此外，[26, Theorem 3.1]提供的简洁性结果为这种过程给出了一个（单）指数上的下界。然而，对于这种“未来化”方向，文献中最好的方法在公式复杂度上是三指数的[5]，因此仍然存在一个紧密的复杂性结果的问题。这与本文考虑的片段的凝固化过程形成对比，后者提供了一个紧密的单指数界限。

2.3. 凝固化与DFA构建的比较
有人可能会怀疑，将时间逻辑公式（例如LTL[X,F]公式）转换为DFA，而不是进行凝固化，是否可能在实践中带来更好的方法。实际上，可以说，任何涉及对LTL[X,F]公式进行凝固化然后构建相应的DFA的问题（这将导致原始公式复杂度的双重指数增长）同样可以通过首先从LTL[X,F]公式生成NFA，然后再将其确定为DFA来解决。首先，我们指出，虽然研究LTL[X,F]公式编译成等价确定性自动机的复杂性（无论是有限词还是无限词，包括确定性Büchi自动机DBA）仍然是一个未解决的问题，但LTL[X,F]公式不太可能在单指数时间和空间内被编译成DFA或DBA。例如，由公式?i=1n(pi→XFpi)定义的语言就是一个例子。任何等价的DFA都必须跟踪在初始时间点为真的命题字母的所有可能性，以及它们在后续时间点可能再次出现的顺序。如果所有在初始状态下为真的命题字母的子集S?{p1,?,pn}有2n种选择，那么DFA需要维护与S的子集数量成比例的可能性数量，从而导致双重指数的复杂性。其次，我们想强调的是，即使对应于LTL[X,F]公式的DFA是双重指数的——与凝固化LTL[X,F]然后从得到的纯过去公式生成DFA的复杂性相匹配——凝固化作为一种工具本身仍然是有价值的。尽管在精神上有关联，但凝固化的结果与可分性的保证结果完全不同。实际上，凝固化并不要求在纯过去和纯未来成分之间做出明确的分割，而只是要求将纯过去成分封闭在纯未来的环境中。此外，Gabbay的著名分离定理[27] [28]将公式在给定时间逻辑中的可分性与表达完备性联系起来，即能够准确捕捉到后继函数的一阶理论中可定义的属性。该定理指出，一个时间逻辑是表达完备的当且仅当其中的每个公式都是可分的。相比之下，凝固化并不产生表达等价性的对应关系。最后，众所周知，从LTL+P公式有效计算出分离时间公式的算法是非基本的，而LTL+P的凝固化过程（在无限或有限轨迹上）最多是三指数的。

2.4. 对现有凝固化算法的进一步探讨
凝固化技术最初是与一种称为有界响应度量时间逻辑（MTL-B，简称）[19]的片段相关的。这种逻辑是在密集的线性序上解释的，时间模态有界，限制了它们的应用区间。例如，公式φU[a,b]ψ，其中a,b∈N以二进制形式给出，表示在时间t解释时，ψ必须在t+a和t+b之间的时间t′发生，并且在t和t′之间的时间间隔内?始终为真。在[18]、[19]中，Maler等人开发了一种用于MTL-B的凝固化算法，生成多项式大小的公式。该算法利用了这样一个事实：在MTL-B公式?的每个模型中，存在一个最远的时间点t之后，?不再对模型施加任何约束。该算法返回的公式：(i)仅使用过去模态；(ii)在|?|上是多项式的；(iii)在时间点t解释时等价于?，而不是在原点解释时。当在离散线性序上解释逻辑并表示所有时间界限（例如a和b）为一元而非二进制时，MTL-B等同于LTL[X]。因此，[18]、[19]中的算法也是LTL[X]的凝固化过程。

至于更具表达能力的逻辑coSafetyLTL和安全LTL，它们分别凝固化为G(pLTL)和F(pLTL)的最佳上界已经是三指数的[32]、[33]，正如引言中已经指出的。这种三指数的过程如下：
1. 从输入的coSafetyLTL公式?开始，构建最小的DFA A，该DFA识别?的所有良好前缀[34]。这些是无论如何扩展都能生成?模型的有限轨迹。在最坏的情况下，A的大小是?大小的双指数。
2. 将A分解为重置自动机的级联产品C[2]。这种分解基于著名的Krohn-Rhodes级联分解定理[35]，该定理将任何DFA分解为仅包含两种类型的自动机的级联：排列和重置。在无计数器的自动机[36]（如A）的情况下，只需重置自动机[32]。在最坏的情况下，C的大小是A的大小的指数级。
3. 构建一个纯过去的LTL公式ψ，该公式定义了C的语言。这一步使用了[33]中的算法。
4. ψ的大小是C的大小的多项式，根据构造，输入?等同于F(ψ)。
安全LTL的情况类似，只是良好前缀和不良前缀的角色相反。在这种背景下，不良前缀是一个有限轨迹，其任何扩展都会导致公式?的违反。

值得注意的是，尽管Krohn-Rhodes级联分解算法已有几十年的历史，但据我们所知，第二步中所需的实现仅有一个，而且没有实现coSafetyLTL和安全LTL的凝固化算法。这可能部分是由于该算法的高度技术性。我们选择设计一个完全基于重言式的算法，是为了获得一个易于实现和维护的解决方案。

3. 前言
在本节中，我们正式描述了我们考虑的逻辑的语法和语义，并阐述了凝固化的概念。
设AP是一个（可数的）命题字母集合。线性时间逻辑带过去（LTL+P）的公式?、ψ等是由以下语法构建的：
?::=?∣⊥∣p∣?p
true,false,
以及
literals∣?∨?∣?∧?
布尔连接词∣X
?∣F?∣?U?∣G?∣?R?
未来模态∣Y?∣wY?∣O?∣?S?∣H?∣?T?
其中p∈AP。未来模态X、F、U、G和R分别称为明天、最终、直到、全局和释放。过去模态分别是昨天（Y）、弱昨天（wY）、一次（O）、曾经（S）、历史上（H）和触发（T）。注意，上述语法中的公式都是否定范式（NNF），即否定仅应用于命题字母。这是没有损失一般性的，因为语法在取时间运算符的对偶时是封闭的。实际上，根据即将介绍的语义，以下等价关系成立：
?F?≡G??;
?(?Uψ)≡(??)R?ψ;
?O?≡H??;
?(?Sψ)≡(??)T?ψ。
一个无限轨迹σ是状态σi的无限序列σ0σ1…，即σ属于(2AP)，也就是σ是(2AP)ω的元素。LTL+P公式?相对于轨迹σ和时间i∈N的满足性，表示为σ, i??，定义如下：
?σ, i??始终为真；
?σ, i?⊥始终为假；
?σ, i?piff p属于σi；
?σ, i??piff p不属于σi；
?σ, i??∨ψ iff ?σ, i?? 或 ?σ, i?ψ；
?σ, i??∧ψ iff ?σ, i?? 且 ?σ, i?ψ；
?σ, i?X? iff ?σ, i+1??；
?σ, i?F? iff 存在j≥i使得?σ,j??；
?σ, i?G? iff 对所有j≥i都有?σ,j??；
?σ, i??Rψ iff 要么对于所有j≥i都有?σ,j?ψ，或者存在k≥i使得?σ,k?? 且对于所有i≤j≤k都有?σ,j?ψ；
?σ, i?Y? iff i>0 且 ?σ,i?1??；
?σ, i?wY? iff i=0 或 ?σ,i?1??；
?σ, i?O? iff 存在0≤j≤i使得?σ,j??；
?σ, i??Sψ iff 存在0≤j≤i使得?σ,j?? 且对于所有k≤j≤i都有?σ,k??；
?σ, i?H? iff 对所有0≤j≤i都有?σ,j??。
我们说σ是?的模型，表示为σ??。我们用L(?)表示?的语言，即?的所有模型集合。如果LTL+P中的两个公式?和ψ等价，记作??≡?ψ，那么L(?)=L(ψ)。在第4.2节中，我们将使用强等价的概念，该概念要求对于每个轨迹σ和属于它的每个时间点i，两个公式要么都满足，要么都违反。其正式定义如下：
**定义1**
两个公式?和ψ是强等价的，表示为??ψ，当且仅当对于每个σ∈(2AP)ω和每个k≥0，有σ, k??当且仅当σ, k?ψ。
请注意，在LTL+P的纯未来片段的情况下，等价和强等价的概念是一致的。相反，LTL+P公式p∨Yq和p是等价的例子（因为?σ,0?Yq当且仅当σ, 0?⊥），但不是强等价的。
在整篇文章中，给定n∈N，我们用Xn?表示归纳定义的公式，即X0?:=?且Xn+1?:=XXn?，并用Yn?和wYn?表示类似定义的公式，其中分别用Y和wY代替X。公式?∈LTL+P的大小，表示为size(?)，归纳定义如下：
size(?)=1，
size(⊥)=1，
size(p)=size(?p)，
size(??)=size(?)+1（对于?∈{X,F,G,Y,wY,O,H}），
size(?1⊕?2)=size(?1)+size(?2)+1（对于⊕∈{∨,∧,U,R,S,T}）。
纯未来（或纯过去）公式是LTL+P公式中没有出现过去（或未来）模态的公式。我们用LTL（或pLTL）表示纯未来（或纯过去）公式的集合。给定一个时间模态列表OP，我们用LTL[OP]（或pLTL[OP]）表示只使用OP中的时间模态的LTL（或pLTL）公式集合。例如，LTL[X,F]表示仅包含模态X和F的LTL片段。此外，我们用F(pLTL[OP])（或G(pLTL[OP])表示形式为F(α)（或G(α)）的公式集合，其中α属于pLTL[OP]。
最后，对于所有的k∈N，我们定义了k-指数过去化的概念。它指的是将给定LTL+P片段的公式转换为属于F(pLTL)或G(pLTL)的等价公式的任意过程。如果该过程始终输出的公式大小被输入公式大小的k次幂 Tower所限制，我们称其为k-指数的。
**定义2（k-指数过去化）**
给定一组LTL+P中的公式L和一组属于F(pLTL)或G(pLTL)的公式L′，一个k-指数大小的过去化过程是从L到L′的算法，对于任何?∈L，它返回一个与?等价的ψ∈L′，使得size(ψ)∈exp(k,O(size(?)))，其中exp(0, n)?n且exp(i+1,n):=2^exp(i,n)。
**定义2**使我们能够总结第2节中概述的内容：**存在一个0-指数过去化过程从LTL[X]到F(pLTL)和一个3-指数过程从coSafetyLTL到F(pLTL)（或从SafetyLTL到G(pLTL)）。**我们的主要结果是一个1-指数过去化过程从LTL[X,F]到F(pLTL[Y,Y?,O])。
**4. 规范化**
现在让我们描述提出的LTL[X,F]的过去化过程。在本节中，我们将说明该过程的第一步，该步骤将输入的LTL[X,F]公式转换为适当定义的标准形式。这种转换是由基于LTL[X,F]的重写规则指导的。
**4.1. LTL[X,F]的标准形式**
在提供正式定义之前，让我们解释一下我们将使用的标准形式背后的理由。以公式(为了可读性，我们使用?而不是∨)?:=F((p1?Fq1)∧(p2?Fq2))为例，其中对于i=1,2，pi和qi都属于AP。想象为?构建一个模型。首先要做的选择是确定在满足公式(p1?Fq1)∧(p2?Fq2)的轨迹状态中哪些（如果有的话）原子字母p1和p2为真。假设p1和p2都被设置为真。之后，第二个选择是确定何时（以及以什么顺序）满足字母q1和q2。该公式对此没有时间依赖性，因此q1在q2之前或之后，或者在轨迹的同一状态下使q1和q2都为真都是可接受的解决方案。四种可能的模型示例是：
?{p1,p2}
?{q1}
?{q2}
?{p1,p2}
?{q1,q2}
?{p2}
?{q2}
?{p1,q1}
?
我们的标准形式旨在“移动”在公式的顶层选择满足哪些子公式，同时保持关于何时满足子公式的时间依赖性。在我们的例子中，这很简单：将Fqi视为原子命题，我们首先将公式(p1?Fq1)∧(p2?Fq2)转换为析取标准形式（DNF），然后将最顶层的F分配到析取的范围之内。结果是
F(?p1∧?p2)∨F(?p2∧Fq1)∨F(?p1∧Fq2)∨F(Fq1∧Fq2)。
我们看到这个公式的每个析取项都明确了必须满足哪个子公式p1、p2、Fq1和Fq2，同时保持q1和q2之间（不存在的）时间依赖性。
**转向正式定义**，我们的标准形式是一个“双层”标准形式。内层断言由模态F给出的时间依赖性：
**定义3 标准形式的内层**
我们用conj(F,pLTL[Y])表示由语法?::=ψ|?∧?|F?生成的公式集合，其中ψ来自逻辑pLTL[Y]。
外层则猜测哪些子公式应该被满足：
**定义4 (LTL[X,F]的标准形式)**
我们用nf(LTL[X,F])表示所有形式为Xk?i=1c?i的公式集合，其中k,c∈N，并且每个?i都属于conj(F,pLTL[Y])。
**4.2. 将LTL[X,F]转换为nf(LTL[X,F])**
LTL[X,F]到nf(LTL[X,F]的转换包括应用六个重写规则??ψ（R1–R6）。值得注意的是，每个规则??ψ将应用于输入公式的任意子公式。因此，?和ψ不仅需要等价，它们还需要强等价（定义1），即在轨迹的任何点进行解释时都等价。R4是一个例外，它处理的是由规则R1引入的“昨天”模态Y：该规则中的公式仅在假设k≥1的情况下等价（规范化过程——算法1——将仅在此约束下使用此规则）。此外，回想一下，在LTL+P的纯未来片段的情况下，等价和强等价的概念是一致的。然而，nf(LTL[X,F])中的公式包含“昨天”模态Y，因此需要做出这种区分。
**下载：** 下载高分辨率图像（147KB）
**下载：** 下载全尺寸图像
**算法1. NF(?)**：将LTL[X,F]公式转换为标准形式的算法。
以下是规则R1–R6的列表，以及它们在规范化过程中作用的非正式描述：
R1: Xi?1?Xj?2?Xj(Yj?i?1??2)，其中i≤j, j≥1, ?∈{∧, ∨}；
R2: FX??XF?[
R1和R2的作用是将模态X置于公式的最顶层，遵循标准形式的“外层”（见定义4）；
R3: Y(?1??2)?Y?1?Y?2，其中?∈{∧, ∨}；
R4: YF??FY?；[
R3和R4的作用是将模态Y推到不在该模态范围内的位置（如定义3所述）；
R5: F(?1∨?2)?(F?1)∨(F?2)；
R6: (?1∨?2)∧?3?(?1∧?3)∨(?2∧?3)[
R5和R6的作用是将F和∧推到∨的范围内，从而在标准形式的“外层”创建析取（见定义4），其中?,?1,?2,?3∈LTL[X,F,Y]。
我们假设有一个交换合取项和析取项的规则。此规则仅用于当Xi?1?Xj?2（其中i≥j）时应用规则R1，以及当?3∧(?1∨?2)时应用规则R6。
下面的引理说明了这六个规则的正确性。
**引理1**
对于R1–R6中的每个规则??ψ（R4除外），我们有??ψ。
**证明**
R5和R6的证明很直接（实际上，后者是命题逻辑的标准重写）。我们只证明剩余规则的双重等价性。设σ∈(2AP)ω和k≥0。下文中，我们稍微滥用符号，将∧和∨既作为LTL+P的结构，也作为我们用于形式化证明的元语言中的符号。
**R1的证明：** 对于i≤j和?∈{∧, ∨}，我们有：
??????σ,k?Xi?1?Xj?2 iff (σ,k+i??1)?(σ,k+j??2) iff (σ,k+j?(j?i)??1)?(σ,k+j??2) iff σ,k+j?Yj?i?1??2) iff σ,k?Xj(Yj?i?1??2)。
**R2的证明：**
?????σ,k?FX? iff σ,h?X? 对于某些h≥k
iff σ,h+1?? 对于某些h≥k
iff σ,h?? 对于某些h≥k+1
iff σ,k+1?F? iff σ,k?XF?。
**R3的证明：** 对于?∈{∧, ∨}，我们有：
????σ,k?Y(?1??2) iff σ,k?1??1??2
且k>0 iff (σ,k?1??1)?(σ,k?1??2)，
且k>0 iff σ,k?Y?1?Y?2。
□
**引理2**
R4中的公式在轨迹的所有位置上都是等价的，除了第一个位置，即?σ,k+1?YF?当且仅当?σ,k+1?FY?，对于每个轨迹σ∈(2AP)ω和k≥0。
**证明**
?????[t]σ,k+1?YF? iff σ,k?F? iff σ,h?? 对于某些h≥k
iff σ,h+1?Y? 对于某些h≥k
iff σ,h′?Y? 对于某些h′≥k+1
iff σ,k+1?FY?。
□
**算法1**指定了规则R1–R6的执行策略，以将输入的LTL[X,F]公式转换为标准形式。伪代码中的注释突出显示了每个规则的使用位置。算法调用pushY(Yjψ)过程，其中ψ是conj(F,pLTL[Y])中的公式。当j≥1时，pushY(Yjψ)过程通过迭代规则R3和R4从Yjψ返回conj(F,pLTL[Y])中的公式；当j=0时，它返回输入公式ψ。注意，当j≥1时，算法构建的公式pushY(Yjψ)随后被放置在至少j+1个嵌套模态X的范围之内（第9行和第10行）。根据引理2，这证明了使用规则R4的合理性。
**命题1 算法1的正确性**
对于每个输入的LTL[X,F]公式?，算法1返回一个nf(LTL[X,F])中的公式γ，使得γ≡?。
**证明**
算法的终止是直接的：每次递归调用NF(·)的输入都是输入的一个适当子公式。输出公式γ属于nf(LTL[X,F])且?≡γ的证明是通过?的结构归纳得到的：
**基本情况：** ?∈conj(F,pLTL[Y])。我们有γ=?（第1行）。显然，γ≡?，并且γ属于conj(F,pLTL[Y])，这是nf(LTL[X,F])的一个子集。
**归纳步骤：** ?=X(ψ)。我们有γ=X(NF(ψ))（第2行）。根据归纳假设，NF(ψ)≡?，因此γ≡?。此外，NF(ψ)属于nf(LTL[X,F])。因此，根据定义4，γ也满足条件。
**归纳步骤：** ?=F(ψ)。根据归纳假设，NF(ψ)=Xk?i=1dψi，其中每个ψi都属于conj(F,pLTL[Y])。算法的输出是公式γ=Xk?i=1dFψi（第5行），根据定义4，γ属于nf(LTL[X,F])。因此，NF(ψ)≡?，从而?≡F(NF(ψ))。所以，?≡γ。
**归纳步骤：** ?=?1??2，其中?∈{∨, ∧}。根据归纳假设，NF(?i)=Xki?j=1diψi,j，其中每个ψi,j属于conj(F,pLTL[Y])且i∈{1, 2}。假设k1≤k2（k2≤k1的情况类似）。我们有：
?≡(Xk1?j=1d1ψ1,j)?(Xk2?j=1d2ψ2,j)（根据归纳假设）
≡Xk2((Yk2?k1?j=1d1ψ1,j)?(?j=1d2ψ2,j)（根据规则R1）
≡Xk2((?j=1d1Yk2?k1ψ1,j)?(?j=1d2ψ2,j)（根据规则R5）
≡Xk2((?j=1d1pushY(Yk2?k1ψ1,j))?(?j=1d2ψ2,j)（根据规则R6）。
其中最后一个等式在k1=k2时是显而易见的，否则根据引理2通过迭代应用规则R3和R4得到。现在，如果?代表∨，则最后一个公式等于输出公式γ（见第9行）。如果?代表∧，则这个公式仍然等同于γ（见第10行），通过迭代应用规则R6得到。最后，通过观察pushY(Yk2?k1ψ1,j)生成了conj(F,pLTL[Y])中的公式，我们得出NF(?)属于nf(LTL[X,F])。 □
**4.3. 算法1的复杂性分析**
我们展示了算法1返回的公式大小为2^O(size(?))，其中?是输入的LTL[X,F]公式。对于分析，我们依赖三个参数：
1. sizeY(ψ)，其中ψ来自conj(F,pLTL[Y])。这是ψ中不包含模态F的任何子公式的最大大小。
2. sizeF(ψ)，其中ψ来自conj(F,pLTL[Y])。这是通过用?替换ψ中不包含模态F的所有最大子公式得到的公式大小。
3. R(?)，其中?来自LTL[X,F]。这个量度的是DNF转换表达式的子句数量，定义如下：
R(χ):=1 对于χ∈{?,⊥,p,?p|p∈AP}
R(?1∧?2):=R(?1)·R(?2)
R(?1∨?2):=R(?1)+R(?2)
R(⊕?′):=R(?′) 对于⊕∈{X,F}。
根据定义，我们有size(?)≤sizeF(ψ)·sizeY(ψ)，对于conj(F,pLTL[Y])中的每个公式ψ，以及R(?)≤2size(?)，对于LTL[X,F]中的每个公式?。
**引理3**
考虑LTL[X,F]中的一个公式?，并设NF(?)=Xj?i=最后，d1·d2≤R(?1)·R(?2)=R(?)。□ NF(?)的大小上限为2O(size(?))，如下所示：命题2 算法1的输出大小对于LTL[X,F]中的每个公式?，NF(?)的大小为2O(size(?))。证明设NF(?)=Xj?i=1cψi。*** 根据引理3，j≤size(?)，c≤R(?)≤2size(?)，且对于每个i∈[1, c)，都有sizeF(ψi)≤size(?)和sizeY(ψi)≤size(?)+j。那么，size(NF(?))=j+∑i=1csize(ψi)≤j+c·max{size(ψi):1≤i≤c}≤j+c·max{sizeF(ψi)·sizeY(ψi):1≤i≤c}≤j+c·size(?)·(size(?)+j)≤size(?)+2size(?)+1·size(?)2∈2O(size(?))。□ 注1 算法1的复杂性命题2表明算法1的运行时间为2O(size(?))。实际上，NF过程递归地应用于输入公式?的所有子公式；总共有size(?)次调用。根据命题2，所有递归调用的输出大小为2O(size(?))，而该过程仅对该输出执行多项式时间操作。由于poly(2O(n))=2O(n)，因此总运行时间为2O(size(?))。5. 转换到F(pLTL[Y,Y?,O]) 甜蜜化算法的第二步将(nf(LTL[X,F])公式(在多项式时间内)转换为F(pLTL[Y,Y?,O])公式。为了更好地解释转换背后的想法，我们首先定义依赖树的概念，它是一种简单的conj(F,pLTL[Y])公式表示方法，用于突出模态F的各种出现之间的相互作用。接下来，我们将展示如何从这些树开始对conj(F,pLTL[Y])公式进行甜蜜化处理，然后将其扩展到任意的nf(LTL[X,F])公式。5.1. 依赖树考虑一个属于conj(F,pLTL[Y])的公式?。回想一下，这样的公式形式为ψ∧F(?1)∧?∧F(?n)，其中ψ属于pLTL[Y]，每个?i都属于conj(F,pLTL[Y])（且n∈N）。那么，公式?可以用一种直观的方式表示为树：在这样的树中，根节点标记为ψ，并且有n个子节点，以第i个子节点为根的子树（递归地）表示公式?i。以下是正式定义：定义5 依赖树公式?∈conj(F,pLTL[Y])的依赖树T是一个元组(V, E, r, μ, ν)，其中(V, E, r)是一个具有节点V、边E和根r∈V的有根树，μ:V→conj(F,pLTL[Y])和ν:V→pLTL[Y]是满足以下两个属性的标记函数：(i) μ(r)=? 和 (ii) 对于每个v∈V，μ(v)=ψ∧F(?1)∧?∧F(?n)（其中ψ∈pLTL[Y]，n∈N，且每个?i都属于conj(F,pLTL[Y)）当且仅当ν(v)=ψ且v的子节点集合为E(v)={v1,?,vn}，其中μ(vi)=?i对于每个i∈[1, n]。图1显示了一个依赖树的例子。注意，当上下文中?明确时，T(?)的缩写为T。我们用Π(T)表示从根到T的叶子的路径集合，即序列π=〈π1,…,πn〉中的V中的节点，满足(i) π1=r，(ii) 对于每个i∈[1,n?1]，πi+1∈E(πi)，以及(iii) E(πn)=?。下载：下载高分辨率图像（36KB）下载：下载全尺寸图像图1. 公式?:=p∧F(p∧F(YYr∧F(s∨Yq))∧F(Yq∧p)的依赖树T(?)。为了清晰起见，仅显示了标记函数ν。5.2. 从依赖树到F(pLTL[Y,Y?,O])考虑来自nf(LTL[X,F])的公式Xk?i=1c?i，其中k,c∈N，且每个?i都属于conj(F,pLTL[Y])。给定i∈[1, c]，我们的目标现在是利用依赖树T(?i)构造一个纯过去式公式ψik，该公式在任何轨迹的第k个时间点都等价于?i（由于k个模态X出现在?i=1c?i之前，这与我们相关）。简而言之，想法是分别考虑Π(T(?i))中的每条路径，并通过仅使用过去式模态O、昨天(Y)和弱昨天(wY)的公式“逆向重写”它（即从叶子到根）。特别是，弱昨天模态用于描述T(?i)根节点的属性，因为atk:=Zk+1⊥∧Yk?公式仅在轨迹的第k个时间点为真。以下是正式的转换定义：定义6 路径公式设?是conj(F,pLTL[Y])中的一个公式，k∈N。此外，设π=〈π1,?,πn〉∈Π(T)。设〈〈π〉〉ki是对于每个i∈[1, n]递归定义的公式，如下：〈〈π〉〉ki={O(ν(π1)∧atk)如果i=1，否则O(ν(πi)∧〈〈π〉〉ki?1)。我们定义π的路径公式为〈〈π〉〉k:=〈〈π〉〉kn。给定conj(F,pLTL[Y])中的?和k∈N，依靠上述路径公式，我们定义past(?,k):=F(?π∈Π(T)〈〈π〉〉k)。注意，这是一个来自F(pLTL[Y,Y?,O])的公式，我们将证明它在轨迹的第k个时间点解释时等价于?。示例1 考虑图1中的公式?，并设k∈N。那么，past(?,k)=F(〈〈π1〉〉k∧〈〈π2〉〉k)，其中：〈〈π1〉〉k:=O((s∨Yq)∧O(YYr∧O(p∧O(p∧atk))))，〈〈π2〉〉k:=O((p∧Yq)∧O(p∧O(p∧atk)))。在上面的例子中可能看起来令人惊讶的是，与图1中的依赖树相比，公式past(?,k)似乎丢失了关于π1和π2共享的所有信息（即这些路径中的前两个节点）。即将推出的引理4表明这是没有问题的：公式past(?,k)等价于Xk?。从这个等价关系中，我们终于可以完成从nf(LTL[X,F])的Xk?i=1c?i到F(pLTL[Y,Y?,O])的转换。算法只需输出：F?i=1cψi，其中每个ψi满足past(?i,k)=Fψi。实际上：Xk?i=1c?i≡?i=1cXk?i（见引理1和R1）≡?i=1cpast(?i,k）（见引理4，下文）≡F?i=1cψi（见引理1和R5）。引理4 设?属于conj(F,pLTL[Y])，且k∈N。那么，Xk?≡past(?,k)。证明作为初步步骤，让我们考虑以下重写规则：R7:F(ψ1∧F(ψ2)∧F(ψ3))?F(ψ1∧F(ψ2))∧F(ψ1∧F(ψ3))。让我们证明这个规则的两边是强等价的。从左到右的方向很容易证明，因此我们关注从右到左的方向。考虑σ∈(2AP)ω和i≥0，并假设?σ,i?F(ψ1∧F(ψ2))∧F(ψ1∧F(ψ3))。那么，存在位置j1, j2, k1, k2使得i≤j1≤j2，i≤k1≤k2，且σ, j1?ψ1，σ, k1?ψ1，σ, j2?ψ2和σ, k2?ψ3。假设j1≤k1（k1>，都有F(〈〈π〉〉k)≡Xk(ν(π1)∧F(ν(π2)∧F(?F(ν(πn))?))。让我们证明这个等价的从右到左的方向。另一个方向的证明类似。考虑一个轨迹σ∈(2AP)ω，并假设?σ,0?Xk(ν(π1)∧F(ν(π2)∧F(?F(ν(πn))?)))。根据定义，存在j1,j2,?,jn∈N使得k=j1≤j2≤?≤jn且σ, ji?ν(πi)，对于每个i∈[1, n]。直接根据定义6，对于每个i∈[1, n]，我们有?σ,ji?〈〈π〉〉ki；特别地，σ, jn???π??k。因此，?σ,0?F(〈〈π〉〉k。□下载：下载高分辨率图像（68KB）下载：下载全尺寸图像图2. 公式?:=p∧F(p∧F(YYr∧F(s∨Yq))∧F(Yq∧p)的依赖树应用规则R7的示例。最右边的依赖树对应于公式p∧F(p∧F(YYr∧F(s∨Yq)))∧F(p∧F(Yq∧p))。5.3. 算法输出大小的分析我们现在证明我们的程序输出的是一个指数级的公式，从而显示了本文的主要结果：定理1 存在一个从LTL[X,F]到逻辑F(pLTL[Y,Y?,O])的甜蜜化程序，其大小为1-指数级。证明设?是来自LTL[X,F]的一个公式。根据命题1和2，nf(LTL[X,F)中有一个公式Xk?i=1c?i与?等价，其大小为2O(size(?))。这个公式由算法1计算得出。我们的甜蜜化程序的输出是等价的（根据引理4）公式F?i=1cψi，其中past(?i,k)=Fψi，对于每个i∈[1, c]。因此，为了证明这个定理，只需证明对于conj(F,pLTL[Y])中的给定公式γ和k∈N，公式past(γ,k)的大小是polynomial in size(γ)和k。实际上，我们证明这个公式的大小为O(n·(k+n))，其中n?size(γ)。设T?T(γ)。根据past(γ,k)的定义，我们有size(past(γ,k))=∑π∈Π(T)size(〈〈π〉〉k)，其中对于长度为j≤n的通用路径π，我们有size(〈〈(π1,?,πj)〉〉k)=size(〈〈(π1,?,πj)〉〉kj)和size(〈〈(π1,?,πj)〉〉k1)=size(atk)+size(ν(π1))+2，size(〈〈(π1,?,πj)〉〉ki)=size(〈〈(π1,?,πj)〉〉ki?1)+size(ν(πi))+2，其中i∈[2, j]。简单的归纳法表明size(〈〈(π1,?,πj)〉〉k)=size(atk)+2·j+∑i=1jsize(ν(πi))。注意，j和∑i=1jsize(ν(πi))都受到n的限制，且size(atk)属于O(k)，因此size(past(γ,k))属于O(|Π(T)|·(k+n))。最后，|Π(T)|≤n，因为Π(T)中的每条路径都由依赖树T的一个不同叶子表示，且每个这样的叶子都通过映射ν由γ的不同的子公式标记。注2 程序的复杂性根据注1，我们还指出，我们的算法不仅产生了一个指数级的公式，而且运行时间为2O(n)，其中n是输入LTL[X,F]公式的大小。5.4. LTL[X,G]的甜蜜化程序由于最终模态和始终模态之间的对偶性，即?G?≡F??，很容易获得一个1-指数级的LTL[X,G]的甜蜜化算法：推论1 存在一个从LTL[X,G]到逻辑G(pLTL[Y,wY,H])的甜蜜化程序，其大小为1-指数级。证明设?属于LTL[X,G]。以下是甜蜜化程序：1. 将??转换为否定规范形式，并设γ为结果公式。由于?Xψ≡X?ψ且?G?≡F?ψ，这个公式属于LTL[X,F]。2. 将来自定理1的甜蜜化程序应用于γ。结果公式形式为Fχ，其中χ属于pLTL[Y,wY,O]，且?≡?Fχ。3. 将?χ转换为否定规范形式，并设χ′为结果公式。由于?Oψ≡H?ψ且?Yψ≡wY?ψ（且?wYψ≡Y?ψ），这个公式属于pLTL[Y,wY,H]。4. 输出Gχ′。由于?Fχ≡G?χ且?χ≡χ′，我们有?≡Gχ′。□6. 关于算法最优性的讨论现在让我们讨论所提出的算法用于将LTL[X,F]公式转换为F(pLTL[Y,Y?,O]公式的最优性。我们首先提供简洁性的定义。定义7 给定两个时间逻辑L和L′，我们说L可以比L′指数级更简洁，当存在一个（无限的）语言家族 Ln∈N，使得对于每个n∈N，•L中有一个大小为O(n)且语言为Ln?(2AP)ω的公式；•L′中所有语言为Ln的公式大小为2Ω(n)。显然，一旦证明LTL[X,F]可以比F(pLTL[Y,Y?,O])指数级更简洁，我们的算法就是最优的。最近的论文[20]显示了一个更强的结果：从LTL[X,F]中移除模态X后得到的逻辑已经比通过添加模态H扩展的F(pLTL[Y,Y?,O])更简洁。命题3 [20] 逻辑LTL[F]比逻辑F(LTL[Y,Y?,O,H)指数级更简洁。反之亦然。注3 [20]中“更简洁”的定义比上面给出的定义稍微弱一些。特别是，L只需要有一个多项式大小的公式来表征Ln（而不是线性的）。然而，在[20]中用于证明命题3的公式确实具有线性大小。在我们的情况下，我们需要这个更强的结果（和定义）来得出我们的算法是最优的。证明命题3的难点在于证明在前一种情况下，命题符号是从字母表中的所有命题符号中均匀分布中选出的；而在第二种情况下，时间模态同样是从均匀分布中选出的。对于每个输入公式，我们测量了四个不同的指标，这些指标与其对应的输出公式相关：(i) 大小，见图3a；(ii) 时间模态的出现次数，见图3b；(iii) 布尔运算符的出现次数，见图3c；(iv) 深度，定义为嵌套时间模态的最大数量，见图3d。在讨论实验评估的结果之前，我们首先描述图3中的图表是如何组织的。x轴表示输入公式，而y轴表示输出公式。在所有图表中，x轴采用的是线性比例尺，y轴采用的是对数比例尺，除了图3d，其中两个轴都采用线性比例尺。橙色线条代表图表的对角线；蓝色线条则是分段函数，用于插值给定大小的输入公式对应的输出公式的平均值。蓝色线条与橙色线条越接近（或越远离），算法的运行时间就越接近多项式（或指数）时间。

考虑图3a，它将输出公式的大小（y轴上，采用对数比例尺）与输入公式的大小（x轴上，采用线性比例尺）进行了对比。从蓝色线条的趋势可以明显看出指数级的增长，该线条与橙色对角线逐渐分离。因此，至少在随机输入的情况下，我们的pastification算法将LTL[X,F]转换为F(pLTL[Y,Y?,O])的指数级膨胀不仅是最坏情况下的结果；这种情况在大多数情况下都会发生。我们通过绘制输出公式中的时间模态数量（图2b）和布尔运算符数量（图3c）与输入公式中的相应数量的关系，进一步细化了对输出公式大小的分析。这两张图表都显示了相同的指数级增长趋势，表明图3a中的指数级增长既是由于时间模态数量的增加，也是由于布尔运算符数量的增加。最后，在这四个指标中，只有深度没有表现出指数级增长。实际上，图3d中绘制的输出公式深度与输入公式的深度呈线性关系。这并不令人意外，因为：(i) 在转换为标准形式的过程中，所有的重写规则只会使公式深度增加一个常数因子；(ii) 对于任何处于标准形式的公式?，其依赖树T的高度正好是?的深度；(iii) 从依赖树T构建的公式的深度正好是T的高度。

8. 结论与未解决的问题

我们设计并实现了一个pastification算法，用于处理LTL[X,F]公式，该算法生成的F(pLTL)公式的大小与输入公式的大小呈单指数关系。根据[20]中的匹配下界，该算法被证明是最优的。与我们的工作相关的主要未解决问题是coSafetyLTL逻辑的pastification过程的复杂性，即包含模态U的LTL[X,F]的扩展。目前针对这种逻辑的最佳pastification过程是基于Krohn-Rhodes级联分解的方法[5]，该方法在第2节中有所概述，其输出可能达到三指数级大小。该过程需要经过多个中间步骤才能最终构建级联分解。原则上，通过研究用于实现coSafetyLTL语法中所有模态和布尔连接词的级联分解的封闭属性的有效算法[33]，有可能改进这一过程。例如，有一种算法以表示coSafetyLTL公式?的级联分解为输入，返回F?的级联分解。通过这组完整的算法，可以直接构建整个输入公式的级联分解，而无需经过中间自动机表示；希望这样可以显著提高pastification过程的运行时间。最近在[37]中出现了这方面的初步研究成果。

直接研究级联分解的封闭属性的方法似乎比尝试将本文提出的技术扩展到整个coSafetyLTL更有前景。为了解释我们技术的当前局限性，考虑以下公式：F((ψ1Uγ1)∧(ψ2Uγ2))。当ψ1=ψ2=?时，这个公式等同于F(Fγ1∧Fγ2)，根据规则R7，这又等同于(Fγ1)∧(Fγ2)，这意味着两次出现的γ1和γ2是独立的。这种等价性在证明引理4时起着基础性作用。将Fγi替换为ψiUγi会得到公式F(ψ1Uγ1)∧F(ψ2Uγ2)，但这与初始公式不等价。直观上讲，这是因为原始公式要求轨迹中的单个点同时满足两次出现U模态的条件，而后者公式允许轨迹中的不同点分别满足每次出现U模态的条件。因此，如何定义一个合适的依赖树概念变得不明确。上述公式似乎也是获得更强闭包性质下界的有趣起点。特别是，我们无法为形式为F(?i=1n(piUqi))的公式生成一个pastification结果，因为这需要枚举q1,?,qn之间的所有可能顺序。因此，我们推测不存在一个适用于coSafetyLTL的pastification算法，能够生成大小小于O(n!)的公式；换句话说，我们认为像本文提出的单指数级pastification过程不太可能存在。

CRediT作者贡献声明：
Alessandro Artale：撰写——审稿与编辑、初稿撰写、验证、监督、形式分析。
Luca Geatti：撰写——审稿与编辑、初稿撰写、可视化、验证、监督、软件开发、项目管理、方法论研究、形式分析、概念化。
Nicola Gigante：撰写——审稿与编辑、初稿撰写、验证、软件开发、方法论研究、概念化。
Alessio Mansutti：撰写——审稿与编辑、初稿撰写、验证、监督、方法论研究、形式分析、概念化。
Andrea Mazzullo：撰写——审稿与编辑、初稿撰写、可视化、验证、方法论研究、形式分析、数据整理、概念化。
Angelo Montanari：撰写——审稿与编辑、初稿撰写、验证、资源管理、方法论研究、形式分析、概念化。