程序合成(program synthesis)的概念最早由美国数学家、逻辑学家Alonzo Church于1957年提出^[1], 一直以来都是计算机科学领域的难解问题. 简单地说, 程序合成是一种针对用户意图构造出相关程序的软件开发活动, 而用户意图可以采用形式化或半形式化规约, 甚至是自然语言来描述. 如果意图表达为线性时序逻辑(linear temporal logic, LTL)公式, 则称此类问题为LTL合成(LTL synthesis), 通常看作程序合成的一种子类. 一般来说, 可以将LTL合成定义为二人博弈(two-player game)问题, 博弈的双方是环境(environment)和控制器(controller). 控制器的行为被智能体(agent)操控, 根据环境变化做出反应, 但智能体无法干涉环境的行为. LTL合成的解(称为合成策略)是使得控制器能够获胜的策略, 目的是令环境和控制器的所有交互行为序列满足给定的LTL公式. 1989年, Pnueli和Rosner证明了LTL合成的计算复杂度为2EXPTIME-complete^[2]. 由于复杂度较高, 学者们通过研究LTL子集的合成来获得较低的复杂度, 进而提高合成效率. 其中, 针对一类子集GR(1) (generalized reactivity(1)), 学者们提出了复杂度为多项式级别($ \mathbb{O}$(n³))的算法, 用于检查GR(1)公式是否可实现(realizable), 并给出了合成策略^[3]. 目前存在许多有效的LTL合成工具, 如Acacia+^[4], Lily^[5], SynKit^[6]和ltlsynt^[7]等.

近期涌现出许多工作, 通过借鉴高效的符号化技术求解LTL合成问题. 文献[8]致力于研究安全LTL(不含until操作符的LTL公式)合成, 并提出一种构建符号化安全自动机(deterministic safety automata)的方法, 从而利用基于传统的BDD (binary decision diagram)技术直接求解. Bohy等人提出了一种基于反链符号化增量算法求解安全博弈问题, 而安全博弈问题刚好可以由LTL合成问题归约而来^[4]. 在求解过程中, LTL公式尽可能地被转换为确定Büchi自动机(deterministic Büchi automata). 该方法的优势在于可以获得更紧凑的策略, 并可对规模较大的LTL合取公式进行组合求解; 而缺点在于不是所有LTL公式都存在对应的确定Büchi自动机, 因此存在一定的局限性.

LTL_f是LTL的一个变种, 二者的区别在于, 前者的语义模型限制为有穷^[9]. 目前也存在一部分研究工作聚焦LTL_f合成问题. Giacomo和Vardi从理论的角度证明了一个重要结论, 即LTL_f合成的计算复杂度与LTL合成相同, 前者并没有因为有穷模型而使得复杂度降低^[10]. Zhu等人提出了一种基于符号化的框架, 将LTL_f合成问题归约为DFA (deterministic finite automata)博弈, 并进一步表示为布尔公式, 然后利用布尔分析生成策略^[11]. LTL_f合成还在机器人领域得到实际应用. 文献[12]提出了一种基于BDD的组合方法, 将LTL_f合成应用于有限视野任务, 能够合成UR5机器人的任务策略. 文献[13]在资源有限条件下研究如何生成机器人策略, 采用LTL_f描述有限任务, 并通过将LTL_f合成归约为定量博弈的技术路线进行求解. 此外, 最新的工作着重在不同假设的前提下研究LTL_f合成问题, 如公平性和稳定性^[14]、LTL条件^[15]等.

近年来, 有研究成果表明, 智能规划(automated planning)^[16]与LTL合成有着紧密的联系, 从而开辟了一种LTL合成的新途径. 具体而言, LTL合成与智能规划的一类子问题, 即非确定规划(non-deterministic planning)存在很多相似之处. Camacho等人将LTL_f合成问题转换为非确定规划问题, 融合了动态状态抽象和惰性自动机确定化技术, 不仅能够给出合成策略, 在合成不可实现(unrealizable)的情况下, 还能够给出相应证明^[17]. 文献[18]将目标为LTL公式的非确定规划描述为二人博弈, 基于此构建起LTL合成和非确定规划的关系, 使得二者可以很容易地进行相互转换. 本文借鉴了文献[19]提出的转换方法, 并对其进行改进. 关键的区别在于: 本文提出的方法在规划过程中仅模拟自动机的一条路径, 而文献[19]则同时保留多条路径. 两种方法的详细比较将在后续实验章节阐述. 与前述工作不同, D’Ippolito等人从相反的思路研究非确定规划与LTL合成的关系, 将非确定规划编码为LTL合成问题, 并利用合成技术进行规划求解^[20]; Bonet等人将广义规划(generalized planning)问题规约为LTL合成问题^[21]. 此外, 还有工作研究其他类型时序逻辑的合成问题, 如采用STL (signal temporal logic)描述合成意图^[22]. 其中, STL能够表达实值信号的时序性质, 一般可用于分析混成系统或混合信号电路.

本文提出了一种新的基于智能规划技术的LTL合成方法, 其核心思想是: 在二人博弈定义的前提下, 将LTL合成转换为非确定规划模型. 博弈双方的行为均由规划动作模拟. 在此过程中, 需要将LTL公式转换为非确定Büchi自动机. 相比其他求解方法, 本文提出的方法可以直接利用现有高效规划器, 并且获得的合成策略更为紧凑, 具备一定的实际应用价值.

本文第1节简要介绍LTL、LTL合成以及非确定规划的基本概念. 第2节详细给出从LTL合成到非确定规划模型的具体转换方法, 将LTL合成过程变为规划求解过程, 这也是本文的主要贡献. 第3节通过实验对比, 证明本文所提方法的可行性和有效性. 最后总结全文, 并对未来可能的研究方向进行初步探讨.

1 技术背景 1.1 线性时序逻辑LTL

LTL是一种模态逻辑, 在命题逻辑的基础上引入时序操作符next(○)和until(U), 用于描述线性时间性质.令P表示原子命题集合, LTL公式ϕ的语法定义如下(其中, p∈P):

$ \phi::=p|\neg \phi| \phi_{1} \wedge \phi_{2}|\bigcirc \phi| \phi_{1} {\bf{U}} \phi_{2} . $

LTL的语义模型定义为无限状态序列σ=s₀, s₁, …, 其中, 任意s_i为P的一个子集. true, false和其他命题逻辑操作符∨, →, ↔可以由ϕ中定义的基本操作符导出. LTL公式的可满足性定义如下:

