Loading [MathJax]/jax/element/mml/optable/SuppMathOperators.js
  • ISSN 0258-2724
  • CN 51-1277/U
  • EI Compendex
  • Scopus 收录
  • 全国中文核心期刊
  • 中国科技论文统计源期刊
  • 中国科学引文数据库来源期刊

基于改进NMPC的永磁电动悬浮汽车横向控制

毕经国 柯志昊 杨轶莹 李诤言 邓自刚

曾国艳, 徐扬, 陈树伟, 姜世攀. 基于多属性决策的一阶逻辑子句选择方法[J]. 西南交通大学学报, 2025, 60(1): 185-193. doi: 10.3969/j.issn.0258-2724.20230023
引用本文: 毕经国, 柯志昊, 杨轶莹, 李诤言, 邓自刚. 基于改进NMPC的永磁电动悬浮汽车横向控制[J]. 西南交通大学学报. doi: 10.3969/j.issn.0258-2724.20240494
ZENG Guoyan, XU Yang, CHEN Shuwei, JIANG Shipan. First-Order Logic Clause Selection Method Based on Multi-criteria Decision Making[J]. Journal of Southwest Jiaotong University, 2025, 60(1): 185-193. doi: 10.3969/j.issn.0258-2724.20230023
Citation: BI Jingguo, KE Zhihao, YANG Yiying, LI Zhengyan, DENG Zigang. Lateral Control of Permanent Magnet Electrodynamic Suspension Vehicle Based on Improved Nonlinear Model Predictive Controller[J]. Journal of Southwest Jiaotong University. doi: 10.3969/j.issn.0258-2724.20240494

基于改进NMPC的永磁电动悬浮汽车横向控制

doi: 10.3969/j.issn.0258-2724.20240494
基金项目: 中央高校基本科研业务费专项资金(2682023CG010);江苏省交通运输厅科技项目
详细信息
    作者简介:

    毕经国(1999—),男,博士研究生,研究方向为磁悬浮汽车智能感知与控制,E-mail:935993966@qq.com

    通讯作者:

    邓自刚(1982—),男,研究员,博士,研究方向为磁浮交通技术及应用,E-mail:deng@swjtu.cn

  • 中图分类号: xxx

