加权/定价时间自动机模型检验与博弈的电子笔记

理论计算机科学电子笔记158（2006）3-17www.elsevier.com/locate/entcs加权时间自动机：模型检测与博弈Patricia Bouyer帕特里夏·布耶1，2LSV摘要在本文中，我们提出了加权/定价时间自动机，时间自动机的成本的扩展，并解决了几个有趣的问题，该模型。保留字： 加权/定价时间自动机，模型检验，博弈。1介绍实时系统的模型检验 时间自动机[3，4]是一种成熟的实时系统模型。它们所享有的最重要的属性之一可能是可达性属性可以为该类系统决定。这引起了多个作品，无论是在理论方面和更实际的和算法方面。事实上，甚至已经开发了几种工具来检查该模型，例如HyTech [24]、Kronos [21]或Uppaal [29]，并且已经有几个成功的案例，例如，如果我们只想引用其中一个例子，BangOlufsen音频/视频协议的校正和验证[22]。加权/定价时间自动机。加权时间自动机3扩展类-[1]法国研究部ACI SI Cortos项目支持的工作2 电子邮件地址：bouyer@lsv.ens-cachan.fr[3]在本文中，我们沿用了[5]中的术语，但在[9]中，这个模型被称为定价时间自动机。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.04.0024P. Bouyer/Electronic Notes in Theoretical Computer Science 158（2006）3用自动机的位置和边缘上的成本信息来调用时间自动机标记位置的成本表示停留在该位置的每时间单位的价格，而标记边缘的成本表示进行转移的价格。 这样，自动机中的每一次运行 全局成本，它是在每个延迟和离散转换过程中的累积价格。该模型特别适用于实时系统中的资源消耗建模这在嵌入式系统中是基本的，嵌入式系统面临着几个资源约束（例如带宽，内存，功耗等）。模型检验与具有最佳化准则的博弈 成本可以用来衡量时间自动机中运行的“性能”，并且它可以用于优化模型的性能。例如，该模型可用于解决调度问题，并计算调度所有任务的最佳成本[31]。在这种情况下，解决诸如“优化到达自动机的某些预定位置的成本”或“优化自动机中无限次运行的每时间单位的平均成本”之类的问题是有趣的。更一般地，我们可以考虑模型检查问题，其中成本被视为可以在公式中使用的观察变量。例如，这是逻辑WCTL的情况，它扩展了CTL与模态上的成本约束。在这个逻辑中，我们可以表示像“每个”这样的属性请求之后是回答，并且花费小于5然后，系统可以嵌入到环境中。因此，在有对手的情况下研究类似的问题是有意义的。在过去的几年里，有大量关于最优可达性定时游戏的文献。纸的计划本文综述了加权时间自动机的一些最新结果。在第2节中，我们定义了基本的材料，比如我们考虑的模型（加权时间自动机，逻辑WCTL和加权时间游戏）。在第三节中，我们给出了时间自动机的最优费用和最优平均费用问题。在第四节中，我们给出了关于逻辑WCTL的模型检验的结果。最后，在第五节中，我们简要地给出了关于加权时间对策的一些结果。最密切相关的话题加权时间自动机中的成本变量可以被视为混合变量4，因此加权时间自动机是线性混合自动机的特殊情况[23]，其中所有变量都是时钟，但成本除外，然而，它从不用于au中的执行。4混合变量是在不同位置上具有不同斜率的变量。P. Bouyer/Electronic Notes in Theoretical Computer Science 158（2006）35≥0∪→≥0R不表示集合{v∈RX |= g }。|= g}.≥0≥0tomaton，但仅用于最优性准则，或作为公式中的约束。2定义2.1预赛我们把非负实数集R≥0看作时域我们考虑变量的有限集合X，称为时钟。X上的时钟赋值是一个映射v：X→R≥0，它为每个时钟分配一个时间值。所有时钟的集合在X上的赋值记为RX。设t∈R≥0，定义赋值v+tby（v + t）（x）= v（x）+t对所有x∈X.对于Y<$X，我们用v [Y← 0]表示赋值为0的赋值（分别为）。v（x））对于任何x∈Y（resp. x∈X\Y）。我们写0为赋值，它将0赋给每个时钟x∈ X。我们将C（X）表示为时钟约束的集合，其被定义为形式为x da c的原子约束的合取，其中x∈X，c∈N并且da∈ {<，≤，=，≥，>}。 对于g∈C（X）和v∈RX，我们记为v| = g，如果v满足g和<$g）2.2加权/定价时间自动机加权/定价时间自动机是时间自动机的扩展[4]，在位置和边缘上都有成本信息设X是一组有限的时钟，AP是一组有限的原子命题。定义2.1X和AP上的加权（或定价）时间自动机是一个元组（L，l0，T，λ，cost），其中L是位置的有限集合，l0∈L是初始位置，TL×C（X）×2X×L是转换的有限集合，λ：L→2AP是标记函数，并且cost：LTN分配给每个位置和每个位置。转型有成本。加权时间自动机的语义与时间自动机的语义相似因此，它被给出为定时转移系统（S，s0，−→），其中S=L×RX，s0=（10，0），−→包含两种类型的转换：δ（d）• 延迟变换：（l，v）−−→（l，v+d）ifd∈≥0• 如果存在一个跃迁t=（l，g，Y，lJ）∈，则圆盘的剩余距离为：（l，v）−→（lJ，vJ这样，v| = g和vJ= [Y← 0] v6P. Bouyer/Electronic Notes in Theoretical Computer Science 158（2006）3−−→L对于每一个这样的步骤，我们关联一个成本，定义如下：我不知道。（l，v）δ（d）（l，v+d）=cost（l）·d你好。（l，v）−→t （lJ，vJ）=cost（t）加权时间自动机的运行Q是转换系统中的有限或无限步骤序列（没有时间口吃）。Q的成本，记为cost（Q），是沿着行程的步骤的累积成本例2.2让我们考虑图1中给出的加权时间自动机ffi。x≤2;c1y：=01成本=10ul2x≥2;c2成本=1目标成本=5[y=0]u3x≥2;c2成本=7成本=1Fig. 1. 一种加权时间自动机ffi在ffi中可能的运行是：δ（0. 1）δ（1. 九、Q：（l0，0）−→（l0，0. 1）−→（l1，0. 1）−→（l3，0. 1）−→（l3，2）−→（W，2）Q的成本是cost（Q）= 5·0。1+1·1。9+ 7 =9。4.2.3逻辑WCTL逻辑WCTL5是一个分支时间逻辑，它用模态上的成本约束来扩展CTL第一次是在[18]。WCTL的语法由以下语法给出：WCTL3，：：= p|ϕ∨ψ|ϕ∧ψ|¬ϕ|E（Uc）|A（<$U<$c<$）其中p∈AP，c∈N且<$∈{<，≤，=，≥，>}.WCTL的公式被解释为加权时自动机ffi（即，pairs（l，v），其中l是位置，v是估值）。然后，它的语义被归纳地定义如下（原子命题和布尔组合被省略，因为它们是直接的）：5 WCTL代表“加权CTL“。l0LP. Bouyer/Electronic Notes in Theoretical Computer Science 158（2006）37|∼|||∼||−→−→对于任意的DJ≤jd，f（Q）=λ，对于任意<的dd<≤≤• ffi，（l，v）= E（Uc）i在ffi中存在从（l，v）开始到（lJ，v j）结束的游程Q，使得对于沿着Q的所有配置（l jj，v jj），ffi，（lJ，vJ）=，cost（Q）c，并且ffi，（lJJ，vJJ）=。6• ffi，q= A（Uc）i，对于ffi中从（l，v）开始到（l j，v j）结束的每个无限次运行Q，使得ffi，（lJ，vJ）=，cost（Q）c，并且对于沿着Q的所有配置（l jj，v jj），ffi，（lJJ，vJJ）=。例2.3图1的加权时间自动机ffi是这样的：|= EF≤10W（这里我们假设状态由对应于它们名字的原子命题来标记）。该公式表示，位置W可以用一条成本小于或等于10的路径到达，该公式的证明是例2.2中给出的游程Q。2.4加权定时博弈加权定时游戏是一种加权定时自动机，其中转换被解耦为可控转换（由控制器进行）和不可控转换（由环境进行）。设G=（L，l0，T，cost）7是一个加权时间对策.我们假设G有一组独特的目标位置，这些位置是每时间单位成本为0的汇点位置。从（l，v）到G的策略是从以下集合到f的部分函数：在G中从（l，v）开始运行到G加上符号λ（其用于“延迟”）的可控转变的集合中，• f（（l，v））被定义，• 如果f（Q）被定义且Q以（lJ，vJ）结尾，则：· f（Q）是G中的跃迁t，并且t从（lJ，vJ）启用，在这种情况，必须定义f（Qt）8，并且对于G中从（l j，v j）启用的每个不可控跃迁u，必须定义f（Quδ（dJ）· 或f（Q）是λ，且存在d >0，使得f（Q−−→）定义为δ（dJ）不可控跃迁ue−n−a→bledatsome（lJ，vJ+dJ），其中h0≤dJ≤d，f（Qδ（dJ））（1）必须定义。−−→−→这样的策略f以自然的方式产生一组最大对策（这意味着它们不能被扩展），记为对策G（f，（l，v））。战略F6.第N个f（l，v）δ（d）（l，v+d）是Q的一个离散，则所有的连续函数都是（l，v+d′）其中h0d′dare−“− a l → o n g Q“。7 我们抽象出标签功能，因为它在游戏框架中不起作用。8ThentationQ−→t是由变迁t扩展的游程Q的捷径。8P. Bouyer/Electronic Notes in Theoretical Computer Science 158（2006）33343是从（l，v）中获胜，用于可达性目标目标i是以下的所有（最大）发挥：策略G（f，（l，v））在某个点通过Goal。经典的可达性定时博弈可以被解决并且是EXPTIME-完全的[8，25]。对于加权定时游戏，可以向这些游戏添加最优性标准。（l，v）中的策略f的成本定义为：c〇stG（fi（l，v））=sup{c〇st（Q）|Q∈play sG（f，（l，v））}我们的目标是优化这个值并计算OptcostG（l，v）= inf {costG（f，（l，v））|f从（l，v）}并且，在可能的情况下，综合最佳获胜策略（注意，这样的策略可能不存在）。例2.4 [摘自[16]]我们考虑图1的加权时间自动机。虚线（分别为plain）arrows are for uncontrolled（resp. 可控制的）转换。取决于环境的选择（去位置l2或l3），在游戏过程中的累计成本是5t + 10（2−t）+1（至l2）或5t+（2−t）+7（至l3），其中t是在位置l0中经过延迟。因此，控制器可以确保的最优成本是inf t≤2max（5 t+10（2 − t）+1，5 t+（2 − t）+7）= 14 +1，并且最优延迟是t =。因此，控制器的最佳策略是等待状态l0直到x =4，然后进入状态l1。然后，环境选择进入l2或l3，最终当x = 2时，控制器进入状态Goal。3最优费用和最优平均费用问题用代价信息扩展时间自动机会引起各种内部优化问题：是否有可能最小化达到给定目标状态的全局代价？或者，有没有可能永远活着，同时最小化平均成本（例如每时间单位）？这样的问题是相关的，例如在调度问题中，成本可以被视为资源消耗。3.1可判定性结果最优成本问题问什么是最优的（例如，最小或最大）的成本，以达到一个给定的位置，在加权时间自动机。给定加权时间自动机ffi=（L，l0，T，λ，cost）和位置l∈L，它是P. Bouyer/Electronic Notes in Theoretical Computer Science 158（2006）39正式定义为Optcost（f1，1）=inf{cost（Q）}|从（l 0，0）到（l 0，0）运行已经解决的第一个问题是最优时间问题，当成本代表时间流逝时（位置的成本率等于1，转移的离散成本等于0）：问题是计算到达给定位置的最短时间定理3.1（[20]）时间自动机中的最优时间是可计算的。在这个第一个结果的近十年后，一般最优可达性问题已经在[5]和[9]中独立解决定理3.2（[5，9]）最优费用在加权时间自动机中是可计算的.注3.3此外，该问题是PSPACE完备的，如[6]中所述，并在[12]中得到发展这是非常令人惊讶的，因为它与简单可达性（没有任何优化标准）具有相同的复杂性最优平均成本问题问什么是最优的（例如，最小或最小）平均成本（例如每时间单位的成本），用于在加权时间自动机中保持生存。给定一个加权时间自动机ffi=（L，l0，T，λ，cost），它被正式定义为：Optcostω（ffi）=iinf{cost（Q）}|Qin finiterunfrom（l0，0）}定理3.4（[14]）最优平均费用在加权时间自动机中是可计算的。注3.5如前所述，此问题的复杂性为PSPACE-complete。3.2角点抽象这两个可判定性结果依赖于区域构造的细化[9]事实上，区域不适合计算最优（平均）成本，因为区域等价轨迹的成本可能非常不同。例如，例2.2中给出的运行Q的成本是9。4，而（区域等效）运行等待的成本为0。9个时间单位在l0，然后是2。l3中的1时间单位是13。6. 然后，想法是记录移动通过区域的极值点（具有整数坐标）（称为角点）的成本，9我们假设读者熟悉时间自动机区域的经典概念，最好参考[4]。10P. Bouyer/Electronic Notes in Theoretical Computer Science 158（2006）3从而用角点装饰区域直觉上，一个区域R被一个角点α装饰意味着α是R的一个极值点（被看作一个多面体），我们在区域R中，靠近点α（然后被看作一个赋值）。我们在例3.6中说明了这个概念。例3.6我们举例说明二维时钟空间中角点的概念经典的区域演化如图2（a）所示：随着时间的流逝，区域会跟随时间的后继者被访问（三角形区域的直接后继者是一个三角形区域，而三角形区域的直接后继者是一个三角形区域），当触发跃迁时，时钟可能会重置，然后区域会以某种方式投射到后面的区域。重置为0时间流逝(a) 区域的经典演化重置为0时间流逝成本率：3 p.u. 离散成本：7(b)角点区域的演化图二. 区域和角点抽象角点抽象如图2（b）所示。角装饰区域用黑色粗点表示我们考虑用底部的角装饰图形的左上角区域。当时间流逝时，它被变换到几乎一个时间单位之后的相同区域的顶角：因此，由于当前位置的成本率被假定为每时间单位3，因此该移动的成本为3（因为几乎一个时间单位已经流逝，因此成本增加了几乎3）。然后，因此，成本几乎为0（因为几乎没有时间流逝），这就是为什么我们将移动标记为0。对于离散移动，区域会像往常一样进行变换，角点也会投影（投影保留30 00700073P. Bouyer/Electronic Notes in Theoretical Computer Science 158（2006）311∈{≤ ≥}∈多面体端点的性质）。然后用转换的成本（在我们的示例中为7）标记转换。给定一个时间自动机ffi，我们构建了所谓的ffi的角点抽象，记为Γ（ffi），它通过包含角点信息来完善经典的区域自动机构造，如例3.6所示。 结果是一个加权有限图。这个图的最重要的性质是，给定一个有限游程Q：（l0，v0）→（l1，v1）→. →（ln，vn）在ffi中，有存在两条有限路π：（l0，R0，α0）→（l1，R1，α1）→. →（ln，Rn，αn）和πJ：（l0，R0，α0J）→（l1，R1，α1J）→. . →（ln，Rn，αnJ）inΓ（ffi）suchthatvi∈Ri，对每一个i，αi和αIJ 是Ri的角，并且cost（π）≤cost（Q）≤成本（πJ）。 相反，对于任何有限路径π：（l0，R0，α0）→（l1，R1，α1）→... →（ln，Rn，αn）在Γ（ffi）中，对任意ε> 0，都有可能构造一条实路Q：（l0，v0）→（l1，v1）→. →（ln，vn）在ffi中，使得|cost（Q）−cost（π）|<ε。因此，在ffi中的有限路径和Γ（ffi）中的有限路径之间存在很强的关系，并且计算ffi中的最优成本减少到计算离散加权图Γ（ffi）中的最优成本[5，9，12]。虽然在ffi中的无限路径和Γ（ffi）中的无限路径之间不可能有如此强的关系，但角点抽象可以用来计算有限路径中的最优平均成本[14，15]。事实上，在Γ（ffi）中的有限路径的最优平均成本是最优平均成本的循环[26]，并且它的成本总是优于ffi中任何无限路径的平均成本。3.3更进一步：最优可达性成本的符号计算最优可达性成本的可计算性依赖于区域自动机的改进的构造。在实践中，这不能用于计算最优成本，并且在[28]中提出了一种符号解决方案时间自动机的分析实际上依赖于区域，这是时间自动机状态空间的符号表示[11]，用于许多工具，如Kronos [21]或Uppaal [29]。 区域是一种特殊的多面体，具有对形式为x da c和x-yda c的时钟的约束，其中x和你是钟表，<、，=，，> 和cZ. 然后，提出了算法，在[28]中依赖于区域的扩展，称为定价区域，其记录广告成本信息（如区域的最小角落的成本，以及每个时钟的全局成本函数（表示最小成本）可以被恢复，因为它是一个递归函数。工具Uppaal Cora（Uppaal的一个分支）实现了基于定价区域的算法，并且可以可在网址http://www.cs.auc.dk/上下载。的论文[10]报告了该工具的算法和应用12P. Bouyer/Electronic Notes in Theoretical Computer Science 158（2006）32c2c12c22c1+14模型检查WCTL所有这些关于加权时间自动机的正可判定性结果都是非常令人鼓舞的。然后，考虑更一般的属性是非常自然的：逻辑WCTL被定义为CTL的自然扩展，对模态有成本约束[18]。当成本对应于时间流逝时，WCTL与经典逻辑TCTL[2]一致虽然WCTL并没有扩展那么多TCTL，但模型检查要困难得多事实上，已经证明了定理4.1（[18，13，17]）模型检验WCTL对于至少有三个时钟的加权时间自动机是不可判定的。它是单时钟加权时间自动机可判定的。不可判定性的结果首先在具有五个时钟的加权定时自动机中得到了证明[18]，并在具有三个时钟的加权定时自动机中得到了进一步的改进[13]。可判定性结果已在文献[17]中得到证明，问题的复杂性在于2EXPTIME。注4.2注意，上述结果仅适用于密集时间语义，即当时域为Q≥0或R≥0时。 事实上，在[18]中已经证明，如果我们限制到离散时间域N，的WCTL变得可判定（时间空间可以离散化）。本文简要地说明了定理4.1关于四时钟加权时间自动机的不可判定性结果，这是文[13]中关于三时钟加权时间自动机证明的简化版本。它是由两个计数器机器的停机问题的归约来完成的。设M是一台双计数器机器。计数器将使用值为1的时钟进行编码，其中c是计数器的值。 M的每个指令（测试到0、递增和递减）都将用一个小部件模拟其将根据指令的性质改变时钟的值。我们考虑增量指令。其模拟如图3所示。当进入模块时，第一个值（分别为秒）计数器存储在时钟X（resp.y），这意味着x（resp.y）为1（分别）1）其中c1（分别） c2）是第一个（分别）的值。（第二次）柜台然后遍历模块只需要一个时间单位（确保到时钟u），在其结束时，我们期望z的值为1价值之时y仍然是一样的。 为了使y的值保持不变，我们重置时钟y，当它等于1时，并且由于在模块内经过的总时间为1，因此它在开始和结束时的值相同。同样，x的值在模块的开始和结束处是相同的。 现在，z的值是通过在模块中的某个时间重置它来非确定性地猜测的P. Bouyer/Electronic Notes in Theoretical Computer Science 158（2006）313y=1，y：=0y=1，y：=0成本=1x=1，x：=0z：=0u：=0u=1Ru=1，u：=0测试（x=2z）2c1@y=@y=一一2x=1，x：=0或y=1，y：=0x=1，x：=0或y=1，y：=0u：=0z=1，z：=0u=1，u：=0成本=0成本=1y=1，y：=0或z=1，z：=0y=1，y：=0或z=1，z：=0u：=0x=1，x：=0u=1，u：=0成本=1成本=0u：=0Su=0Add（z）Add（z）成本=0加上（1−x）T成本=0模块Test（x= 2z）（我们将在后面介绍）将检查（与WCTL公式一起）z存储正确的值，即x的一半值。0Bx=11C0Bz= 图11c1B C B C图3.第三章。递增指令的模拟(a) 自动机加法（z）(b) 自动机加法（1 −x）见图4。 成本增加z 0或1− x 0的自动机我们首先解释图4中的两个小自动机。由于这些自动机的位置上的成本信息，沿着自动机Add（z）（resp.Add（1−x））增加z的初始值z0（分别）1−x0，其中x0是x的初始值）当进入自动机时，而时钟x、y和z在初始时和结束时具有相同的值自动机图5中的自动机Test（x= 2z）将成本值增加2z0+（1−x0）。为了检查最初（当进入Test（x= 2z）时），然后检查该成本等于1将是足够的。这将使用WCTL公式完成。图五、自动机测试（x= 2z）c+112c212c214P. Bouyer/Electronic Notes in Theoretical Computer Science 158（2006）3这与模拟递减非常相似，并且对0的测试是显而易见的。全局归约最终的工作原理如下：我们希望达到停止状态（标记为Halt），并且我们希望计数器的模拟沿着停止路径都是正确的这将通过以下方式强制执行WCTL公式：哪里E.你好，我是说，校正=R→E（RU≤0（S校正EF=1T））公式correct检查Test（x= 2z）模块中的累积成本等于1，这意味着我们确实有x0= 2z0。5最优时间博弈在20世纪90年代后期定理5.1（[7]）最优时间博弈是可判定的。原因在于，区域足以解决这一问题。然后，在[27]中，考虑了最优时间博弈（具有一般成本），并设计了一个2EXPTIME算法来计算非循环时间博弈中的最优成本（并该算法在某种程度上扩展了经典的最小/最大算法的离散游戏定时游戏。从2004年开始，最优时间博弈得到了进一步的研究文[1]改进了上述的2EXPTIME上界，给出了一个EXPTIME请注意，该算法为每个获胜状态计算获胜的最佳成本，并提供（可能几乎）最佳获胜策略。该算法将状态空间分割成多面体，在多面体上（大致）最优获胜策略是一致的，它是相当复杂的，并依赖于良好的几何性质的状态空间。此外，一个家庭的加权定时游戏，这是不可避免的-能够分裂成指数数量的块的胜利状态的集合。加权定时博弈的有界成本问题是，给定一个加权定时博弈G和一个阈值c，G中是否存在一个获胜策略，其成本小于或等于c。定理5.2（[19，13]）具有三个以上时钟的加权定时博弈的有界成本问题是不可计算的。P. Bouyer/Electronic Notes in Theoretical Computer Science 158（2006）315这一结果首先是在有五个时钟的加权定时博弈中得到的[19]，然后在[13]中进一步改进。不可判定性的结果与我们在第4节中介绍的WCTL的结果非常接近。在文献[19]，我们证明了带秒表和一个时钟的加权定时对策的最优成本是可判定的。实际上，在这种情况下，可以使用经典的区域最近，在一个时钟（但任意成本）的加权定时游戏中的最优成本已被证明是可计算的[17]（尽管在位置可控的限制框架中，即 离开该位置的所有转换都是可控的或不可控的）。6结论在过去的几年中，扩展了成本信息的时间自动机得到了广泛的我们已经在这里介绍了一些已经在模型检查和游戏的背景下获得的结果。让我们也提到，扩展了几个成本的时间自动机已经被考虑，例如，一个最优条件可达性问题已经被证明是可判定的[30]。致谢。 我想感谢我的合著者，感谢他们就扩展了成本信息的时间自动机这一主 题 进 行 的 富 有 成 效 的 合 作 和 讨 论 ： ThomasBrih aye ， EdBrin ksma ，V′eroniqueBruy`ere，FranckCassez，EmmanuelFy，FranEschercoisLaroussinie，KimG.拉尔森、尼古拉斯·马克、让·弗朗科斯·拉斯金和雅科·伊卢·拉斯穆森。引用[1] 巴尔河，M. Bernadsky和P.Madhusudan，加权定时游戏中的最优可达性，在：Proc. 第31届自动机、语言和编程国际学术讨论会（ICALP'04），计算机科学讲义3142（2004），页。122-133。[2] 巴尔河，C. Courcoubetis和D. Dill，Model Checking in Dense Real-Time，Information andComputation104（1993），pp. 2-34[3] 巴尔河和D. Dill，Automata for modeling real time systems，in：Proc. 第17届自动机、语言和编程国际学术讨论会（ICALP'90），计算机科学讲义443（1990），pp。322-335[4] 巴 尔 河 和 D. Dill ， A theory of timed automata ， Theoretical Computer Science126（1994），pp. 183-235[5] 巴 尔 河 ， S. La Torre 和 G. J. Pappas ， 加 权 时 间 自 动 机 中 的 最 优 路 径 ， 在 ： Proc.4thInternational Workshop on Hybrid Systems：Computation and Control（HSCC49比62[6] 巴尔河和P. Madhusudan，Decision problems for timed automata：A survey，in：Proc.4thInternational School on Formal Methods for the Design of Computer，Communication andSoftware Systems ： Real Time （ SFM-04 ： RT ） ， Lecture Notes in Computer Science3185（2004），pp. 122-133。16P. Bouyer/Electronic Notes in Theoretical Computer Science 158（2006）3[7] Asarin，E.和O. Maler，尽快：时间自动机的时间最优控制，在：Proc。第二届国际混合系统研讨会：计算与控制（HSCC'99），计算机科学讲义1569（1999），页。19比30[8] Asarin，E.， O. Maler，A. Pnueli和J. Sifakis，时间自动机的控制器合成，在：国际会计师联合会系统结构和控制专题讨论会论文集（1998年），第100页。469-474.[9] Behrmann，G.， A. Fehnker，Th. Hune，K. G. Larsen，P. Pettersson，J. Romijn和F. Vaandrager，定价时间自动机的最小成本可达性，在：Proc. 4th International Workshop onHybrid Systems：Computation and Control（HSCC147-161[10] Behrmann ， G. ， K. G. 拉 森 和 J. I. Rasmussen ， Priced Timed Automata ： DecidabilityResults，Algorithms，and Applications，Proc. 第三届组件和对象的形式化方法国际研讨会（FMCO'04），计算机科学讲义3657（2004），pp。162-186.[11] Bouyer，P.，可更新时间自动机的前向分析，系统设计中的形式化方法24（2004），pp. 281-320。[12] Bouyer，P. ，Th. 好的，小维。 布鲁和J。-F. Raskin，Onteo timalreachabiltyproblem（2006），已提交。[13] Bouyer，P.，日Brihaye和N.Markey，Improved undecidability results on weightedtimed automata，Information Processing Letters（2006）.[14] Bouyer，P.，E. Brinksma和K. G. Larsen，Staying alive as cheaply as possible，in：Proc.7thInternational Workshop on Hybrid Systems：Computation and Control（HSCC203-218[15] Bouyer，P.，E. Brinksma和K.G. Larsen，Optimal Infinite Scheduling for Multi-pricedTimed Automata，Formal Methods in Systen Design（2005）。[16] Bouyer，P.，F. Cassez，E. Fleury和K. G. Larsen，定价时间博弈自动机中的最优策略，Proc.第24届软件技术和理论计算机科学基础会议（FST& TCS'04），计算机科学讲义3328（2004），pp。148比160[17] Bouyer，P.，F. Laroussinie，K. G. Larsen，N.马基和J. I. Rasmussen，One Clock PricedTimed Automata：Model Checking and Optimal Strategies（2006）.[18] 好的，T。、V. 你和J都在。-F. Raskin，Model-checkingfororeghttimeddautomata，in：Proc. Joint Conference on Formal Modeling and Analysis of Timed Systems and FormalTechniques in Real-Time and Fault Tolerant System（FORMATS+FTRTFT'04），LectureNotes in Computer Science 3253（2004），pp. 277-292.[19] 好的，T。、V.你和J都在。-F.Rask in，On onoP roc.3RD时间系统的形式化建模和分析国际会议（FORMATS'05），计算机科学讲义3821（2005），页。49比64[20] 库尔库贝蒂斯角和M. Yannakakis，实时系统中的最小和最大延迟问题，系统设计中的形式化方法1（1992），pp.385-415.[21] 道斯角，A. Olivero，S. Tripakis和S. Yovine，Kronos工具，在：Proc. Hybrid SystemsIII：Verification and Control（1995），Lecture Notes in Computer Science1066（1996）。208-219[22] Havelund ， K. ， A. Skou ， K. G. Larsen 和 K. Lund ， Formal modeling and analysis of anaudio/video protocol：An industrial case study using Uppaal，in：Proc. 18th IEEE Real-Time Systems Symposium（RTSS2-13.[23] Henzinger，Th.一、 混合自动机的理论，在：Proc。第11届计算机科学逻辑年度研讨会（LICS '96）（1996），pp。278-292.[24] Henzinger，Th.一、P. - H. Ho和H.Wong-Toi，HyTech：混合系统的模型检查器，Journalon Software Tools for Technology Transfer1（1997），pp.110-122P. Bouyer/Electronic Notes in Theoretical Computer Science 158（2006）317[25] Henzinger，Th. A.和P.W. Kopke，离散时间控制矩形混合自动机，理论计算机科学221（1999），pp。369-392.[26] 卡普河M.，A characterization of the minimum mean-cycle in a digraph，DiscreteMathematics23（1978）. 309-311[27] La Torre，S.，S. Mukhopadhyay和A. Murano，非循环加权时间自动机的最优可达性和控制，在：第二届IFIP国际理论计算机科学会议（TCS 2002），IFIP会议论文集223（2002），pp.485-497.[28] Larsen ， K. G. ， G. Behrmann ， E.Brinksma ， A. Fehnker ， Th.Hune ， P. Pettersson 和 J.Romijn，尽可能便宜：定价时间自动机的有效成本最优可达性，在：Proc.13th计算机辅助验证国际会议（CAV493-505[29] Larsen，K. G.，Pettersson和W. Yi，Uppaal in a nutshell，Journal of Software Tools forTechnology Transfer1（1997），pp. 134-152。[30] Larsen ， K. G. 和 J. I. Rasmussen ， 多 价 格 时 间 自 动 机 的 最 优 条 件 调 度 ， 在 ： Proc.8thInternational Conference on Foundations of Software Science andComputation Structures（FoSSaCS234-249.[31] Rasmussen，J.，K. G. Larsen和K. Subramani，使用定价时间自动机的资源优化调度，在：Proc. 第10届国际会议的工具和算法的建设和分析系统（TACAS'04），在计算机科学讲义2988（2004年），页。220-235