σ, i|p       iff       p∈P;

σ, i|¬ϕ       iff       not σ, i|ϕ;

σ, i|ϕ₁∧ϕ₂       iff       σ, i|ϕ₁ and σ, i|ϕ₂;

σ, i|ϕ₁Uϕ₂       iff       ∃j≥i such that σ, j|ϕ₂, and σ, k|ϕ₁ for each i≤k≤j−1.

我们称σ满足ϕ, 表示为σ|ϕ, 当且仅当σ, 0|ϕ. 简单地说, ○ϕ描述ϕ将在下一状态成立; ϕ₁Uϕ₂的含义是直到ϕ₂成立之前, ϕ₁一直成立. 其他时序操作符, 如eventually(◊)和always(□)定义为: ◊ϕ$ \triangleq $trueUϕ, □ϕ$ \triangleq $¬◊¬ϕ.

定义1. 非确定Büchi自动机(non-deterministic Büchi automata, NBA)是一个五元组: B=(Q, Σ, δ, q₀, F), 其中, Q是自动机的状态集合, Σ是字母表, δ⊆Q×Σ×Q是迁移关系, q₀是初始状态, F⊆Q是接受状态集合.

P的字集合表示为Lits(P)=P∪{¬p|p∈P}. 一般地, 可令Σ=2^Lits(P). B路径γ=q₀, q₁, …是一个无限状态序列, 定义在字序列σ=s₀, s₁, …之上, 满足对于任意i≥0, 有(q_i, s_i, q_i+1)∈δ. 如果一条路径中出现无限多个接受状态, 则称该路径是可接受的. 如果存在B的一条可接受路径定义在σ之上, 则称B接受σ. 给定LTL公式ϕ, 我们可以构造NBA B_ϕ, 使得B_ϕ接受σ当且仅当σ|ϕ. 在最坏情况下, 构造B_ϕ的时间复杂度随着ϕ大小的增加(公式的大小由其包含的操作符和变量的数量决定)呈指数级增长^[23].

例1: 图 1展示了LTL公式□(x↔◊y)和◊□(x↔y)对应的NBA. 自动机的状态表示为圆(双环圆是接受状态), 迁移表示为箭头. 需要注意的是, 这里用“∨”操作符简化了迁移的描述. 例如, 迁移(q₀, ¬x∨y, q₀)可以看作由两条迁移(q₀, ¬x, q₀)和(q₀, y, q₀)组合而成.

1.2 LTL合成

LTL合成的定义最早由Pnueli和Rosner给出^[2], 他们将LTL合成描述为二人博弈, 博弈的双方分别为环境和控制器. 博弈过程包括一个无限的回合序列, 每个回合首先由环境执行一个动作, 然后智能体为控制器选择另一个动作应对(控制器也可先于环境执行). 动作的任务是对一些变量赋值. 无论环境如何选择动作, 如果环境和控制器交互产生的状态序列满足给定的LTL公式, 则称控制器存在获胜策略. LTL合成的形式化定义如下:

定义2. LTL合成问题是一个三元组$\mathcal{L} $=(X, Y, ϕ), 其中, X={x₁, …, x_n}为环境变量集合, Y={y₁, …, y_n}为控制器变量集合, 且X和Y不相交(任意变量x∈X∪Y为命题变量), ϕ为LTL公式. 如果存在一个函数f: (2^X)*→2^Y, 对于任意X的子集序列X₁, X₂, …和σ=(X₁∪f(X₁)), (X₂∪f(X₂)), …, 使得σ|ϕ, 且ϕ中所含变量属于X∪Y, 则称ϕ是可实现的. 其中, X_i为成立的环境变量集合, X\X_i为不成立的环境变量集合. f(X₁, X₂, …)和Y\f(X₁, X₂, …)的含义类似.

直观地说, LTL合成要求无论环境如何选择(序列X₁, X₂, …), 控制器都能找到相应的策略(f), 保证此博弈模型满足ϕ. 实际上, LTL合成问题就对应求解函数f. 若存在f, 称LTL合成问题为可实现的; 否则, 称其为不可实现的.

例2: 令$\mathcal{L} $₁=({x}, {y}, □(x→◊y)), $\mathcal{L} $₂=({x}, {y}, ◊□(x↔y))为LTL合成问题. 一般情况下, 可以用自动机形式描述合成策略. 图 2(a)和图 2(b)分别给出了$\mathcal{L} $₁与$\mathcal{L} $₂的一种合成策略. 容易验证, 图 2所示的任意无限序列均满足给定公式.

1.3 非确定规划

定义3. 完全可观测的非确定规划(fully observable non-deterministic planning, FOND)问题是一个四元组: $\mathcal{P} $=(P, I, G, A), 其中, P是事实(fluent)集合, I⊆P是初始状态, G⊆P是目标条件, A是动作集合. 完全可观测的含义是所有事实的真值在每个状态下都是可以确定的, 凡是未出现在状态中的事实均不成立.

每个动作a∈A包含两个元素(pre(a), eff(a)), 其中, pre(a)⊆Lists(P)是a的前置条件, eff(a)是a的效果. 需要强调的是: eff(a)是非确定的, 即可能存在多个互斥的子效果. 每个子效果e∈eff(a)是一个条件效果集合, 形如C > l, 其中, C⊆Lits(P)并且l∈Lits(P). 给定状态s⊆P和事实p∈P, s满足p当且仅当p∈s, s满足¬p当且仅当p∉s.此外, s满足字集合L当且仅当s满足任意l∈L. 下面将举例说明非确定效果的含义. 在经典的规划问题Tireworld中, 汽车在两点之间移动采用一个动作模拟, 该动作包含两个非确定子效果: 一个是到达目的地后轮胎气充足, 另一个是到达目的地后轮胎亏气. 在求解时, 需要同时考虑两个子效果出现的情况, 即: 若轮胎气充足时继续行驶, 若轮胎亏气时则补气后再行驶.