Lateral Control of Permanent Magnet Electrodynamic Suspension Vehicle Based on Improved Nonlinear Model Predictive Controller

  • 摘要:

    针对横向力不足、模型不确定和时变扰动环境下永磁电动悬浮汽车横向运动控制问题,提出一种改进非线性模型预测横向跟踪控制方法(NMPC-ESO-EKF)以实现车辆横向精准控制. 首先,提出通过偏转磁轮来补偿系统横向力的横向运行模式,以此建立横向非线性动力学模型;然后,建立含有约束条件的NMPC控制器,并构造扩张状态观测器(ESO)来观测系统内外扰动以补偿控制输入,同时引入扩展卡尔曼滤波器(EKF)消除传感器测量噪声对ESO观扰的影响;最后,搭建联合仿真平台和实验平台进行仿真与实验验证. 研究结果表明:永磁电动悬浮汽车在横向运行模式下,能有效实现左右横移运动;相较于PID-EKF控制,在定常数参考信号下,NMPC-ESO-EKF超调量降低98.90%,系统调节时间缩短47.78%;在方波参考信号下,系统平均超调量和平均跟踪误差分别降低了93.77%和36.13%;施加扰动后,系统横向位移波动幅值减小34.51%,恢复时间缩短42.08%,横向控制精度与抗扰能力大幅提升,为永磁电动悬浮汽车横向控制研究提供一定参考.

     

  • 一阶逻辑是经典的逻辑理论,基于一阶逻辑的定理机器证明和自动推理是人工智能领域的重要研究课题. 1965年,Robinson[1]提出的归结原理是实现定理自动证明的工具之一,推动了自动推理的发展.自动定理证明器(ATP)通过输入被形式化为一阶逻辑的前提条件和结论,自动从前提条件推出结论. 研究ATP有重要的应用价值:一阶逻辑可以形式化研究软件验证[2]、数学定理证明[3]、信息安全的程序自动验证[4]等.

    因为一阶逻辑子句含有变元的函数项,所以搜索空间是无限的,这使得一阶逻辑定理的证明成为一个无限问题. 目前,ATP采用的推理规则主要有2类:一类是归结原理,每次有且仅有2个子句参与归结,只消去一组互补对文字,生成的归结式含有大量文字;另一类是2018年Xu等[5]提出的标准矛盾体分离(S-CS)规则,突破了静态二元归结的限制,允许多个子句动态参与演绎,生成大量单元子句. Xu等[6]同年分析了(S-CS)规则的优势,如动态性、协同性、鲁棒性等.

    根据上述提到的2类推理方法,ATP选择其中一种作为推理机制. 确定推理机制后,提高ATP的证明效率是关键. ATP选择子句集中的子句,按照推理规则进行推理,直至推出空子句,定理得证. 子句的选择是ATP必不可少的部分. 理论和实验表明,有些子句会多次参与演绎推理,而有些则未能参与. 因此,通过启发式策略选取合适的子句对提升ATP性能至关重要. 由于不同推理规则之间存在本质差异,针对基于不同推理规则的ATP,应采用不同的启发式策略.

    当前,针对ATP的启发式策略已有广泛研究. 例如,基于重写规则的E中多种项排序策略[7]、基于二元归结的Vampire中动态选择策略[8]. 基于S-CS规则的启发式策略包括子句演绎权重[9]、决策文字选择策略和矛盾体分离式策略[10]等. 这些子句选择策略通常通过设定策略优先级来决定子句参与演绎的顺序,优先级越高的策略对应的子句会优先被选择. 然而,这些策略有时需要多次比较子句优先级,才能选择出一个合适的子句,在一定程度上会影响对子句的评估.

    为解决该问题,本文提出一种新的子句选择框架,将多种策略选择子句视为多属性决策问题. 不同的子句选择策略反映了子句的不同属性特征,因此,每种策略对应不同的子句属性,为多属性决策(MCDM)方法综合评估子句提供了基础. 本文利用MCDM方法,根据多种子句属性值对各子句进行综合评估.

    目前,已有多种经典的MCDM方法,例如逼近理想解法(TOPSIS) [11]、VIKOR[12]和偏好顺序结构评估法(PROMETHEE) [13]等. 其中,PROMETHEE能在丢失很少属性信息情况下对候选子句进行部分或完全排序,因而在实际决策过程中较其他MCDM方法具有更高的灵活性. PROMETHEE的核心思想是通过正、负优先流以及净占优流对候选子句进行排序,其已扩展出多种形式[14],包括PROMEHTEE Ⅰ 、PROMETHEE Ⅱ 、PROMETHEE Ⅲ、PROMETHEE Ⅳ等. 其中,PROMETHEE Ⅱ能够对候选子句进行完全排序,且无需对子句属性值进行量纲化和规范化处理,从而避免了信息偏差. 因此,本文选择PROMETHEE Ⅱ对子句进行评估.

    本文采用MCDM方法评估子句有如下优点:1) MCDM基于子句的多种客观信息进行评估,有效避免了人为设定策略优先级的问题,一定程度上减少了为设置优先级而进行的大量实验测试. 2) MCDM已有成熟的研究,为多属性决策评估子句提供了理论依据,支持多种子句属性同时参与决策评估. 3) WCDM是一种高效的动态综合评估方法,能够反映子句的多种属性特征,通过组合策略进行评估,通常优于单一策略.

    本文基于S-CS规则的多个子句动态参与演绎的特性,在演绎过程中应用PROMETHEE Ⅱ方法对子句进行排序. 当子句属性值在演绎过程中发生更新时,子句排序也会相应更新. 对比实验结果表明,基于S-CS规则的PROMETHEE Ⅱ方法能有效提升ATP的性能.

    首先介绍本文涉及的一阶逻辑的相关概念[15].原子公式由谓词符号(如P)和项组成. 其中,变元(如x, y)、常元(如a)和函数符(如f)都是项. 原子公式A及其否定¬A称为文字,称A¬A为互补对. 若干个文字的析取称为子句,只有一个文字的子句称为单元子句. 若干个子句的合集称为子句集. 一个替换是形如{t1/y1,t2/y2,,tN/yN}的有限集合,其中,yJJ=1,2,,N为变量符号,N为变量个数, tJ为不同于yJ的项. 集合中yJ各不相同,称tJ为替换的分子,yJ为替换的分母.

    二元归结方法只允许(有互补对的) 2个子句参与归结,从而仅消去1组互补对文字;而矛盾体分离规则允许多个子句参与演绎,每次演绎可消去多组互补对,是二元归结方法的拓展.

    矛盾体分离规则[5]:设一阶逻辑子句集 S={C1,C2,,Cm}m为子句个数),子句 C1C2Cm之间不存在相同变元(若存在不同的子句有相同的变元,则需对变元更名),称由子句集S产生新子句的推理规则为标准矛盾体分离规则,简称S-CS规则.

    对于任意子句Ckk=1,2,,m),存在替换σk可以应用于子句Ckσk可以为空替换),使得Ck中相同的文字可以合并,得到子句Ckσk.Ckσk分为两部分子句(CkσkC+kσk),满足:

    1) Ckσk=CkσkC+kσk, CkσkC+kσk不含相同的文字,Ckσk不能为空,C+kσk可以为空.

    2) 对任意x1,x2,,xmmk=1Ckσkx1,x2,,xm中至少存在一个互补对文字,称mk=1Ckσk为标准矛盾体(S-SC).

    3) mk=1C+kσk=Csmσ(C1,C2,,Cm),其中,σ=mk=1σk,称Csmσ(C1,C2,,Cm)为矛盾体分离式(S-CSC).

    根据上述S-CS规则,演绎定义如下:

    定义1 矛盾体分离动态演绎[5]:设一阶逻辑子句集S={C1,C2,,Cm},对于任意的h{1,2,,ˉt}ˉt为演绎序列个数),当Φ1,Φ2,,Φˉt满足下列条件之一,则称Φ1,Φ2,,Φˉt为基于标准矛盾体分离的多元动态演绎序列,称该演绎为S-CS演绎:

    1)ΦhS.

    2) 存在 r1,r2,,rlh<h, 有矛盾体分离式Φh=Csrlhθh(Φr1,Φr2,,Φrlh). 其中,替换 θh=lhK=1σK,σKΦrK的变元替换,K=1,2,,lh.

    与二元归结演绎形成鲜明对比,S-CS演绎有以下显著的优势:

    1) 多元演绎. 多个子句协同参与演绎,通过分离矛盾体删除多个互补对,从而生成含有文字数较少的矛盾体分离式.

    2) 可控性. 矛盾体的大小和文字数均可控. 可限制S-CS规则生成的矛盾体分离式所含的文字数,如限制在6个文字以内. 当生成的子句不符合该限制时,将重新构造矛盾体,直到生成的子句满足文字数限制或产生空子句为止.

    3) 生成大量单元子句,S-CS规则有生成大量单元子句的能力. 如在矛盾体分离式的文字数不超过6个的限制下,通过实验分析发现,矛盾体分离式为单元子句的占比为90%左右.

    为更好地规划演绎搜索路径并节省计算资源,学者们提出了多种启发式策略[16-19] ,用于选择合适的子句和文字参与演绎推理. 子句选择策略主要依据不同的评估标准来选择最优子句进行推理,即从不同角度刻画子句特性,描述子句各种属性,根据选择方案确定当前推理过程中的最优子句. 目前,国际主流ATP采用的主要策略包括以下几种类型:

    1) 基于字符符号和“序”评估的策略[7,16]. 如基于重写规则的E中KBO (Knuth-Bendix order) 序方法对等词的有效处理[16]. 基于人为设定项的权重,KBO序是项重写的基础,可终止等词替换.

    2) 分层的子句选取策略. 如 GKC (graph knowledge core)中分层的子句选择策略[17]. 针对大知识库,GKC使用2层的子句选择方法,多个队列被用于选择子句,并赋予不同的优先级. 如第1层使用项总数排序和子句生成时间排序的队列,第2层使用4个队列.

    3) 基于二元归结的Vampire中动态调度策略[8,18]. Vampire实现了动态调用策略[18],给定策略优先级,优先使用最有可能成功的策略,如生成子句的文字数最小策略.

    由于上述ATP受推理机制的影响,在搜索空间中保留了大量含有较多文字数的归结式,所以上面的子句选择策略主要是为了避免搜索空间的迅速增长. 相比而言,基于S-CS规则的子句选择策略有明显不同. 针对S-CS规则的策略更倾向于全面的路径搜索,以充分发挥S-CS规则的动态演绎能力.

    基于子句的符号特征,提出以下子句选择策略:

    1) 子句的文字数:子句中包含的文字数目. 在演绎过程中,包含文字数较少的子句通常有更高的演绎推理效率. 因此,只含一个文字的单元子句必定参与演绎,其次选择文字数较少的非单元子句参与演绎.

    2) 子句函数项嵌套层数:子句的函数项嵌套层数越多,所涉及的替换越复杂,因此,选择函数项嵌套层数少的子句参与演绎,同时也控制生成的矛盾体分离式的函数项嵌套层数.

    3) 子句的负文字数:子句中包含的负文字数目. 在演绎过程中,包含负文字多的子句通常与结论密切相关,所以优先选择包含负文字多的子句参与演绎推理. 比如,最多只含一个正文字的Horn子句被优先选择. 特别地,优先选择只有负文字的负子句.

    4) 矛盾分离式的文字数:S-CSC包含的文字数目. 当矛盾体分离式为空子句时,ATP证明定理成功. 所以应该控制矛盾体分离式的文字数,如少于6个文字. 当矛盾体分离式的文字数不小于6个时,返回上一演绎步骤,重新选择子句构造矛盾体. 将生成的矛盾体分离式加入原始子句集,以构造新的子句集,直到演绎出空子句.

    在子句的使用次数方面,提出以下子句选择策略:

    1) 子句参与演绎的次数:每当子句参与一次演绎,其计数加 1,重复使用的子句会多次累计. 这一策略有效避免了演绎路径的局部最优和部分子句未参与推理的情况,确保路径搜索的全面性.

    2) 重复使用子句策略[19]:对子句集中的子句进行重复使用,并设置重复使用次数的阈值. 该策略确保充分使用子句的演绎能力,以搜索更多的演绎路径.

    本文根据S-CS规则的特点,为充分利用其优势,并体现 S-CS 演绎的以下特性:文字的可控性、子句的可重复性、协同性、灵活性、目标导向性,选取以下5种属性进行综合评估:子句的文字数、重复使用子句的次数、子句参与演绎的次数、子句函数项嵌套层数和子句的负文字数.

    MCDM方法中,确定属性权重主要有主观赋权法和客观赋权法2种方式. 属性权重对子句的最后排序影响较大,因此,为保证评估的客观性,选择客观赋权法更为合适. 常见的客观赋权方法包括标准离差法[20]、因子分析法[21]、熵权法[22]等. 其中,熵权法因应用广泛、计算和编程实现简单且精度较高而被广泛采用. 熵权法通过属性的离散程度直观地解释权重赋值,易与MCDM方法结合. 因此,本文采用熵权法确定属性权重. 其计算步骤如下:

    步骤1 给定1组候选子句SC={C1,C2,,Cm}和1组属性SG={G1,G2,,GM}M为属性个数). 其评价矩阵中的元素ciji=1,2,,m;j=1,2,,M是候选子句的各属性值.

    步骤2 将各属性的数据分类按式(1)进行归一化处理.

    dij={cijmincijmaxcijmincij,maxcijcijmaxcijmincij, (1)

    式中:dij为[0,1]之间的实数.

    若属性的属性值越大,对子句的评估表现越好,则该属性为正向属性;反之,为负向属性.

    步骤3 根据信息熵的定义,求各属性的熵. 第j个属性的熵值为

    ej=1lnmmi=1pijlnpij (2)

    式中:ej { {p}}_{ {ij}}={ {d}}_{ {ij}}\bigg/{\displaystyle\sum }_{ {i=} {1}}^{ {m}}{ {d}}_{ {ij}};当 { {p}}_{ {ij}} {=} {0} 时,定义 { {p}}_{ {ij}} {\ln}\;{ {p}}_{ {ij}} =0.

    步骤4 传统计算第j个属性的熵权wj如式(3)所示.

    { {w}}_{ {j}} = {(1}{ - {e}}_{ {j}} {)}\bigg/{\displaystyle\sum }_{ {j=} {1}}^{ {M}} {(1} -{ {e}}_{ {j}} {)} . (3)

    当各熵值 { {e}}_{ {j}} 趋于1且差异微小时,得到的熵权 { {w}}_{ {j}} 却差异很大. 因此,本文采用式(4)所示的改进熵权计算方法[23]确定属性权重.

    { {w}}_{ {j}} =\frac{ {1} -{ {e}}_{ {j}} { + } {0.1} {\displaystyle\sum }_{ {j} {=1}}^{ {M}}\left( {1-}{ {e}}_{ {j}}\right)}{{\displaystyle\sum }_{ {j=} {1}}^{ {M}}\left[ {1} -{ {e}}_{ {j}} { + } {0.1} {\displaystyle\sum }_{ {j} {=1}}^{ {M}}\left( {1-}{ {e}}_{ {j}}\right) {}\right]} {,} (4)

    式中: {\displaystyle\sum }_{ {j=} {1}}^{ {M}}{ {w}}_{ {j}} {=} {1} .

    步骤1 根据式(4)可得每个属性的熵权 { {w}}_{ {j}} .

    步骤2 计算每对候选子句在各属性下的差异值 \overline{{ {d}}_{ {j}}} {(}{ {C}}_{ {i}} {,}{ {C}}_{\bar { {r}}} {)} ,如式(5)所示. 其中, \bar { {r}}\in \{{{1} ,2{,\cdots,m} {}}\}.

    \overline{{ {d}}_{ {j}}}\left({ {C}}_{ {i}} {,}{ {C}}_{\bar { {r}}}\right) = { {g}}_{ {j}}\left({ {C}}_{ {i}}\right)-{ {g}}_{ {j}}\left({ {C}}_{\bar { {r}}}\right) {,} (5)

    式中: { {g}}_{ {j}} {(}{ {C}}_{ {i}} {)} { {g}}_{ {j}} {(}{ {C}}_{\bar { {r}}} {)} 分别为子句 { {C}}_{ {i}} { {C}}_{\bar { {r}}} 的第 {j} 个属性值.

    步骤3 选择合适的偏好函数. Brans等[14]提出6种含参数的偏好函数类型(V-shape、V-shape I、Level、U-shape、Usual 和Gaussian). 根据评估矩阵的信息,偏好函数选取V-shape,如式(6)所示,其中,参数 {q} 为每种属性的最大值. 因为不同的属性,其值域有明显差异,所以,不同的属性对应不同的参数. 本文同时也测试了其他参数以及其他类型的偏好函数,如Usual类型的偏好函数,研究发现式(6)的效果最好. 因此,选择式(6)作为本文的偏好函数.

    {P}_{j}\left({ {C}}_{ {i}},{ {C}}_{\bar { {r}}}\right)=\left\{\begin{array}{l} {0} {,}\quad \overline{{ {d}}_{ {j}}}\left({ {C}}_{ {i}} {,}{ {C}}_{\bar { {r}}}\right) {\leqslant } {0},\\ \overline{{ {d}}_{ {j}}}\left({ {C}}_{ {i}} {,}{ {C}}_{\bar { {r}}}\right)/ {q} {,} \quad {0} { < }\overline{{ {d}}_{ {j}}}\left({ {C}}_{ {i}} {,}{ {C}}_{\bar { {r}}}\right) {\leqslant } {q},\\ {1} {,}\quad \overline{{ {d}}_{ {j}}}\left({ {C}}_{ {i}} {,}{ {C}}_{\bar { {r}}}\right) { > } {q}.\end{array}\right. (6)

    偏好函数 { {P}}_{ {j}}\left({ {C}}_{ {i}} {,}{ {C}}_{\bar { {r}}}\right) 表示在第 {j} 个属性上子句 { {C}}_{ {i}} 优先于 { {C}}_{\bar { {r}}} 的程度,取值范围为 [0,1].

    步骤4 定义并计算每一对候选子句的偏好指数,偏好指数 {\pi }\left({ {C}}_{ {i}} {,}{ {C}}_{\bar { {r}}}\right) 表示在所有属性上, { {C}}_{ {i}} 超过 { {C}}_{\bar { {r}}} 的偏好度. 对于任意的 \bar { {r}}、 {i}{,} {\pi }\left({ {C}}_{ {i}} {,}{ {C}}_{\bar { {r}}}\right) 的定义如式(7)所示,取值范围为 [0, 1].

    {\pi }\left({ {C}}_{ {i}} {,}{ {C}}_{\bar { {r}}}\right) ={{\displaystyle\sum }}_{ {j=} {1}}^{ {M}}{ {P}}_{ {j}}\left({ {C}}_{ {i}} {,}{ {C}}_{\bar { {r}}}\right){ {w}}_{ {j}} {.} (7)

    步骤5 定义和计算正负优先流.

    \mathrm{正优先流}:\varphi^{ + }\left(C_{{i}}\right)=\frac{1}{{{n}}-1} {\sum}_{\bar{r}=1}^n \pi\left({{C_{{i}}}}, {{C_{\bar{r}}}}\right), (8)
    负优先流: { {\varphi }}^- {(}{ {C}}_{ {i}} {)} =\frac{ {1}}{ {n}- {1}}{\displaystyle\sum }_{\bar { {r}} = {1}}^{ {n}} {\pi }\left({ {C}}_{\bar { {r}}} {,}{ {C}}_{ {i}}\right) {,} (9)

    正优先流 { {\varphi}}^{ { + }} {(}{ {C}}_{ {i}} {)} 表示 { {C}}_{ {i}} 优于其他候选子句的程度; { {\varphi }}^{ { + }} {(}{ {C}}_{ {i}} {)} 越大,子句越优. 负优先流 { {\varphi }}^{-} {(}{ {C}}_{ {i}} {)} 表示 { {C}}_{ {i}} 劣于其他候选子句的程度; { {\varphi }}^{-} {(}{ {C}}_{ {i}} {)} 越小,子句越优. { {\varphi }}^{ { + }} {(}{ {C}}_{ {i}} {)} { {\varphi }}^{-} {(}{ {C}}_{ {i}} {)} 取值范围为[0, 1].

    步骤6 计算候选子句的净占优流.

    净占优流 {\varphi } {(}{ {C}}_{ {i}} {)} 表示子句的综合优先值, {\varphi } {(}{ {C}}_{ {i}} {)} 越大,子句越优, {\varphi } {(}{ {C}}_{ {i}} {)} 取值范围为[−1, 1],如式(10)所示.

    {\varphi } {(}{ {C}}_{ {i}} {)} ={ {\varphi }}^{ { + }} {(}{ {C}}_{ {i}} {)}-{ {\varphi }}^- {(}{ {C}}_{ {i}} {)} {.} (10)

    步骤7 对候选子句按净占优流的值从大到小进行排序.

    基于PROMETHEE Ⅱ方法的候选子句选择框架如图1所示. 本文只对5个属性进行评估,根据图1中的计算流程,得出候选子句的完全排序.

    图  1  基于 PROMETHEE Ⅱ的候选子句选择框架
    Figure  1.  Framework diagram for candidate clause selection based on PROMETHEE Ⅱ

    目前,基于S-CS规则研发了多个自动定理证明器,如MC-SCS (multi-clause synergized contradiction separation) [24]和CSE (contradiction separation extension)[25]等. 其中,CSE从2018年开始一直参加国际竞赛CADE (Conference on Automated Deduction) [25]. 为继续提高CSE的性能,本文将MCDM方法应用到CSE 1.5自动定理证明器,记作MCDM_CSE,其流程如图2所示.

    图  2  基于 PROMETHEE Ⅱ的 S-CS 算法流程
    Figure  2.  Flowchart of S-CS algorithm based on PROMETHEE Ⅱ

    将基于MCDM方法的S-CS演绎算法流程中选择的第一个参与矛盾体分离演绎的子句称为起步子句. 根据S-CS演绎时间决定是否使用新的PROMETHEE Ⅱ方法评估子句,如每隔20 s使用PROMETHEE Ⅱ方法评估子句.

    基于S-CS规则的PROMETHEE Ⅱ子句评估方法的主要优势如下:1) MCDM方法可组合多种子句属性,评估出当前演绎步骤中的最优子句. 相比优先级子句选择方法,MCDM方法更高效,对子句评估更灵活. 2) 可增加、删减、更换属性.属性的选取非常重要,所选属性的数量会直接影响评价矩阵,从而影响对子句的评估结果. 3) 克服主观因素对权重的影响. 采用熵权法客观确定属性权重,有效避免了人为因素的影响. 针对不同的子句集,其评价矩阵不同,因此相应属性权重也不同. 4) 使用多属性决策方法的次数可动态调整,可控性更强. 随着演绎过程中属性值的动态变化,更新评价矩阵,再动态使用多属性决策方法.

    本文对2022年国际竞赛CADE 中FOF (First-Order Form) 组的500个定理和TPTP-v8.1.0 (Thousands of Problems for Theorem Provers)[26]问题库中FOF格式的9091个定理以及最难的定理进行证明. TPTP问题库中每个定理对应一个rating值参数,代表定理的难度等级. 定理的难度等级是[0, 1]中的实数,rating = 0的定理能被所有自动定理证明器证明,rating = 1的定理目前不能被任何自动定理证明器证明. TPTP问题库也对每个定理进行了分类,如SET表示集合论定理,SWV表示软件验证类的定理. 为评估本文多属性决策方法的有效性,该方法被加入到Vampire 4.7[27]和Eprover (E 2.6)[28],自动定理证明器记作MCDM_V 和MCDM_E.

    实验硬件环境为3.4 GHz Inter (R) Core (TM) i7-6700处理器,11.1GB内存,操作系统为Ubuntu15.04 64位. 证明每个定理的时间为国际竞赛标准时间300 s. 本文所有的自动定理证明器在相同的测试环境下进行测试. Prover9[29] 和Otter[30]均可检查证明过程的正确性,而Prover9自动定理证明器是在Otter自动定理证明器基础上改进的,并一直参与国际竞赛,所以Prover9作为本实验S-CS演绎过程的验证工具.

    MCDM_CSE自动定理证明器证明的定理个数为2586个,比CSE 1.5多证明151个. 其中,CSR、GEO、SET、NUM、SEU、SWV、KRS、SWC和SYN这9类定理的证明数量均超过 100 个. 分析实验数据发现,除SYN以外,其他8类定理的证明个数在MCDM_CSE中均超过CSE 1.5,尤其是NUM多证明了38个. 因此,MCDM_CSE比CSE 1.5的性能更好. 特别地,CSR、GEO、SET、NUM、SEU这5类定理证明的个数均不低于200个.

    MCDM_CSE和CSE 1.5在不同难度等级下证明的定理数量对比如表1所示. 每个定理的证明时间均在300 s内,MCDM_CSE证明的数量比CSE 1.5多151个. 当rating值不低于0.1时,MCDM_CSE证明的定理数量均超过了CSE 1.5,表明MCDM_CSE的能力优于CSE 1.5.PROMETHEE Ⅱ方法能有效提升CSE 1.5的性能.

    表  1  MCDM_CSE和CSE 1.5在不同难度等级下证明的定理数量对比
    Table  1.  Comparison of the number of theorems proved by MCDM_CSE and CSE 1.5 at different difficulty levels
    难度等级 MCDM_CSE CSE 1.5
    [0, 0.10) 1061 1073
    [0.10,0.50) 1338 1212
    [0.50,0.60) 98 79
    [0.60,0.70) 43 39
    [0.70,0.80) 22 16
    [0.80,0.90) 13 11
    [0.90,1.00) 8 5
    1.00 3 0
    下载: 导出CSV 
    | 显示表格

    分析结果表明,多属性决策子句评估方法发挥了关键作用. 对于CSE 1.5不能证明的151个定理,多属性决策方法能缩短定理判定的总时间,使得这些定理能在300 s内被MCDM_CSE证明. 在证明定理效率方面,CSE 1.5的平均时间为26.19 s,而MCDM_CSE平均时间为25.24 s. 相比CSE 1.5, MCDM_CSE提高了1540个定理的证明效率.

    表2列出6个被MCDM_CSE证明但未被CSE 1.5证明的定理,这些定理的难度等级均大于 0.90,平均证明时间为132.34 s. 这表明 MCDM_CSE 对较难定理的证明具有良好表现. 尤其值得注意的是,其中有 3 个定理的难度等级为 1.00,目前尚无其他 ATP 能证明这些定理.

    表  2  MCDM_CSE证明难度大于0.90的定理所需的证明时长
    Table  2.  Time consumed by MCDM_CSE to prove theorems with difficulty greater than 0.90
    定理名称 难度等级 证明时间/s
    SEU413 + 2 0.92 26.81
    SWB088 + 1 0.97 137.78
    SWB090 + 1 0.97 126.04
    NUM736 + 4 1.00 65.49
    SYO625-1 1.00 219.51
    SYO587 + 1 1.00 218.41
    下载: 导出CSV 
    | 显示表格

    表3为MCDM_CSE已证明的2586个定理在国际知名自动定理证明器中的对比情况. Vampire 自 2002 年起一直是国际自动定理证明器竞赛 (FOF 组) 的冠军,E 多年稳居亚军或季军,而 Prover9 被广泛视为衡量 ATP 能力的基准自动定理证明器. 因此,本文选取这3个证明器作为比较对象. 结果显示,Vampire 4.7有5个定理不能证明, E 2.6有41个定理不能证明, Prover9有293个定理不能证明.

    表  3  对已证明定理(按难度等级)在国际知名自动定理证明器中证明数量的比较
    Table  3.  Comparison of the number of theorems (by difficulty level) proved by internationally known ATPs
    自动定理证
    明器
    难度等级
    [0,0.70) [0.70,0.80) [0.80,0.90) [0.90,1.00]
    MCDM_CSE 2540 22 13 11
    Vampire 4.7 2539 21 13 8
    E 2.6 2532 12 1 0
    Prover9 2264 13 8 8
    下载: 导出CSV 
    | 显示表格

    为进一步评估多属性决策方法的有效性,本文测试了2022年CADE竞赛的500个竞赛例,测试的自动定理证明器为MCDM_V、 MCDM_E、Vampire 4.7和E 2.6.

    表4为各自动定理证明器在2022年CADE竞赛的比较结果. MCDM_V 证明了462个定理,比Vampire 4.7多6个. MCDM_E证明了387个定理,比E 2.6多7个. 因此,本文的多属性决策评估子句的方法能有效地评估子句,能提高Vampire 4.7和E 2.6的能力. 在效率方面,MCDM_V证明462个定理的平均时间为15.30 s,比Vampire 4.7少0.80 s. MCDM_E证明387个定理的平均时间为27.40 s,比E 2.6少4.30 s. 实验表明,多属性决策评估子句方法能节省子句评估时间.

    表  4  2022年CADE竞赛的比较结果
    Table  4.  Comparative results on the CADE 2022 competition
    自动定理证明器 平均时间/s 证明个数/个
    MCDM_V 15.3 462
    Vampire 4.7 16.1 456
    MCDM_E 27.4 387
    E 2.6 31.7 380
    下载: 导出CSV 
    | 显示表格

    图3表示在300 s内每个自动定理证明器证明定理的实验结果,横轴表示证明的定理个数,纵轴表示证明定理所需的CPU时间. 从图3可以看出,在相同时间内(同一水平线),MCDM_E的曲线几乎在E 2.6的右边或与E 2.6重合,MCDM_V的曲线几乎在Vampire 4.7的右边或与Vampire 4.7重合. 并且通过分析实验数据发现,相比E 2.6,MCDM_E提高了证明79个定理的效率;相比Vampire 4.7, MCDM_V提高了28个定理的效率. 因此,多属性决策方法能提高自动定理证明器的能力和效率.

    图  3  不同ATP在2022年CADE竞赛的CPU时间比较
    Figure  3.  Comparison of CPU time of different ATPs for the CADE 2022 competition

    为削弱主观因素对子句评估的影响,通过充分利用多种子句属性信息对子句进行客观评估,本文提出一种用于动态综合评估子句的多属性决策方法.实验结果表明,本文提出的方法能提高自动定理证明器的性能,主要贡献如下:

    1) 本文提出一种新的子句选择方法,结合S-CS规则的特性,应用PROMETHEE Ⅱ方法得到子句的完全排序,从而选择最优的候选子句参与S-CS演绎.

    2) 针对PROMETHEE Ⅱ方法中属性权重的确定,采用熵权法(客观赋权法)计算属性权重,避免人为因素造成偏差.

    3) 将PROMETHEE Ⅱ方法应用到自动定理证明器CSE 1.5、Vampire 4.7和E 2.6中. 实验表明,该方法有效提高了证明器的性能,尤其在子句的选择方面发挥重要作用,能更精确地评估子句,有利于子句的选择.

    4) 针对多个属性值相同的子句,PROMETHEE Ⅱ方法可以进行完全排序,从而选择更适合的子句参与S-CS演绎,有效避免按照优先级对子句进行多次比较.

    综上所述,多属性决策子句评估方法均能提高CSE 1.5、Vampire 4.7和E 2.6的性能,但仍有一些不足之处可改进. 如可以按照TPTP库的定理类型进行评估,以及增加对文字的评估.

  • 图 1  环形Halbach阵列永磁轮

    Figure 1.  Annular Halbach permanent magnet wheel

    图 2  常规永磁轮与偏转永磁轮示意

    Figure 2.  Conventional permanent magnet wheel and deflecting permanent magnet wheel

    图 3  永磁电动悬浮汽车原理样机结构示意

    Figure 3.  PMEDS vehicle prototype structure

    图 4  系统横向运行原理

    Figure 4.  Principle of lateral motion of system

    图 5  NMPC-ESO-EKF控制器结构

    Figure 5.  NMPC-ESO-EKF controller structure

    图 6  定常数轨迹跟踪控制系统响应

    Figure 6.  System response of constant trajectory tracking control

    图 7  外部扰动信号

    Figure 7.  External disturbance signal

    图 9  ESO扰动观测值

    Figure 9.  Disturbance observation value of ESO

    图 8  外部扰动条件下的系统响应

    Figure 8.  System response under external disturbance

    图 10  内外部扰动条件下系统响应

    Figure 10.  System response under internal and external disturbance

    图 11  EKF滤波估计仿真结果

    Figure 11.  Simulation results of EKF estimation

    图 12  实验平台结构

    Figure 12.  Experimental platform structure

    图 13  EKF滤波估计实验结果

    Figure 13.  Experimental results of EKF estimation

    图 14  小距离定常数轨迹跟踪控制系统响应

    Figure 14.  System response of short-distance constant trajectory tracking control

    图 15  方波信号轨迹跟踪控制系统响应

    Figure 15.  System response of square wave signal trajectory tracking control

    图 16  大距离定常数轨迹跟踪控制系统响应

    Figure 16.  System response of long-distance constant trajectory tracking control

    表  1  永磁电动悬浮汽车模型参数

    Table  1.   Model parameters of PMEDS vehicle

    编号 参数 数值
    整车
    参数
    整车质量m/kg
    悬浮间隙h/mm
    横向阻尼系数c/(N·s·m−1
    18.1
    10
    17.2
    磁轮
    参数
    极对数P
    外径Ro/mm
    内径Ri/mm
    宽度d/mm
    磁化角q
    磁轮转速n0/rpm
    磁轮磁阻力Fr0/N
    4
    50
    32.5
    35
    90
    2000
    17.33
    磁轮偏转角度范围α −20~20
    下载: 导出CSV

    表  2  系统响应结果对比

    Table  2.   Comparison of system response results

    控制器 0~12 s 12 s后
    平均误差/mm 性能提升/% 平均误差/mm 性能提升/%
    NMPC 71.31 34.41
    NMPC-ESO 319.54 −348.10 183.07 −432.03
    NMPC-EKF 57.99 18.70 6.12 82.20
    NMPC-ESO-EKF 57.93 18.76 3.52 89.77
    下载: 导出CSV

    表  3  方波信号轨迹跟踪控制系统响应结果对比

    Table  3.   Comparison of system response results of square wave signal trajectory tracking control mm

    控制器 平均跟踪误差 平均超调量
    PID-EKF 57.60 164.96
    MPC-EKF 38.48 20.48
    NMPC-EKF 36.82 15.69
    NMPC-ESO-EKF 36.79 10.27
    下载: 导出CSV

    表  4  大距离定常数轨迹跟踪控制系统响应结果对比

    Table  4.   Comparison of system response results of long-distance constant trajectory tracking control

    控制器 位移波动幅值/mm 恢复时间/s
    PID-EKF 40.89 6.82
    MPC-EKF 45.39 10.46
    NMPC-EKF 35.73 6.80
    NMPC-ESO-EKF 26.78 3.95
    下载: 导出CSV
  • [1] LIU B, SUN C, WANG B, et al. Adaptive speed planning of connected and automated vehicles using multi-light trained deep reinforcement learning[J]. IEEE Transactions on Vehicular Technology, 2022, 71(4): 3533-3546. doi: 10.1109/TVT.2021.3134372
    [2] 邓自刚,刘宗鑫,李海涛,等. 磁悬浮列车发展现状与展望[J]. 西南交通大学学报,2022,57(3): 455-474,530.

    DENG Zigang, LIU Zongxin, LI Haitao, et al. Development status and prospect of maglev train[J]. Journal of Southwest Jiaotong University, 2022, 57(3): 455-474,530.
    [3] 林国斌,刘万明,徐俊起,等. 中国高速磁浮交通的发展机遇与挑战[J]. 前瞻科技,2023,2(4): 7-18.

    LIN Guobin, LIU Wanming, XU Junqi, et al. Opportunities and challenges for the development of high-speed maglev transportation in China[J]. Science and Technology Foresight, 2023, 2(4): 7-18.
    [4] 赵春发,刘浩东,冯洋,等. 五位姿参数下车载永磁体与永磁轨道之间的磁力特性研究[J]. 西南交通大学学报,2024,59(4): 804-811.

    ZHAO Chunfa, LIU Haodong, FENG Yang, et al. Magnetic force characteristics between on-board permanent magnet and permanent magnetic rail considering five pose parameters[J]. Journal of Southwest Jiaotong University, 2024, 59(4): 804-811.
    [5] 胡永攀,曾杰伟,王志强,等. 超高速永磁电动悬浮系统性能优化[J]. 西南交通大学学报,2023,58(4): 773-782.

    HU Yongpan, ZENG Jiewei, WANG Zhiqiang, et al. Performance optimization of ultra-high speed permanent magnet electrodynamic suspension system[J]. Journal of Southwest Jiaotong University, 2023, 58(4): 773-782.
    [6] QIN W, BIRD J Z. Electrodynamic wheel magnetic rolling resistance[J]. IEEE Transactions on Magnetics, 2017, 53(8): 8107407.1-8107407.7.
    [7] SHI H F, KE Z H, ZHENG J, et al. An effective optimization method and implementation of permanent magnet electrodynamic wheel for maglev car[J]. IEEE Transactions on Vehicular Technology, 2023, 72(7): 8369-8381. doi: 10.1109/TVT.2023.3245620
    [8] WRIGHT J D. Modeling, analysis, and control of a radial electrodynamic wheel vehicle and analysis of an axial electrodynamic wheel[D]. Charlotte: The University of North Carolina at Charlotte, 2019.
    [9] FUJII N, NONAKA S, HAYASHI G. Design of magnet wheel integrated own drive[J]. IEEE Transactions on Magnetics, 1999, 35(5): 4013-4015. doi: 10.1109/20.800739
    [10] FUJII N, HAYASHI G, SAKAMOTO Y. Characteristics of magnetic lift, propulsion and guidance by using magnet wheels with rotating permanent magnets[C]//Conference Record of the 2000 IEEE Industry Applications Conference. Thirty-Fifth IAS Annual Meeting and World Conference on Industrial Applications of Electrical Energy. Rome: IEEE, 2002: 257-262.
    [11] JUNG K S. Parametric design of contact-free transportation system using the repulsive electrodynamic wheels[J]. Journal of the Korea Academia-Industrial Cooperation Society, 2016, 17(3): 310-316. doi: 10.5762/KAIS.2016.17.3.310
    [12] JUNG K S. Transfer system using radial electrodynamic wheel over conductive track[J]. The Korea Academia-Industrial Cooperation Society, 2017, 18(11): 794-801.
    [13] 刘新,邓自刚,梁乐,等. 基于斜置环形Halbach永磁轮的磁浮列车“悬浮-导向-推进” 一体化方案设计[J]. 机车电传动,2023(2): 90-96.

    LIU Xin, DENG Zigang, LIANG Le, et al. Levitation-guidance-propulsion integrated design for maglev trains based on oblique ring Halbach permanent magnet wheels[J]. Electric Drive for Locomotives, 2023(2): 90-96.
    [14] ZHANG Z, DENG Z G, ZHANG S, et al. Design and operating mode study of a new concept maglev car employing permanent magnet electrodynamic suspension technology[J]. Sustainability, 2021, 13(11): 5827.1-5827.20.
    [15] 徐俊起,林国斌,荣立军,等. 中低速磁浮列车悬浮控制技术成果及应用[J]. 铁道技术标准(中英文),2022(10): 34-39.

    XU Junqi, LIN Guobin, RONG Lijun, et al. Research achievements and application of levitation control technology for medium-low speed maglev train[J]. Railway Technical Standard (Chinese & English), 2022(10): 34-39.
    [16] DE BOEIJ J, STEINBUCH M, GUTIERREZ H. Real-time control of the 3-DOF sled dynamics of a null-flux maglev system with a passive sled[C]//2006 IEEE International Symposium on Industrial Electronics. Montreal: IEEE, 2006: 2549-2555.
    [17] ZHANG B J, KE Z H, LI Z Y, et al. Yawing stability and manipulative approach design for maglev car based on active disturbance rejection control[J]. Asian Journal of Control, 2024, 26(2): 1003-1016. doi: 10.1002/asjc.3246
    [18] LI Z Y, KE Z H, SHI J H, et al. Investigation of RBF-SMC control strategy for vertical dynamics of maglev car considering temperature rise effects[J/OL]. IEEE Transactions on Intelligent Vehicles, 2024, 3456784.1-3456784.14(2024-09-10)[2024-09-28]. https://ieeexplore.ieee.org/document/10670497.
    [19] BIRD J, LIPO T A. Characteristics of an electrodynamic wheel using a 2-D steady-state model[J]. IEEE Transactions on Magnetics, 2007, 43(8): 3395-3405. doi: 10.1109/TMAG.2007.900572
    [20] BIRD J, LIPO T A. Calculating the forces created by an electrodynamic wheel using a 2-D steady-state finite-element method[J]. IEEE Transactions on Magnetics, 2008, 44(3): 365-372. doi: 10.1109/TMAG.2007.913038
    [21] PAUL S, BIRD J Z. A 3-D analytic eddy current model for a finite width conductive plate[J]. COMPEL: the International Journal for Computation and Mathematics in Electrical and Electronic Engineering, 2013, 33(1/2): 688-706. doi: 10.1108/COMPEL-03-2013-0083
    [22] 闫玉盼,饶兵,刘砚菊,等. 基于非线性模型预测的四旋翼无人机轨迹跟踪控制[J]. 沈阳理工大学学报,2024,43(1): 36-43,49.

    YAN Yupan, RAO Bing, LIU Yanju, et al. Trajectory tracking control of quadrotor based on nonlinear model predictive control[J]. Journal of Shenyang Ligong University, 2024, 43(1): 36-43,49.
    [23] KAMEL M, ALEXIS K, ACHTELIK M, et al. Fast nonlinear model predictive control for multicopter attitude tracking on SO(3)[C]//2015 IEEE Conference on Control Applications (CCA). Sydney: IEEE, 2015: 1160-1166.
    [24] 许鹏,邢伯阳,刘宇飞,等. 基于扩张状态观测器和模型预测方法的四足机器人抗干扰复合控制[J]. 兵工学报,2023,44(增2): 12-21.

    XU Peng, XING (Bai| Bo)(Yang), LIU Yufei, et al. Anti-disturbance composite controller design of quadruped robot based on extended state observer and model predictive control technique[J]. Acta Armamentarii, 2023, 44(S2): 12-21.
    [25] HAN J Q. From PID to active disturbance rejection control[J]. IEEE Transactions on Industrial Electronics, 2009, 56(3): 900-906. doi: 10.1109/TIE.2008.2011621
    [26] 王天威,黄军魁. 控制之美(卷2): 最优化控制MPC与卡尔曼滤波[M]. 北京:清华大学出版社,2023.
    [27] REIF K, UNBEHAUEN R. The extended Kalman filter as an exponential observer for nonlinear systems[J]. IEEE Transactions on Signal Processing, 1999, 47(8): 2324-2328. doi: 10.1109/78.774779
    [28] LI J, XIA Y Q, QI X H, et al. On convergence of the discrete-time nonlinear extended state observer[J]. Journal of the Franklin Institute, 2018, 355(1): 501-519. doi: 10.1016/j.jfranklin.2017.11.019
    [29] 陈松林,王鑫,何宗儒. 一种兼顾带宽拓展和噪声抑制的ESO参数整定方法[J]. 控制与决策,2018,33(10): 1908-1914.

    CHEN S L, WANG X, HE Z R. A parameter tuning method for extended state observer with balance of bandwidth expansion and noise suppression[J]. Control and Decision, 2018, 33(10): 1908-1914.
    [30] 郭永飞,张荣彬,姚植元,等. 基于ESO-MPC的核电厂协调系统优化控制研究[J]. 核动力工程,2024,45(6): 178-184.

    GUO Yongfei, ZHANG Rongbin, YAO Zhiyuan, et al. Research on optimization control of nuclear power plant coordination system based on ESO-MPC[J]. Nuclear Power Engineering, 2024, 45(6): 178-184.
    [31] HUANG R, PATWARDHAN S C, BIEGLER L T. Robust stability of nonlinear model predictive control based on extended Kalman filter[J]. Journal of Process Control, 2012, 22(1): 82-89. doi: 10.1016/j.jprocont.2011.10.006
  • 加载中
图(16) / 表(4)
计量
  • 文章访问数:  13
  • HTML全文浏览量:  11
  • PDF下载量:  3
  • 被引次数: 0
出版历程
  • 收稿日期:  2024-09-28
  • 修回日期:  2025-01-05
  • 网络出版日期:  2025-03-15

目录

/

返回文章
返回