基于约束的混合系统建模语言HydLa及其符号实现HyLaGI

可在www.sciencedirect.com在线获取理论计算机科学电子笔记317（2015）109-115www.elsevier.com/locate/entcsHyLaGI：混合约束语言HydLa的符号实现Shota Matsumoto，FumihikoKono，Teruya Kobayashi和KazunoriUeda1早稻田大学日本东京摘要描述了一种混合系统建模语言HydLa及其实现方法HyLaGI。HydLa是一种基于约束的语言，可以平滑地处理模型的不确定性。HyLaGI通过符号公式操作计算轨迹，以排除由浮动点算法产生的误差。HyLaGI具有非确定性仿真算法，因此它可以计算具有不确定性的模型的所有可能的定性不同轨迹。保留字：混杂系统，严格仿真，约束，符号计算1一种基于约束的语言HydLa可靠性是混杂系统计算中的一个关键问题，定量的误差很容易导致定性的错误结果。考虑到这一点，我们开发了HydLa [12]，一种用于混合系统[8]的基于约束的建模语言HydLa的主要特点是约束被用作定义系统连续和离散行为的唯一机制。约束包括常微分方程和实数上的时态逻辑公式，以及表达条件和同步的逻辑蕴涵。HydLa的前身是Hybrid cc [2，5]，但其实现并不能完全保证结果的正确性。另一种方法是CLP（F）[7]，实值函数上的约束逻辑编程它的目标是严格的仿真和处理区间约束，但它的控制结构与HydLa非常不同。1电邮地址：{matsusho，kouno，teruya，ueda}@ ueda.info.waseda.ac.jphttp://dx.doi.org/10.1016/j.entcs.2015.10.0111571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。110S. Matsumoto et al. /Electronic Notes in Theoretical Computer Science 317（2015）109INIT<=> y=10/\y'=0/\x=0/10< x' =20<。FALL => [] （ y“=-10 ） 。BOUNCE< =>[]（y-=-7\/（（x-<=7\/x->=10）/\y-=0）=>y ' =-4/5* y'-）。XCONST<=>[]（XBOUNCE =>[]（（x-=7\/x-=10）/\y- 0=>初始化，落弹，XCONST XBOUNCE。Fig. 1. 一个在HydLa图二. 一个在洞HydLa允许以约束层次结构的形式为各个约束分配优先级[1]。约束层次结构中的基本单元称为约束模块。如果HydLa程序中的某些约束模块不一致，则采用具有高优先级的约束。换句话说，约束层次的含义是满足优先级的约束模块的候选集合有了这个特性，程序员HydLa程序的声明性语义[12]是一组轨迹，这些轨迹在每次都满足最大一致候选集之一HydLa中的2个示例程序图1是一个HydLa程序，它模拟了一个围绕着一个洞反弹的粒子（图1）。2）。变量x和y表示粒子的位置。HydLa中的每个变量都是时间的函数，例如，x表示x（t）。该程序包括五个约束模块INIT、FALL、BOUNCE、XCONST和XBOUNCE。INIT表示模型的初始状态。运算符用两个不等式描述xFALL代表重力下落。运算符[]是时态逻辑中的“always”运算符，意味着约束在 当前时间BOUNCE表示粒子的垂直反弹。运算符BOUNCE的右边说，如果颗粒到达孔的底部（y =-7）或孔周围的地面。孔（（x-=7 \/ x- >=10）/\ y- =0），垂直速度乘以-4/5。XCONST表示水平速度是恒定的。XBOUNCE表示孔壁上的水平反弹。下面一行声明了这个程序的约束层次：FALL弱于BOUNCE，XCONST弱于XBOUNCE。当球到达地面或球洞时，FALL或XCONST与BOUNCE或XBOUNCE发生碰撞，导致前者暂时从模块组中移除。HydLa最近推出了列表解析，以简洁地描述具有多个对象的模型。图3是一个带有列表解析的示例程序。该程序包括初始状态、碰撞和匀速运动三个约束模块INIT、COL、CONST。X是变量列表，S. Matsumoto et al. /Electronic Notes in Theoretical Computer Science 317（2015）109111INIT（b，b0，vb0）<=> b = b0/\b ' = v b 0 。COL（b1，b2）<=>[]（b1-= b2- => b1 &' = b2'- b2' = b1'-）。CONST（b）<=> []（b “ = 0 ）.X ：={x0..x9}。init：={INIT（X[i]，2*i-2，0）|iin {2..| X|}}。COL_HIERARCHY：={（CONST（X[i]），CONST（X[j]））<2^（1/2）x： t*p[x，1，1]y：（t^2+（-2））*（-5）y’:y’’:(The以下阶段省略）--参数条件-p[x，1，1]：（0，2^（-1/2）*7）图五. HyLaGI的输出（片段）算法模拟重复点相位和间隔相位，直到满足终止条件（时间限制或相位数）。在每个阶段，通过检查一致性和保护条件来计算模块的最大一致集点阶段涉及时间点的离散变化，而间隔阶段涉及时间间隔的连续变化。区间相位的计算比点相位的计算更复杂，因为它包括求解常微分方程和极小化问题。为了象征性地模拟不确定模型，HyLaGI使用符号参数来表示某些时间点变量的不确定值。 图5是图1程序的HyLaGI输出样本。IP 2代表第二间隔相位，符号参数p[x，1，1]代表初始水平速度。这个输出表示可以通过实例化p[x，1，1]获得的无限多个连续轨迹。请注意，符号参数表示的不确定性可能导致轨迹的定性差异。当出现这种差异时，HyLaGI自动执行案例分析，将参数范围缩小到每个定性差异案例中。案例分析可能发生在图4中的所有框中，但在大多数模型中，它发生在下一个离散变化的计算中，因为参数条件与离散变化的顺序和数量密切相关3.2案例分析实例作为一个例子，我们展示了模拟结果的模型图。 一个断言ASSERT（！（y>=0 /\x>=10）），这说明粒子永远不会超过空穴。时间限制设置为20个单元，相数限制为13个。我们以初始水平速度的参数条件的形式得到了反例，如表1所示。表中的每一行对应于每种定性不同的情况。每种情况下的条件表示的符号和数字的初始水平速度必须属于的间隔。请注意，HyLaGI4HyLaGI的可扩展性符号技术的一个关注点是它的可扩展性。HydLa的简单实现将导致计算每个阶段的所有约束，但S. Matsumoto et al. /Electronic Notes in Theoretical Computer Science 317（2015）109113√√表1球出洞的参数条件弹跳顺序符号表示数值表示[1250/（4052 + 317 + 91387），地板，地板，底部1250/（405<$2−<$317 +9<$1387）][1. 36027，1. 40428][125/1997，35/（13/12）][1. 82244，1. 90375]（35/（13×2），地板，底部右下角，左下角，右（11252 + 225 67 + 25197）/（928 +81134）][-40 197/（928 + 81134）+360（52+67）][105/ 17，10 5/ 17]（10分5/ 17，（9分85+485）/16）（1. 90375，2. 02803][2. 64300，2. （71964）HyLaGI仅计算与每个离散变化相关的约束。这种改进基于以下三个想法。第一个想法是分析约束的依赖性。 的依赖性可以用变量节点和约束节点组成的二分图表示。图形边对应于约束中变量的引用。在HyLaGI的模拟中，约束之间的依赖性动态地改变，因为（i）受保护的约束可以被打开和关闭，（ii）未被选择用于特定阶段的约束HyLaGI动态地管理依赖图的节点和边的有效性，并计算相关约束的最小集合第二个想法是利用变量及其导数值的连续性。值跳跃的变量必须在触发离散变化的约束中引用，HyLaGI保持其他变量连续变化而不重新计算。第三种思想是动态计算约束模块的候选子集。在HydLa中，候选子集的数量可以相对于模型中对象的数量呈指数增长例如，对于具有n个球的图3的程序，它是2n然而，要检查其最大值的子集的数量通常很小。HyLaGI通过使用在一致性检查过程中获得的不一致子集的信息来按需计算这样的当已知子集不一致时，必须从子集中删除至少一个模块以使其一致，HyLaGI删除低优先级模块M和约束层次中低于M这些改进降低了计算每个离散变化的时间复杂度例如，对于图3的程序，它从指数（没有第三个想法）或O（n3）（有第三个想法）减少到O（n）。埃塞尔穆尔/（928 + 81134），252/ 13）[25[2013年2月，2012年7月][2. 71964，4. 94975]下，右，左下+右，左((11785 + 13485）/256，105/ 17）（5. 33196，5. （42326）[5. 42326，5. 42326]右下左（5. 42326，6. 56241]不得打球[2019-05 -20][7. 07107， 20]114S. Matsumoto et al. /Electronic Notes in Theoretical Computer Science 317（2015）1095目前和今后工作我们的经验表明，HyLaGI的符号方法与约束语言HydLa表现出极大的相似性，原则上工作良好，并带来了几个有趣的优点，总结如下：• 严格的模拟，可以扩展到无限的长度和验证，• 参数条件的自动按需案例分析，以及• 多个参数之间的关系的计算和维护（参见，包装效果[11]）。另一方面，我们发现HyLaGI的当前限制因素是最小化问题求解器（图4的第三个框）的能力和效率，该求解器可能使用Mathematica中的量化消除：随着模拟的进行，公式可能变得复杂，最终变得不可解。为了处理这些情况，我们开始将区间算法集成到HyLaGI的符号模拟中。区间是约束的一种特殊形式，在符号方法中表现出完美的一致性。即使当状态可以被严格地表示时，有时使用区间来近似它们也是有用的;这是一个权衡的问题我们正在实现区间牛顿法来可靠地解决最小化问题和复杂符号公式的区间近似。将区间算术集成到符号模拟中，预计会比相反的方向更平滑。符号方法的另一个局限性是， 非线性常微分方程不能用符号来解决。在这里，我们再次可以通过数值方法对解进行过近似，并将近似解视为带参数的公式，这是我们未来的工作。我们希望HyLaGI能够在表现出微妙行为并需要仔细分析的应用中找到自己的位置。引用[1] Borning，A.，Freeman-Benson，B. Wilson，M.约束层次结构，Lisp和符号计算，卷。号53，1992，pp.223-270[2] 卡尔森湾，澳-地和Gupta，V.：Hybrid cc with Interval Constraints，In Proc.HSCC，LNCS 1386，Springer，1998，pp. 80比94[3] 陈旭，Abraham，E.和Sankaranarayanan，S.：Flow*：An Analyzer for Non-Linear Hybrid Systems.在proc计算机辅助验证，2013年，pp。258-263[4] F·塞尔斯，G.，格尔尼克角L.， 唐泽，A.，科顿，S.， 是的，是的，最好的，奥利维尔，里帕多河Girard，A.，天啊T马莱尔岛SpaceEx：混合系统的可扩展验证，在Proc.计算机辅助验证，2011年，pp.379-395.[5] 古 普 塔 ， 五 ， Jagadeesan 河 ， Saraswat ， V. 和 Bobrow ， D. ： Programming in Hybrid ConstraintLanguages，in Hybrid Systems II，LNCS 999，Springer，1995，pp.226-251[6] Henzinger ， T. ： The Theory of Hybrid Automata ， In Proc. LICS'96 ， IEEE Computer SocietyPress，1996，pp. 第278-292页。[7] 希基，T。J.和Wittenberg，D. K.：使用区间算术约束的混合系统的严格建模，在过程中。HSCC 2004，LNCS 2993，Springer-Verlag，2004，pp.402-416[8] Lunze ， J. ： Handbook of Hybrid Systems Control ： Theory ， Tools ， Applications ， CambridgeUniversity Press，2009.S. Matsumoto et al. /Electronic Notes in Theoretical Computer Science 317（2015）109115[9] 松本，S.和Ueda，K. Hyrose：A Symbolic Simulator of Hybrid Constraint Language HydLa，ComputerSoftware，Vol.30，No.4，2013，pp.18[10] Platzer，A.，J.D. Question KeYmaera：A Hybrid Theorem Prover for Hybrid Systems.在IJCAR 2008，LNCS 5195，Springer-Verlag，2008，第171 -178页中[11] 穆尔河，巴西-地E、基尔福特河B、Cloud. M. J.：Introduction to Interval Analysis，Society forIndustrial and Applied Mathematics，2009.[12] Ueda，K.，Matsumoto，S.，Takeguchi，A.，Hosobe，H.和Ishii，D. HydLa：A High-Level Languagefor Hybrid Systems.在proc第二次系统分析逻辑研讨会，2012年，第3 -17页[13] Zeng，Y.，罗斯角，Brauner，P.，Taha，W.，Masood，J.，Philippsen，R.， 和卡特赖特河信息物理系统的基本方面建模，第二部分。2014年第11届IEEE嵌入式软件与系统国际会议论文集