如果状态s满足pre(a), 则称动作a在s下是可执行的. s′是a在s下执行的结果, 且s′=s\{p|(C > ¬p)∈e, s满足C}∪{p|(C > p)∈e, s满足C}. 策略$\mathbb{P} $是将状态映射到动作的部分函数, 满足: 如果$\mathbb{P} $(s)=a, 则a在s下是可执行的. $\mathbb{P} $在s下的执行π是一个有限或者无限序列s₀, a₀, s₁, a₁, …, 其中, s₀=s, 每个“状态-动作-状态”子序列s, a, s′满足$\mathbb{P} $(s)=a, 且s′是a在s下的执行结果. 若去除执行的所有动作, 则可以获得一个状态序列, 称执行产生该状态序列. 同理, 若去除执行的所有状态, 称执行产生动作序列.

如果有限执行π的最终状态s满足字集合L, 则称π达到L. 如果存在无限执行π的某个状态s在π中出现无限多次, 且s满足L, 则称π达到L. 无限执行π是公平的(fair)当且仅当如果s, a在π中出现无限多次, 则s, a, s′也在π中出现无限多次, 其中, s′是a在s下的任意执行结果. 在这种定义下, 意味着有限执行是公平的. 策略$\mathbb{P} $是$\mathcal{P} $的一个强循环解(strong-cyclic plan)当且仅当$\mathbb{P} $在I下的每个公平执行均达到G. FOND问题还有强解(strongplan)和弱循环解(weak-cyclic plan)的定义, 但本文并未涉及^[24].

2 LTL合成的FOND模型

LTL合成是否可实现, 与FOND问题是否存在强循环解有着紧密的联系. 本节主要介绍一种转换方法, 将LTL合成的二人博弈定义转换为FOND模型.

2.1 从LTL合成到非确定规划的转换

给定一个LTL合成问题$\mathcal{L} $=(X, Y, ϕ). 首先对$\mathcal{L} $进行预处理, 去除X和Y中不在ϕ出现的变量. 这样做可以简化问题, 因为这些变量对于合成ϕ是无关的, 其真值的变化不影响ϕ的任意模型. 接着, 将$\mathcal{L} $转换为标准的FOND问题模型$\mathcal{P} $=(P, I, G, A). 最后, 直接利用FOND规划器求解$\mathcal{P} $. 所得的强循环解需要进一步变形才能得到$\mathcal{L} $的合成策略, 但是这个步骤比较直观, 可以很容易地实现.

这里重点阐述$\mathcal{L} $到$\mathcal{P} $的转换过程, 我们将其称为$\mathcal{L} $2$\mathcal{P} $. 在此过程中, ϕ需要被转换为等价的NBA B_ϕ=(Q, Σ, δ, q₀, F). 结合$\mathcal{L} $和B_ϕ, 通过模拟环境和控制器的博弈过程以及B_ϕ的迁移约束, 进而得到FOND模型. B_ϕ的每个状态由与之同名的事实变量模拟, B_ϕ的每个迁移由一个规划动作模拟. 在规划过程中, 规划状态s需满足: 事实变量q(对应自动机状态q)成立当且仅当存在B_ϕ的某条路径定义在σ之上, 且路径的最后一个状态为q, 其中, σ为从初始状态到s的规划搜索状态序列. 博弈的过程在规划模型中主要由两个交替变换的模式来模拟, 即“环境模式”和“自动机模式”. 前者模拟环境的行为, 该模式的所有行为是非确定的且无法预知和控制; 后者通过同步自动机的迁移模拟控制器的行为, 该模式下的每个行为对应一个迁移. 此外, 还存在另外一个“记录模式”, 目的是记录当前激活的自动机状态, 下文将会具体解释.

下面将详细说明转换的技术细节. 转换后P的定义如下.

● 事实集合P

P={prev_q, q|q∈Q}∪{env_mode, aut_mode, record_mode}∪{turn_i|1≤i≤|X|}∪{v_x, v_¬x|x∈X∪Y}∪{goal}.

自动机的状态是否成立, 由其前序状态以及两状态之间的迁移条件决定. 因此, 针对每个自动机状态q∈Q, 引入两个事实变量prev_q和q与之对应, 分别表示自动机状态q在上一状态是否成立以及在当前状态是否成立. 事实变量env_mode, aut_mode和record_mode用于标记规划所处的模式: 分别表示环境模式、自动机模式和记录模式. 记录模式主要为后续规划记录此时成立或激活的自动机状态. 3个模式依次交替变换. 事实变量turn_i的作用将在介绍动作集合时给出. 对于每个变量x∈X∪Y, 采用两个事实变量v_x, v_¬x分别显式描述将x赋值为真或假(值得注意的是, 根据等价关系x≡¬¬x, 可以得出v_x≡¬v_¬x). goal用于标记规划目标.

● 动作集合A

$ A={assign_{x}|x∈X}∪{trans_{t}|t∈δ}∪{record_{q}|q∈Q}. $

(1) 环境模式下可执行的动作集合为{assign_x|x∈X}. 由于环境的行为是智能体不可控的, 环境有可能任意改变变量的值, 因此采用一系列非确定动作来模拟这种不确定性. 假设X={x₁, x₂, …, x_|X|), 其中每个变量x_i∈X对应一个非确定动作$assig{n_{{x_i}}}$, 定义如下:

$ \begin{array}{l} pre(assig{n_{{x_i}}}) = \{ env{\text{_}}mode, tur{n_i}\} \hfill \\ eff(assig{n_{{x_i}}}) = oneof(\{ {v_{{x_i}}}, \neg {v_{\neg {x_i}}}\} , \{ \neg {v_{{x_i}}}, {v_{\neg {x_i}}}\} ) \cup \left\{ {\begin{array}{*{20}{l}} {\{ tur{n_{i + 1}}, \neg tur{n_i}\} , {\text{ if }}i < |X|} \\ {\{ aut{\text{_}}mode, \neg env{\text{_}}mode, \neg tur{n_i}\} , {\text{ if }}i = |X|} \end{array}} \right. \hfill \\ \end{array} $

所有变量按照一定顺序依次被赋值. turn_i在$assig{n_{{x_i}}}$的前置条件中出现, 说明turn_i成立时$assig{n_{{x_i}}}$才能执行. $assig{n_{{x_i}}}$的效果包含一个非确定效果, 用关键字oneof表示, 模拟将x_i赋值为真或假. 当最后一个变量x_|X|执行结束后, 从环境模式切换为自动机模式.

还有其他环境模式的动作定义方法, 只需定义一个动作assign_X, 其效果中包含2^|X|个非确定子效果. 然而, 这种定义可能会导致效果数量爆炸, 只适用于|X|较小的情况.

$ \begin{array}{l} pre(assig{n_X}) = \{ env{\text{_}}mode\} \hfill \\ eff(assig{n_X}) = \{ aut{\text{_}}mode, \neg env{\text{_}}mode\} \cup oneof(\{ {v_{{x_1}}}, \neg {v_{\neg {x_1}}}, {v_{{x_2}}}, \neg {v_{\neg {x_2}}}, ..., {v_{{x_{|X|}}}}, \neg {v_{\neg {x_{|X|}}}}\} , \{ {v_{{x_1}}}, \neg {v_{\neg {x_1}}}, {v_{{x_2}}}, \neg {v_{\neg {x_2}}}, ..., \hfill \\ {\text{ }}\neg {v_{{x_{|X|}}}}, {v_{\neg {x_{|X|}}}}\} , ..., \{ \neg {v_{{x_1}}}, {v_{\neg {x_1}}}, \neg {v_{{x_2}}}, {v_{\neg {x_2}}}, ..., \neg {v_{{x_{|X|}}}}, {v_{\neg {x_{|X|}}}}\} ) \hfill \\ \end{array} $

(2) 自动机模式下的动作模拟Y中变量赋值以及自动机迁移. 每次更新自动机的迁移, 可以看作智能体观察X中变量赋值后所做出的反应(对Y中变量进行赋值). 智能体决定选择执行哪个迁移动作, 并确保不违反激活迁移的条件. 针对每个迁移t=(q_i, guard(t), q_j)∈δ, guard(t)∈2^Lits(P), 定义一个规划动作trans_t:

$ \begin{array}{l} pre(tran{s_t}) = \{ aut{\text{_}}mode, prev{\text{_}}{q_i}\} \cup \{ \neg {v_{\neg l}}|l \in guard(t)\} \hfill \\ eff(tran{s_t}) = \{ record{\text{_}}mode, \neg aut{\text{_}}mode\} \cup \{ {q_j}, \neg prev{\text{_}}{q_i}\} \cup \{ {v_l}|l \in guard(t)\} \hfill \\ \end{array} $

当前序状态下q_i成立, 即prev_q_i成立, 且trans_t的前置条件不违反t的迁移条件{¬v_¬l|l∈guard(t)}, trans_t才存在执行的可能性. trans_t的效果包括设置q_j为真, 并设置guard(t)的所有事实变量条件成立. 注意, 在每个状态下只保持一个活动的自动机状态. 也就是说, 只模拟记录自动机的一条路径. 在此模式下执行一个动作后, 切换至记录模式.

(3) 每个自动机状态q∈Q对应记录模式下的一个动作record_q, 其前置条件要求q成立. 执行某一record_q动作后, 重新切换至环境模式. record_q的效果重置所有x∈X∪Y, 并为后续规划记录q为活动状态(prev_q置为真). 当q为接受状态时, 此时效果包含两个不确定子效果, 其中: 一个子效果包含目标goal和prev_q; 另一个子效果与q为非接受状态时相同, 即prev_q. 将goal加入非确定效果的做法, 使得求解时必须多次执行record_q才能使得经过所有子效果的路径到达目标, 从而模拟B_ϕ的无限可接受路径:

$ \begin{array}{l} pre(recor{d_q}) = \{ record{\text{_}}mode, q\} \hfill \\ eff(recor{d_q}) = \{ env{\text{_}}mode, \neg record{\text{_}}mode, tur{n_1}, \neg q\} \cup \{ \neg {v_x}, \neg {v_{\neg x}}|x \in X \cup Y\} \cup \hfill \\ {\text{ }}\left\{ {\begin{array}{*{20}{l}} {prev{\text{_}}q, {\text{ if }}q \notin F} \\ {oneof(\{ prev{\text{_}}q\} , \{ goal, prev{\text{_}}q\} ), {\text{ if }}q \in F} \end{array}} \right. \hfill \\ \end{array} $

初始状态I和目标G: 初始状态设置模式为环境模式, 且令turn₁成立, 并令B_ϕ的初始状态成立, 即I={env_mode, turn₁, prev_q₀}. 将goal设为规划目标, 即G={goal}.

例3: 令$\mathcal{L} $₁=({x}, {y}, □(x→◊y))为例2的LTL合成问题, □(x→◊y)的NBA如图 1(a)所示. 根据前述转换方法, 事实集合P={prev_q₀, q₀, prev_q₁, q₁}∪{env_mode, aut_mode, record_mode}∪{turn₁}∪{v_x, v_¬x, v_xy, v_¬y}∪{goal}.动作集合定义如下:

环境模式只包含一个动作assign_x:

$ \begin{array}{l} pre(assig{n_x}) = \{ env{\text{_}}mode, tur{n_i}\} \hfill \\ eff(assig{n_x}) = \{ aut{\text{_}}mode, \neg env{\text{_}}mode, \neg tur{n_1}\} \cup oneof(\{ {v_{{x_i}}}, \neg {v_{\neg {x_i}}}\} , \{ \neg {v_{{x_i}}}, {v_{\neg {x_i}}}\} ) \hfill \\ \end{array} $

自动机模式共有5个迁移, 分别为t₁=(q₀, ¬x, q₀), t₂=(q₀, y, q₀), t₃=(q₀, true, q₁), t₄=(q₁, y, q₀), t₅=(q₁, true, q₁), 对应以下5个动作:

$ \begin{array}{l} pre(tran{s_{{t_1}}}) = \{ aut{\text{_}}mode, prev{\text{_}}{q_0}, \neg {v_x}\} , {\text{ }}eff(tran{s_{{t_1}}}) = \{ record{\text{_}}mode, \neg aut{\text{_}}mode, {q_0}, \neg prev{\text{_}}{q_0}, {v_{\neg x}}\} ; \hfill \\ pre(tran{s_{{t_2}}}) = \{ aut{\text{_}}mode, prev{\text{_}}{q_0}, \neg {v_{\neg y}}\} , {\text{ }}eff(tran{s_{{t_2}}}) = \{ record{\text{_}}mode, \neg aut{\text{_}}mode, {q_0}, \neg prev{\text{_}}{q_0}, {v_y}\} ; \hfill \\ pre(tran{s_{{t_3}}}) = \{ aut{\text{_}}mode, prev{\text{_}}{q_0}\} , {\text{ }}eff(tran{s_{{t_3}}}) = \{ record{\text{_}}mode, \neg aut{\text{_}}mode, {q_1}, \neg prev{\text{_}}{q_0}\} ; \hfill \\ pre(tran{s_{{t_4}}}) = \{ aut{\text{_}}mode, prev{\text{_}}{q_1}, \neg {v_{\neg y}}\} , {\text{ }}eff(tran{s_{{t_4}}}) = \{ record{\text{_}}mode, \neg aut{\text{_}}mode, {q_0}, \neg prev{\text{_}}{q_1}, {v_y}\} ; \hfill \\ pre(tran{s_{{t_5}}}) = \{ aut{\text{_}}mode, prev{\text{_}}{q_1}\} , {\text{ }}eff(tran{s_{{t_5}}}) = \{ record{\text{_}}mode, \neg aut{\text{_}}mode, {q_1}, \neg prev{\text{_}}{q_1}\} . \hfill \\ \end{array} $

记录模式有两个动作$recor{d_{{q_0}}}$和$recor{d_{{q_1}}}$:

$ \begin{array}{l} pre(recor{d_{{q_0}}}) = \{ record{\text{_}}mode, {q_0}\} , eff(recor{d_{{q_0}}}) = \{ aut{\text{_}}mode, \neg record{\text{_}}mode, \neg {q_0}, oneof(\{ prev{\text{_}}{q_0}\} , \hfill \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\{ goal, prev{\text{_}}{q_0}\} ), \neg {v_x}, \neg {v_{\neg x}}, \neg {v_y}, \neg {v_{\neg y}}\} ; \hfill \\ pre(recor{d_{{q_1}}}) = \{ record{\text{_}}mode, {q_1}\} , eff(recor{d_{{q_1}}}) = \{ aut{\text{_}}mode, \neg record{\text{_}}mode, \neg {q_1}, prev{\text{_}}{q_0}, \neg {v_x}, \neg {v_{\neg x}}, \neg {v_y}, \neg {v_{\neg y}}\} . \hfill \\ \end{array} $

根据上述FOND模型获得的解, 可以表示为图 3所示的图形. 这里, 有效的迁移为assign_x和$tran{s_{{t_1}}}$. 在进行合成策略转换时, 虽然assign_x和$tran{s_{{t_1}}}$顺序执行, 但实际上二者应为同时发生的动作, 因为二人博弈的定义规定环境变量和控制变量的变化是同步的.

2.2 理论证明

定理1. 若|X|+|Y| ≪ |B_ϕ|, 则$\mathcal{L} $2$\mathcal{P} $转换的时间复杂度与|B_ϕ|线性相关.

证明: 按照传统的定义, |B_ϕ|=|Q|+|δ|. 令LTL合成问题$\mathcal{L} $=(X, Y, ϕ), $\mathcal{L} $经过转换得到的FOND模型为$\mathcal{P} $=(P, I, G, A). $\mathcal{L} $2$\mathcal{P} $转换主要包括事实集合转换、动作集合转换以及初始状态和目标转换. 假设转换每个变量的复杂度为常量1, 各转换的时间复杂度分析如下.

● 事实集合转换复杂度: |{prev_q, q|q∈Q}|+|{env_mode, aut_mode, record_mode}|+|{turn_i|1≤i≤|X|}|+|{v_x, v_¬x|x∈X∪Y}|+|{goal}|=2|Q|+3|X|+2|Y|+4;

● 动作集合转换复杂度: 第1类环境模式动作转换的时间复杂度为|{assign_x|x∈X}|=9|X|, 第2类自动机模式动作转换的时间复杂度为{trans_t|t∈δ}=(6+2|X|+2|Y|)|δ|, 第3类记录模式动作转换的时间复杂度为|{record_q|q∈Q}|=(9+|X|+|Y|)|Q|.

● 初始状态和目标转换复杂度: 该转换的时间复杂度为常量.

已知|X|+|Y| ≪ |B_ϕ|, 因此定理的结论成立.

定理2(正确性). 若$\mathcal{P} $是LTL合成问题$\mathcal{L} $经$\mathcal{L} $2$\mathcal{P} $转换得到的FOND模型, 则$\mathcal{P} $的强循环解对应$\mathcal{L} $的合成策略.

证明: 假设$\mathcal{P} $=(P, I, G, A), $\mathcal{L} $=(X, Y, ϕ), ϕ的NBA为B_ϕ. 首先证明$\mathcal{P} $的强循环解$\mathbb{P} $的任意执行产生的序列满足ϕ. 容易证明, $\mathbb{P} $的任意执行产生的序列一定是无限的. 采用反证法, 假设$\mathbb{P} $的某一执行是有限的. 根据G={goal}, 可知存在动作record_q的执行, 使得其中一个非确定子效果goal成立. 然而, 仍然存在另一个不含有goal的非确定子效果无法到达目标. 因此, $\mathbb{P} $的任意执行一定是无限的, 且存在某record_q的无限多次执行. 一般地, 令执行产生的序列为σ. 再根据自动机模式的动作定义, 每次动作执行都符合B_ϕ的某迁移, 由此可以找到定义在σ之上的一条可接受路径. 因此, $\mathcal{P} $的强循环解$\mathbb{P} $的任意执行产生的序列满足ϕ. 我们可以对$\mathbb{P} $稍加改动, 便可得到$\mathcal{L} $的合成策略, 包括: (1) 去除所有record_q动作; (2) 去除X∪Y之外的所有辅助变量; (3) 假设X={x₁, x₂, …, x_|X|), 将所有动作序列$ assig{n_{{x_1}}}, assig{n_{{x_2}}}, ..., assig{n_{{x_{|X|}}}}, tran{s_t} $的执行统一为一个动作, 该动作的前置条件为$ assig{n_{{x_1}}} $的前置条件, 执行效果为的trans_t执行结果, 没有中间执行过程.

定理结论得证.

定理3(完备性). 若$\mathcal{P} $是LTL合成问题$\mathcal{L} $经过$\mathcal{L} $2$\mathcal{P} $转换得到的FOND模型, 则$\mathcal{L} $的任意合成策略均可由$\mathcal{P} $的强循环解得到.

证明: 假设$\mathcal{P} $=(P, I, G, A), $\mathcal{L} $=(X, Y, ϕ), X={x₁, x₂, …, x_|X|), ϕ的NBA为B_ϕ=(Q, 2^Lits(X∪Y), δ, q₀, F). 令f是$\mathcal{L} $的合成策略, 对于任意序列σ=(X₁∪f(X₁)), (X₁∪f(X₁, X₂)), …, 其中, X_i⊆X, f(X₁, X₂, …, X_i)⊆Y. 已知σ|ϕ, 则存在B_ϕ的一条路径q₀, q₁, …, 使得任意(q_i, (X_i∪f(X₁, X₂, …, X_i)), q_i+1)∈δ. 类似定理2中的策略修改方法.

(1) 将X_i和f(X₁, X₂, …, X_i)分解为一系列动作$ {\tau _i} = assig{n_{{x_1}}}, assig{n_{{x_2}}}, ..., assig{n_{{x_{|X|}}}}, tran{s_t} $的最终效果, 其中, t=(q_i, (X_i∪f(X₁, X₂, …, X_i)), q_i+1). 对于x_i∈X_i, 取$assig{n_{{x_i}}}$的非确定子效果$\{ {v_{{x_i}}}, \neg {v_{\neg {x_i}}}\} $; 而对于x_i∉X_i, 取$assig{n_{{x_i}}}$的非确定子效果$\{ \neg {v_{{x_i}}}, {v_{\neg {x_i}}}\} $;

(2) 在τ_i后增加动作$recor{d_{{q_{i + 1}}}}$, 因此, ${\tau _0}, recor{d_{{q_1}}}, {\tau _1}, recor{d_{{q_2}}}, ...$可看作某执行产生的动作序列. 我们可将所有σ对应的动作序列组合得到$\mathbb{P} $. 根据X_i的任意性(X_i∈2^X), $\mathbb{P} $的所有执行产生的状态序列均满足ϕ, 因此$\mathbb{P} $是$\mathcal{P} $的强循环解.

定理结论得证.

2.3 方法对比

本节提出的$\mathcal{L} $2$\mathcal{P} $转换方法改进了Camacho等人提出的转换方法^[19], 记为$\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$). 下面将对$\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)作简要介绍, 并分析二者异同. $\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)转换后的规划模型定义如下.

● 事实集合P

$ P=\left\{q, q^{5}, q^{t}, q^{5 t} \mid q \in Q\right\} \cup\left\{e n v_{-} {mode,aut\_mode,can\_switch,can\_accept }\right\} \cup\left\{t u r n_{i}|1 \leqslant i \leqslant| X \mid\right\} \cup\left\{v_{x}, v_{\neg {x}} \mid x \in X \cup Y\right\} \cup\{g o a l\} \text {. }$

针对每个自动机状态q, 有4个事实变量与之对应, 主要目的在于, 需要同时记录NBA的多条路径. q与q^s, q^t与q^st的关系类似于$\mathcal{L} $2$\mathcal{P} $中的prev_q与q. q和q^t记录前序自动机状态, q^s和q^st记录当前自动机状态. $\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)的模式只包含环境模式和自动机模式. can_switch用于表示X中的变量赋值结束, can_accept用于标记存在一条路径到达接受状态.

● 动作集合A

$ A={assign_{x}|x∈X}∪{trans_{t}|t∈δ}∪{switch2aut, switch2env, accept}. $

(1) 环境模式下的动作与$\mathcal{L} $2$\mathcal{P} $基本相同, 最后一个变量x_|X|赋值后执行switch2aut动作, 其效果将q和q^t分别变为q^s和q^st. 若自动机的节点数目过多, switch2aut的效果将会出现过多的情况, 从而使规划器无法处理:

$ \begin{array}{l} pre(assig{n_{{x_{X|}}}}) = \{ env{\text{_}}mode, tur{n_{|X|}}\} \hfill \\ eff(assig{n_{{x_{|X|}}}}) = oneof(\{ {v_{{x_{|X|}}}}, \neg {v_{\neg {x_{|X|}}}}\} , \{ \neg {v_{{x_{|X|}}}}, {v_{\neg {x_{|X|}}}}\} ) \cup \{ can\_switch, \neg tur{n_{|X|}}\} \hfill \\ pre(switch2aut) = \{ env{\text{_}}mode, can{\text{_}}switch\} \hfill \\ eff(switch2aut) = \{ aut{\text{_}}mode, \neg env{\text{_}}mode, \neg can{\text{_}}switch\} \cup \{ q \triangleright \{ {q^s}, \neg q\} , {q^t} \triangleright \{ {q^{st}}, \neg {q^t}\} |q \in Q\} \hfill \\ \end{array} $

(2) 虽然仍是每个迁移对应一个动作, 自动机模式下的动作与$\mathcal{L} $2$\mathcal{P} $区别很大. 当迁移的后继状态为接受状态时, 将can_accept设置为真; 否则, 如果前序状态$q_i^{st}$成立, 则令$q_j^t$成立:

$ \begin{array}{l} pre(tran{s_t}) = \{ aut{\text{_}}mode, q_i^s\} \cup \{ \neg {v_{\neg l}}|l \in guard(t)\} \hfill \\ eff(tran{s_t}) = \{ {q_j}\} \cup \{ {v_l}|l \in guard(t)\} \cup \left\{ {\begin{array}{*{20}{l}} {\{ q_i^{st} \triangleright q_j^t\} , {\text{ if }}{q_j} \notin F} \\ {\{ can\_accept\} , {\text{ if }}{q_j} \in F} \end{array}} \right. \hfill \\ \end{array} $

从自动机模式切换到环境模式, 可以通过两个动作switch2env和accept. switch2env将所有条件(除了自动机状态变量)置为初值. accept的效果有对自动机状态变量的处理, 并有非确定子效果goal, 使得可以找到访问无限多次接受状态的无限执行. accept也存在效果过多的潜在问题. 更为详细的解释可参考文献[19]:

$ \begin{array}{l} pre(switch2env) = \{ aut{\text{_}}mode\} \hfill \\ eff(switch2env) = \{ env{\text{_}}mode, \neg aut{\text{_}}mode\} \cup \{ tur{n_1}\} \cup \{ \neg {q^s}, \neg {q^{st}}|q \in Q\} \cup \{ \neg {v_x}, \neg {v_{\neg x}}|x \in X \cup Y\} \hfill \\ pre(accept) = \{ aut{\text{_}}mode, can{\text{_}}accept\} \hfill \\ eff(accept) = oneof(\{ goal\} , \{ tur{n_1}\} \cup \{ env{\text{_}}mode, \neg aut{\text{_}}mode, \neg can{\text{_}}accept\} \cup \{ {q^s} \triangleright \neg {q^s}, {q^{st}} \triangleright \neg {q^{st}}|q \in Q\} ) \cup \hfill \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\{ q \wedge {q^t} \triangleright \{ \neg q, \neg {q^t}\} |q \in (Q\backslash F)\} \cup \{ q \wedge \neg {q^t} \triangleright {q^t}|q \in Q\} \cup \{ \neg {v_x}, \neg {v_{\neg x}}|x \in X \cup Y\} \hfill \\ \end{array} $

由于$\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)没有记录模式, 其转换工作量略少于$\mathcal{L} $2$\mathcal{P} $. 然而在下一节我们将会看到: 由于switch2aut和accept动作的效果过多, 导致规划器无法对其解析; 而$\mathcal{L} $2$\mathcal{P} $把这种复杂性简化分布到多个动作中, 不会产生上述情况. 此外, $\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)只保留部分路径而不是全部路径, 因此该方法不是完备的.

例4: 根据$\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)转换方法, 将例2的LTL合成问题$\mathcal{L} $₁转换为FOND模型.

● 事实集合:

$ \begin{array}{l} P = \{ {q_0}, q_0^s, q_0^t, q_0^{st}, {q_1}, q_1^s, q_1^t, q_1^{st}|q \in Q\} \cup \{ env{\text{_}}mode, aut{\text{_}}mode, can{\text{_}}switch, can{\text{_}}accept\} \cup \hfill \\ \;\;\;\;\;\;\;\;\{ tur{n_1}\} \cup \{ {v_x}, {v_{\neg x}}, {v_y}, {v_{\neg y}}\} \cup \{ goal\} \hfill \\ \end{array} $

● 动作集合定义如下:

环境模式有动作assign_x和动作switch2aut:

$ \begin{array}{l} pre(assig{n_x}) = \{ env{\text{_}}mode, tur{n_1}\} , \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;eff(assig{n_x}) = \{ can{\text{_}}switch, \neg tur{n_1}\} \cup oneof(\{ {v_{{x_i}}}, \neg {v_{\neg {x_i}}}\} , \{ \neg {v_{{x_i}}}, {v_{\neg {x_i}}}\} ); \hfill \\ pre(switch2aut) = \{ env{\text{_}}mode, can{\text{_}}switch\} , \;\;\;\;\;\;\;\;eff(switch2aut) = \{ aut{\text{_}}mode, \neg env{\text{_}}mode, \neg can{\text{_}}switch\} \cup \hfill \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\{ {q_0} \triangleright \{ q_0^s, \neg {q_0}\} , q_0^t \triangleright \{ q_0^{st}, \neg q_0^t\} , {q_1} \triangleright \{ q_1^s, \neg {q_1}\} , q_1^t \triangleright \{ q_1^{st}, \neg q_1^t\} \} . \hfill \\ \end{array} $

自动机模式共有7个迁移, 包括5个迁移t₁=(q₀, ¬x, q₀), t₂=(q₀, y, q₀), t₃=(q₀, true, q₁), t₄=(q₁, y, q₀), t₅=(q₁, true, q₁)对应的动作以及switch2env和accept:

$ \begin{array}{l} pre(tran{s_{{t_1}}}) = \{ aut{\text{_}}mode, q_0^s, \neg {v_x}\} , \;\;\;\;\;\;\;\;\;\;\;\;eff(tran{s_{{t_1}}}) = \{ {q_0}, can{\text{_}}accept, {v_{\neg x}}\} ; \hfill \\ pre(tran{s_{{t_2}}}) = \{ aut{\text{_}}mode, q_0^s, \neg {v_{\neg y}}\} , \;\;\;\;\;\;\;\;\;eff(tran{s_{{t_2}}}) = \{ {q_0}, can{\text{_}}accept, {v_y}\} ; \hfill \\ pre(tran{s_{{t_3}}}) = \{ aut{\text{_}}mode, q_0^s\} , \;\;\;\;\;\;\;\;\;\;\;\;\;\;eff(tran{s_{{t_3}}}) = \{ {q_1}, q_0^{st} \triangleright q_1^t\} ; \hfill \\ pre(tran{s_{{t_4}}}) = \{ aut{\text{_}}mode, q_1^s, \neg {v_{\neg y}}\} , \;\;\;\;\;\;\;\;\;eff(tran{s_{{t_4}}}) = \{ {q_0}, can{\text{_}}accept, {v_y}\} ; \hfill \\ pre(tran{s_{{t_5}}}) = \{ aut{\text{_}}mode, q_1^s\} , \;\;\;\;\;\;\;\;\;\;\;\;\;\;eff(tran{s_{{t_5}}}) = \{ {q_1}, q_1^{st} \triangleright q_1^t\} ; \hfill \\ pre(switch2env) = \{ aut{\text{_}}mode\} , {\text{ }}eff(switch2env) = \{ env{\text{_}}mode, \neg aut{\text{_}}mode, can{\text{_}}accept, tur{n_1}, \hfill \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\neg q_0^s, \neg q_0^{st}, \neg q_1^s, \neg q_0^{st}, \neg {v_x}, \neg {v_{\neg x}}, \neg {v_y}, \neg {v_{\neg y}}\} ; \hfill \\ pre(accept) = \{ aut{\text{_}}mode, can{\text{_}}accept\} , {\text{ }}eff(accept) = oneof(\{ goal\} , \{ env{\text{_}}mode, \neg aut{\text{_}}mode, \neg can{\text{_}}accept, tur{n_1}, \hfill \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\neg q_0^s \triangleright \neg q_0^s, \neg q_1^s \triangleright \neg q_1^s, \neg q_0^{st} \triangleright \neg q_0^{st}, \neg q_1^{st} \triangleright \neg q_1^{st}, \hfill \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;{q_0} \wedge q_0^t \triangleright \{ \neg {q_0}, \neg q_0^t\} , {q_0} \wedge \neg q_0^t \triangleright q_0^t, {q_1} \wedge \neg q_1^t \triangleright q_1^t, \neg {v_x}, \neg {v_{\neg x}}, \neg {v_y}, \neg {v_{\neg y}}\} ). \hfill \\ \end{array} $

假设每个变量的空间复杂度为1, 下面将分析$\mathcal{L} $2$\mathcal{P} $和$\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)中某些关键动作的空间复杂度. 二者最重要的区别在于前者的记录模式以及后者的switch2env和accept动作. $\mathcal{L} $2$\mathcal{P} $中每个动作的空间复杂度为8+2(|X|+ |Y|), 而$\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)中switch2env动作的空间复杂度为5+2|Q|+2(|X|+|Y|), accept动作的空间复杂度为7+11|Q|+2(|X|+ |Y|). 从单个动作的角度看, $\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)的两个动作空间复杂度与自动机规模相关. 尤其在自动机规模较大的情况下, 将会导致动作的复杂度过高; 相反, $\mathcal{L} $2$\mathcal{P} $中所有动作的空间复杂度与自动机规模无关.

3 实验与分析

本节主要通过实验比较本文所提方法与其他方法的优劣, 选取的基准测试集来自最近一届国际合成竞赛SYNTCOMP20 (http://www.syntcomp.org/syntcomp-2020-results/). 实验选取的对比合成工具ltlsynt^[7]是参赛工具之一, ltlsynt将输入的LTL公式转换为确定奇偶自动机(deterministic parityautomata), 而后者等价于奇偶博弈(parity game), 并采用Zielonka提出的递归算法求解^[25]. 对于其他合成工具, 如Acacia+^[4], Lily^[5], SynKit^[6]等, 它们的求解效率远低于ltlsynt, 本文仅将SynKit作为另一个现有合成工具进行实验对比. SynKit将LTL合成规约为安全博弈问题, 并建立了该问题与多种自动机(universal k-coBüchiWord (UkCW) automata and non- deterministic k-Büchi word (NkBW) automata)之间的关系. 实验采用的FOND规划器为非确定规划的著名工具PRP^[26]. LTL公式转换为NBA的过程利用LTL2BA^[27]实现. 我们开发了$\mathcal{L} $2$\mathcal{P} $和$\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)转换工具, 并在实验中列出二者的运行效果. 实验运行的平台配置为Ubuntu 16.04操作系统, Intel i7 CPU, 8 GB内存.

主要从两个方面对实验结果进行分析: 一是求解时间, 二是策略的规模. 求解时间说明工具的求解效率, 策略的规模说明解的质量. 策略规模越小, 质量越高, 即说明该策略更加具备实用性. 第1个实验采用的测试集均为不可实现(unrealizable)的LTL合成问题, 即问题无解. 表 1列出了相应的实验结果. 每个问题包含多个实例, 复杂度由低到高, 每个实例的求解时间限制在1小时以内. 由于问题不可实现, 所以不存在合成策略, 表 1仅对比求解时间. 列“SYN”表示ltlsynt的求解时间. $\mathcal{L} $2$\mathcal{P} $和$\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)的运行时间包括3个部分: NBA转换时间(列“NBA”)、FOND模型转换时间(列“FOND”)和规划器PRP求解时间(列“PRP”). $\mathcal{L} $2$\mathcal{P} $和$\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)采用同样的NBA转换工具, 因而NBA的转换时间相同, 所以列“NBA”只出现1次, 将$\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)的NBA列省略. “−”表示超时或者内存不足. 总体来说, $\mathcal{L} $2$\mathcal{P} $和$\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)转换方法能够求解出更多的问题实例, ltlsynt次之, SynKit表现最差(无法求解大部分实例). 然而, $\mathcal{L} $2$\mathcal{P} $和$\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)方法的瓶颈在于NBA转换, 此过程耗费的时间较长. 在极少数情况下, NBA的转换时间就已经超过了ltlsynt的合成时间, 如full_arbiter_unreal的p4实例和prioritized_arbiter_ unreal的p4实例. 相对而言, FOND模型转换的时间可以忽略不计. 在求解复杂实例时, 绝大多数PRP的求解时间都远远小于NBA转换时间, 也小于ltlsynt的求解时间. 对比$\mathcal{L} $2$\mathcal{P} $和$\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)这两种方法, 二者的FOND模型转换时间相近, 而后者的求解效率稍低一些. 原因在于, 关键动作switch2aut和accept的效果较为复杂.

第2个实验采用的测试集均为可实现的LTL合成问题, 实例的NBA规模普遍比第1个实验大很多. 表 2给出了实验结果. 列“$\mathbb{P} $”表示合成策略的大小(仅统计迁移数量), 其中, $\mathcal{L} $2$\mathcal{P} $和$\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)的合成策略只统计提取有效迁移后的策略规模, 即去除记录模式的动作. 针对每个实例, 所有结果中最紧凑的策略加粗显示. SynKit的运行结果无论从求解时间和解质量来说都不尽如人意. $\mathcal{L} $2$\mathcal{P} $($ \mathcal{C}$)的表现较差, 这是由于转换的NBA规模较大, 使得switch2aut和accept动作的复杂度进一步加大, 进而无法获得大部分实例的解, 绝大部分实例求解时内存不足. 从解的覆盖率来看, $\mathcal{L} $2$\mathcal{P} $并没有比ltlsynt求解出更多的实例. 然而, $\mathcal{L} $2$\mathcal{P} $能够为所有实例合成更为紧凑的策略, 更具有实际意义. 规划器一般会追求解的质量, 其内部设置的启发式算法在考虑效率的同时, 以追求较优解为更重要的目标. 求解时间的瓶颈依然是NBA转换, 如prioritized_arbiter_enc的p4实例, 由于NBA的规模过大, 使得转换后的规划模型也很庞大, 致使规划器无法求解. 在求解效率方面, ltlsynt稍具优势, 但是与$\mathcal{L} $2$\mathcal{P} $差距不大.

4 结论

当前, LTL合成仍然是非常重要且具有挑战性的研究问题. 智能规划涌现出了很多有效的方法和工具, 且与LTL合成有着一定的相似性. 基于此, 本文提出了一种基于非确定规划的LTL合成方法, 试图通过利用非确定规划的高效工具求解LTL合成问题. 本文的主要创新点在于: 提出了一种从LTL合成的二人博弈定义到非确定规划模型的转换方法, 且转换的复杂度与LTL公式的NBA大小线性相关, 并证明了方法的正确性和完备性. 选取国际合成竞赛的基准测试集进行实验, 结果证明: 本文提出的方法在规划解的质量方面具有较大优势, 能够获得更为紧凑的合成策略. 未来的工作将着眼于在保证规划解质量的前提下提高合成效率, 研究在非确定规划工具中设计适合LTL合成过程的启发式算法.