基于块的相位型分布城市中心公交车运行模型及性能分析

可在www.sciencedirect.com在线获取理论计算机科学电子笔记310（2015）157-177www.elsevier.com/locate/entcs基于块的相位型分布城市中心公交车运行建模DaniüelReijsbergen，StephenGilmoreand JaneHillston1，2爱丁堡大学计算机科学基础实验室苏格兰爱丁堡摘要我们提出了一种方法来构建一个随机性能模型的公共交通网络使用真实世界的数据。我们的主要数据源包括自动车辆定位（AVL）测量的巴士在爱丁堡地区。 虽然数据的频率相对较低，但我们可以利用它对一个模型进行参数化，在这个模型中，一辆公共汽车在城市中预定义的区域之间移动。 我们把概率-使用HyperStar工具将斑块中逗留时间的分布转换为相位型分布。然后，我们将HyperStar的输出转换为表示为PRISM模型检查器的反应模块语言。最后，我们演示了如何使用PRISM中实现的数值技术来回答有关公交网络性能的有意义的问题，该案例研究涉及将有轨电车添加到爱丁堡繁忙路段的情况。 市中心。关键词：公共交通、相态拟合、模型检验1介绍一个运作良好的公共交通网络可以帮助一个现代化的城市最大限度地减少道路使用、空气污染、燃料消耗和碳排放。然而，在紧缩和削减预算的时期，市政府和公交公司都面临压力以降低运营成本，这可能会损害客户满意度。为了在成本和服务质量之间实现合理的平衡，上级政府责成外部监管机构评估服务质量是否高于给定的最低限度。制定合理的服务需求的任务是不平凡的，并且由于以下事实而变得复杂：公共交通网络受到随机行为的影响。因此，需要强大的随机模型，以便能够1）评估当前服务是否1这项工作得到了欧盟项目QUANTICOL，600708的支持。2通讯作者：dreijsbe@inf.ed.ac.ukhttp://dx.doi.org/10.1016/j.entcs.2014.12.0171571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/3.0/）。158D. Reijsbergen等人理论计算机科学电子笔记310（2015）157要求可以合理地得到满足，2）以衡量拟议的变化对网络的影响在本文中，我们提出了一个数据驱动的方法来构建一个正式的随机模型，可用于这两个目的。 数据提供给我们由洛锡安巴士公司，总部设在苏格兰和经营广泛的巴士网络在爱丁堡举行。由于过去与监管机构在城市有轨电车工程对时间表遵守的影响方面存在分歧[7]，他们对问题1）特别感兴趣。此外，在研究涉及政策构想或能力重新分配的“假设”情景时，经常出现第2类问题。一个政策建议是，交通灯相位的时间应该调整，以有利于晚运行的公共汽车（通过延长绿色相位以利于他们），并阻止早运行的公共汽车（通过延长红色相位以减缓他们）[16]。在八月爱丁堡节期间，巴士路线会改道往交通较为畅顺的街道，这是重新分配巴士载客量的一个例子。本文的重点是一个案例研究，涉及电车引入爱丁堡这些数据包括全天公交车位置的GPS测量值，大约每30-40秒向中央服务器报告一次。为了应对相对较低的频率的测量，我们将所研究的路由的一部分划分为一系列的补丁。然后，我们提出了一个随机模型，models- els的连续时间运动的补丁之间的巴士。每个补丁所花费的时间的概率分布被建模为超Erlang分布。hyper-Erlang分布允许使用工具HyperStar [13]轻松参数化，并在参数化时对数据进行良好拟合。 此外，可以使用单个补丁逗留时间的超Erlang分布作为构建块来构建连续时间马尔可夫链（CTMC），CTMC又可以使用PRISM [9]模型检查器的基于反应模块的语言来简洁地表达。这些模型可以使用PRISM强大的数值求解引擎进行分析本文的结构如下。在第2节中，我们将对数据进行更详细的描述，讨论与案例研究相关的城市部分，并讨论将这一部分划分为斑块的问题。在第3节中，我们解释了如何使用HyperStar工具将补丁中逗留时间的经验分布拟合为超Erlang分布。在第4节中，我们讨论了如何使用HyperStar的结果来构建公共汽车相关部分的模型，路线，并讨论性能要求的正式规范。在第5节中，我们执行了所提出的方法并给出了结果。第六节介绍相关工作。第七节是论文的结论。D. Reijsbergen等人理论计算机科学电子笔记310（2015）157159(a)（b）（c）（d）Fig. 1.四个不同总线的测量之间的时间分布。有些分布是重尾的，例如在（d）中，观察到47秒的延迟：注意不连续轴。2数据可用性和定义补丁由于我们的方法是数据驱动的，因此对可用数据的清晰理解至关重要。可用数据的一个重要特征是测量频率相对较低，这最适合于空间表示是粗粒度的。因此，我们将与我们的案例研究相关的城市部分划分为斑块。 在本节中，我们首先讨论 的可用数据，然后再转移到补丁结构的描述2.1自动车辆定位（AVL）数据Lothian Buses提供给我们的数据包括使用定期GPS定位测量获得的AVL数据。每个数据条目包括总线标识符、位置测量和测量时间戳。我们的数据集包含有关745辆公共汽车的完整数据集的信息，这些信息是在2014年1月28日11：31：14和2014年1月30日12：38：31之间收集的。数据通过集中的pull request收集。因此，测量通常在数据集内对齐，即，如果对于一个总线的某个时间点存在测量，则对于同一数据集中的所有其它总线的测量应当在同一时间点存在。此规则的主要例外是，当总线在两次测量之间没有移动时，第二次测量不会被记录（对于较大的序列也是如此）。测量之间的时间通常在30到40秒之间。分布图见图1。该数据是在大不列颠地形测量（OSGB）东和北，而不是纬度/经度坐标。一旦转换为纬度/经度坐标，测量值具有约为0的水平（纵向）坐标集。00143度。GPS测量是相当准确的，一旦取消了o-set;我们可以确定巴士的方向，它正在行驶的道路一侧，如图2所示。数据并不总是完美的：在极端情况下，这意味着位置数据明显无效（例如，公共汽车出现在一片农田或中间”（《礼记》）。在不太明显的情况下，公共汽车似乎冻结了很长一段时间，然后突然出现在遥远的地方。公共汽车似乎冻结160D. Reijsbergen等人理论计算机科学电子笔记310（2015）157图二. 数据可以足够准确，通过目视检查侧面来确认总线的方向它行驶的道路在城市中心的位置，可能会对行程时间分析产生重大影响。因此，建议使用可视化工具检查数据中的明显错误，例如[18]。不言而喻的错误观测似乎不成比例地经常发生在晚上;因此，我们将我们的数据集限制为仅包括上午7：30至下午7：30之间记录的测量值。虽然数据条目包括唯一标识公交车的标识符，但将公交车标识符与公交车路线相匹配并不简单，因为公交车到路线的分配可能在几天之间（甚至有时是几小时之间）变化。目前，我们不确定公交车所属的路线，因此每个补丁的逗留时间测量（在第2.2节中更详细地讨论）是针对所有经过的公交车计算的。我们希望将来能够自动匹配公交车和路线，但这取决于以足够详细的粒度将公交车映射到路线的AVL数据的一个积极方面是它可以进行插值。这有助于改善低频数据的问题，允许我们在报告的数据之间插入额外的点。使用线性插值，我们在相邻点之间插入一个中点，以从（真正的）36秒分辨率数据生成（近似的）18秒分辨率数据。重复这个过程，我们从（近似）18秒分辨率的数据生成（近似）9秒分辨率的数据。这种插值是合理的，因为公交车的纬度和经度位置在连续空间中递增地变化因此，我们在必要时以这种方式补充我们的这种插值的示例如图3所示。一旦公交车被映射到路线，我们将能够实现一个更好的插值，其中角落永远不会缩短。未来研究的另一种可能性是实施[17]中更精细的插值技术，其中插值基于历史公交位置测量的第二个数据集。2.2补丁程序选择我们的公交车运动的正式模型背后的主要思想是抽象的公交车被划分为补丁的然后，我们的模型描述了补丁之间的总线的运动。具体来说，我们感兴趣的是D. Reijsbergen等人理论计算机科学电子笔记310（2015）157161图三.同样的插补AVL数据集在图上被语义解释为纬度和经度时间序列（左），并在地图上可视化呈现（右，细节）。 在可视化中，真实的数据点用圆圈表示，内插点用菱形表示。 时间的流逝由光谱表示，因此数据在红色、橙色、黄色、绿色、蓝色、靛蓝和紫色之间循环，然后再次返回红色。这表明巴士首先从西向东沿着王子街行驶，然后返回，从东向西行驶。颜色代表抽象意义上的时间流逝，并通过显示公共汽车正在沿着旅程的出发部分的路线返回来每一个补丁都有一辆公交车。图4显示了将公交路线划分为小块的示例。目前，修补程序是手动选择的。在本文中，我们重点关注城市的一个特定部分，即爱丁堡市中心的王子街。除了是一条繁忙的购物街外，它还是连接城市西部和东部的主要动脉，几乎所有穿越爱丁堡市中心的公交车都沿着王子街的至少一部分行驶。集中在一条街道上的好处是，这些斑块可以排序，在这种情况下，从西南部开始。王子街的补丁选择是不平凡的;例如，可以在规则或不规则网格之间进行选择。图4的斑块划分是不规则的，并且基于沿线的公交车站和交通灯的位置。具体而言，斑块表示（i）直接围绕接合点的区域，或（ii）类型（i）斑块之间的大区域。公共汽车站总是包含在第二类斑块中。这个选择是因为我们还不能自动将公交车映射到路线，如第2节所讨论的。即使不知道公交车所服务的确切路线，我们也知道当它进入类型（ii）的补丁时，它总是必须完成整个补丁。这使我们能够把逗留时间的分布拟合成一个尽可能简单的分布。此外，在我们在这里考虑的城市地区，公共汽车在一个单一的补丁内最多停一个公共汽车站。并不是所有的公交车都停在每一个有公交车站的地方，但大多数都停。这条经验法则也有例外，例如从海运大厦到荷里路德的36号巴士7号巴士数据，2014年1月28日55.97-3.165数据插值-3.1755.965-3.175-3.1855.96-3.18555.955-3.19-3.19555.95-3.2-3.20555.945-3.21-3.21555.94-3.2255.935-3.22517：50 17：55 18：00 18：05 18：10 18：15 18：20 18：25 18：30 18：35 18：4018：45 18：50 18：55 19：00一天纬度经度162D. Reijsbergen等人理论计算机科学电子笔记310（2015）157⎧⎨−≥i=1i=13逗留时间分布在本节中，我们将描述如何将超Erlang分布拟合到经验的逗留时间分布。我们首先正式定义了超Erlang分布，然后讨论了工具HyperStar和参数拟合结果。3.1超厄兰分布虽然我们假设读者熟悉CTMC的概念，但我们从最基本的概念开始，即指数分布。一个随机变量X被称为是指数分布的速率为λ，λ>0，如果1e−λxifx0，P（X x）=如果x为<0，则为0。如果X1，...，X，k都是两两独立的，且以速率λ服从指数分布当k∈N时，S=n ×kXi是Erlang分布，其速率为λ，形状为k. THES的概率密度函数（pdf）fS由下式给出：λkxk−1e−λxfS（x）=.（一）（k−1）！构造一个超Erlang分布随机变量：给定某个m ∈ N，设α1，…， α m是{1，.， m}，也就是说， α i∈ [0，1]和αm α i=1。 此外，令Si，i∈ {1，.，m}，beErlang分布，速率为λi，形状为ki-这些随机变量称为超Erlang分布的分支。 然后我们说一个随机变量Y是超Erlang分布，速率为λ1，...，λ m，形状k1，...，k m和分支123456789101112131415见图4。二维和一维空间中的公共汽车;路线的一部分，包括补丁。请注意，在1D中，我们假设两个方向在最左边的红色斑块中穿过相同的空间量，尽管它从2D图中可以明显看出，情况并非如此。D. Reijsbergen等人理论计算机科学电子笔记310（2015）157163Mαi、（二）-1）！B1λ1B2λ1B3λ1α1一α2α3C1λ2C2λ2C3λ2C4λ2Eλ3D1λ3D2λ3D3λ3D4λ3D5概率 α1，...α mifΣi=1λkixki−1e−λixi=1（k）我其中fY表示Y的pdf。Y的实现很容易绘制如下：从{1，...，m}的概率为α i的情况下，从具有速率λ i的指数分布中得出k i个实现并求和。超厄兰分布是一种相位型分布：它可以用CTMC吸收前的时间来描述。图5中给出了这样一个CTMC的例子，它表示一个具有三个分支的超Erlang。图五.示例三分支（3/4/5）阶段超Erlang分布表示为CTMC。 虚线箭头用于指示瞬时概率转换。实线箭头用于指示具有指数分布持续时间的转换。使用超Erlang发行版的一个重要动机是， Erlang和超Erlang分布表现出在运输系统分析中通常观察到在[17]中使用的分布和Tra Bac EngineeringHandbook [10]推荐的分布是一个三参数伽玛分布，它以以下方式与Erlang分布相关。标准（双参数）伽马分布是Erlang分布的推广，在这个意义上，它的pdf等价于（1），但用伽马函数代替阶乘，因此允许参数k是任何正实数而不仅仅是正整数。上述三参数伽马分布是标准伽马分布加上常数。这个常数补偿了这样一个事实，即对于大的k值（这通常在将伽马分布拟合到大斑块中的逗留时出现正态分布是对称的，而斑块逗留时间分布倾向于向右偏斜（即，大的延迟）。由于以下原因，我们在本文中不使用三参数伽玛分布。首先，从离散到连续k值的推广和确定性常数的增加都禁止模型以CTMC的形式表示，从而禁止使用PRISM中实现的强大的数值技术。此外，由于所考虑的斑块相对较小，在我们的设置中附加常数的影响不是很大。第三，使用hyper-Erlang发行版允许我们包含一个通过混合具有不同峰值的两个Erlang分布来向右偏斜。MP（Y y）=αiP（Si y）和fY（y）=164D. Reijsbergen等人理论计算机科学电子笔记310（2015）1573.2超级巨星软件工具HyperStar [13]将相位型分布的有效参数拟合算法与用户友好界面相结合。在选择数据集之后，要求用户在数据中直观地识别峰值，然后大致对应于各个Erlang分支的均值。Hy- perStar算法考虑用户识别的峰值数量，并将返回具有该分支数量的相位型分布。给定m个峰，有3 ×m个参数要优化，即λ i，ki和α i，对于每个i∈ {1，...，m}。我们优化的标准由对数似然给出：逗留时间测量t的对数似然等于logfY（t），其中fY如（2）的第二个等式中所定义。整个样本的对数似然是所有个体对数似然的总和。对数似然越高越好。HyperStar允许用户从几种相位类型拟合算法中选择一种;对于第5节中的分析，我们使用标准程序，即[12]中描述的基于聚类的拟合。3.3HyperStar结果在本节中，我们将讨论使用HyperStar进行参数拟合的结果。本节的结构如下：我们首先介绍三种呈现数据的方法，即表1和表2以及图6。然后，我们继续解释结果，特别是那些与第5节案例研究相关的结果。在图6中，拟合到每个补丁的超Erlang分布的pdf和累积分布函数（cdf）与它们的经验等价物一起以图形方式描绘。图6可用于直观地测量超Erlang分布的拟合优度，并研究经验分布的性质，如尾部行为和多峰的存在在表1中，给出了hyper-Erlang参数的精确值以及其他详细信息。我们只考虑具有两个分支的超Erlang分布，如我们稍后解释的除了标准的hyper-Erlang参数外，还提供了其他三个指标，这些指标提供了有关预期逗留时间的重要信息前两个是μ1和μ2，分别等于k1/λ1和k2/λ2;这些值对应于两个单独的Erlang分支的平均值第三个度量是μ=α1μ1+α2μ2，它对应于整个超厄兰分布的平均值分支由分支装置排序;即，对于每个补丁α1，k1和λ1对应于具有最短完成时间最后，我们指出每个补丁是否包含一个巴士站，因为这对预期的逗留时间有重大影响在表2中，我们比较了Erlang分布与双分支超Erlang分布的拟合优度。我们以cdf差异（与实证cdf与拟合cdf之间的差异有关的计量）来确认拟合优度。低的cdf-di值对应于良好的拟合。在HyperStar中实施的优化程序旨在最大限度地提高D. Reijsbergen等人理论计算机科学电子笔记310（2015）157165补丁1 -停止，没有光补丁2 -没有停止，光补丁3 -没有停止，光补丁4-停止，没有光补丁5-没有停止，光补丁6-停止，没有光补丁7-没有停止，轻补丁8-没有停止，没有轻补丁9-没有停止，轻补丁10 -停止，没有光补丁11 -没有停止，光补丁12 -没有停止，光补丁13 -停止，没有光补丁14 -没有停止，光补丁15 -没有停止，没有光见图6。经验逗留时间分布和相应的超厄兰适合15个补丁。在本文的数字版本中，轴上的标签是可读的;x轴是秒。请注意，x轴和y轴的比例可能在小数点之间变化166D. Reijsbergen等人理论计算机科学电子笔记310（2015）157贴片（α1，α2）（k1，k2）（λ1，λ2）（μ1，μ2）μ停下来？1（0. 4938，0。（5062）（8，3）（0. 3041，0。（0899）(26. 31，33。（第三十八条）29.89是的2（0. 4970，0。5030）（3，5）（0. 1374，0。（1083）(21. 83，46。十七、34.07没有3（0. 5298，0。（4702）（7，5）（0. 4536，0。（1178）(15. 43，42。第四十四章）28.13没有4（0. 5043，0。（小行星4957）（6，3）（0. 1949年，0。（0618）(30. 78，48。（第五十七条）39.60是的5（0. 5320，0。4680）(16（2）（1. 2626，0。（1144）(12. 67，17。（第四十八条）14.92没有6（0. 5065，0。（4935）（四、六）（0. 1309，0。（0983）(30. 56，61。02）45.59是的7（0. 4939，0。5061）（3，2）（0. 1857年，0。（0572）(16. 十五，三十四。（98）25.68没有8（0. 5568，0。（4432）(17（3）（1. 2685，0。（1108）(13. 四十，二十七。07）19.46没有9（0. 5239，0。（4761）(16（3）（1. 7485，0。（1660年）（9. 15，18。07）13.40没有10（0. 5146，0。4854）（3，3）（0. 1025，0。（0488）(29. 28，61。（第四十三条）44.89是的11（0. 5098，0。（4902）（4，3）（0. 2206，0。（0736）(18. 13，40。（第七十七条）29.23没有12（0. 5378，0。4622）(17（3）（1. 0080，0。（1230）(16. 87，24。（第三十九条）20.34没有13（0. 4800，0。5200）（7，2）（0. 6398，0。（0519）(10. 94，38。（第50段）25.27是的，14（0. 4883，0。（5117）（二、三）（0. 1229，0。（0664）(16. 27，45。十八）31.07没有15（0. 4958，0。（5042）(10（1）（0. 8518，0。（0616）(11. 74，16。第二十三章）14.00没有表1每个补丁的HyperStar结果答：在Patch 13有一个巴士站，但只有两条路线（22和25）使用D. Reijsbergen等人理论计算机科学电子笔记310（2015）157167贴片number1的 分支2巴士站结10.96470.6900是的没有21.56430.9805没有是的33.34441.2408没有是的42.33281.4514是的没有51.92181.1134没有是的60.97100.9320是的没有72.05321.7146没有是的83.51911.3365没有没有92.19520.7391没有是的101.31431.2243是的没有111.33410.8073没有是的122.89600.9251没有是的134.65731.2144是的，没有142.34401.1864没有是的152.02930.5990没有是的表2在这个表中，我们比较了给定补丁的cdf-di统计，以及Erlang分支数的几种选择。较低的cdf-di值意味着更好的拟合。我们不考虑具有两个以上分支的超Erlang分布，因为我们已经观察到这通常会导致过度拟合（例如，两个或更多接近模式的Erlang分支，只是稍微改善了大量样本的拟合答：在Patch 13有一个巴士站，但只有两条路线（22和25）使用168D. Reijsbergen等人理论计算机科学电子笔记310（2015）157对数似然，因此CDF-DI的低值仅仅是副产品。在表2中，我们没有考虑具有两个以上分支的超Erlang分布。我们这样做有两个原因。首先，HyperStar使用的优化过程使用随机化来远离局部最优值，并且对于更高数量的Erlang分支，结果在运行之间开始发生很大变化。第二，我们已经观察到，使用两个以上的分支通常会导致过度拟合，主要表现为Erlang分布的混合，在一个大的峰值周围有两个非常相似的均值。关于结果值的解释，我们首先观察到，对于每个补丁，Erlang分支均值μ1和μ2明显不同，并且分支概率α1和α2都相对接近于（1，1）。为2 2补丁没有公交站，两个分支机构的解释是，分支机构具有最低平均值（即，μ1）表示如果允许公共汽车在很大程度上不受交通灯阻碍的情况下穿过贴片，则在贴片对于有公交站点的斑块，即使取均值最低的Erlang分支，在公交站点上花费的时间也是明显的。这方面的一个例证是，尽管这些补丁的大小大致相同，但补丁6的μ1有公交车站的补丁往往是更好地近似使用一个Erlang分布比那些没有。这可以通过Erlang分布的cdf-di结果（即，表2中补丁1、6和10的超Erlang分布（带有一个分支）给出了相对较好的拟合;补丁4是个例外，它有一个非常长的尾部。交通灯的影响在某些补丁中非常明显。例如，在补丁3中花费的时间的分布具有多于一个明显的峰值，如图6所示。此外，补丁8和补丁13的逗留时间分布具有非常长的尾部，无法用Erlang分布精确建模这可以从表2中看出：Erlang分布对补丁3、8和13的拟合相对较差。由透射光行为引起的一个非常显著的差异是在斑块7和9之间，其具有相似的尺寸和相似的透射图案，但是如在表1中可以看到的，在μ方面有很大的差异。这两个路段的主要区别在于，路段9不允许车辆转弯，因此交通灯只需要三个相位：一个是东西向交通灯，一个是南北向交通灯，一个是行人灯。Patch 7中的交通灯需要更多的相位，导致预期逗留时间显著增加。我们将使用这个关于透射光相位数差异的观察结果来分析4.1节中的PRISM模型。地形强度沿路线变化一个非常明显的例子是王子街的交通限制部分（即，道路上没有汽车），即大致对应于补丁4、5和6的区域。 我们观察到，补丁5有一个更低的预期逗留时间比补丁3和13比预期的，如果只考虑大小的差异。沙漠化的影响似乎没有延伸到第7块，因为与第3块相比没有太大的差异，第3块位于沙漠化区域的另一侧关于当前时间表的遵守情况，请注意，如果我们将表1中每个补丁的μ值相加，我们发现穿越整个时间表D. Reijsbergen等人理论计算机科学电子笔记310（2015）157169一组15个补丁约等于415秒（近7分钟）。目前还不清楚这些站点的时间表，因为在线时间表只给出了沿线几个主要站点的到达时间然而，我们可以使用洛锡安巴士网站上的行程计划来获得整个路线的预计持续时间。要做到这一点，我们专注于路线1和34，这两个停止在名为'喀里多尼亚酒店'（巴士站代码36232692）在补丁1和然后，程序如下：我们使用旅程计划器获得未来大约30分钟内1或34路公交车到达Caledonian Hotel的时间，然后将其与LeithStreet的最近时间进行比较。差异则为完成时间表所指定路线的估计时间。虽然测量值因时间而异，但我们通常观察到，预测值对应于两站之间大约6分钟4建模在获得超厄兰参数，我们用它们来构建一个模型，可以回答问题的案例研究，涉及电车在爱丁堡。我们首先使用PRISM以正式和简洁的方式描述模型。然后，我们讨论了用于评估有轨电车的影响的性能指标4.1PRISM模型PRISM基于反应模块的形式主义，使用自己的语言表达模型[1]。在下文中，我们对PRISM语言进行了简要描述，该语言不是完全通用的，但涵盖了本文的范围。[11]见《无量寿经》顾名思义，反应模块形式主义背后的思想是将复杂的系统模型分解为交互模块的组合。一个典型的模块包括一组局部变量，它们共同代表模块的状态;然后可以使用所有单个模块的状态导出模型的全局状态。模型的转换结构使用命令来描述，其中每个命令都链接到一个特定的模块。的命令······见图7。 PRISM模型部分的CTMC表示。 红色状态对应于总线处于补丁2中，蓝色状态对应于总线处于补丁3中，黄色状态对应于总线处于补丁3中。巴士在Patch 4。当总线在补丁之间移动时，在下一个补丁的两个Erlang分支λ2aα3aλ2aλ3aλ3bλ2bα3bλ2bλ3aα4aλ3aλ4aλ3bλ4bα4bλ3b170D. Reijsbergen等人理论计算机科学电子笔记310（2015）157模块Patch3BusesInP3a：[0.. 1]initbuses3a; BusesInP3b：[0.. 1]init buses3b; Phases3a：[1..k3a]init k3a; Phases3b：[1..int[init];//进入Patch 3的总线[p2aTo3a]（BusesInP3a=0）→1：（BusesInP3a=BusesInP3a+1）;[p2aTo3b]（BusesInP3b=0）→1：（BusesInP3b=BusesInP3b+1）;[p2bTo3a]（BusesInP3a=0）→1：（BusesInP3a=BusesInP3a+1）;[p2bTo3b]（BusesInP3b=0）→1：（BusesInP3b=BusesInP3b+1）;//internal transitions[phCom3a]（Phases3a>1BusesInP3a=1）→Phada3a：（Phases3a=Phases3a−1）;[phCom3b]（Phases3b>1BusesInP3b=1）→Phada3b：（Phases3b=Phases3b−1）;//离开Patch 3的[p3aTo4a]（Phases3a=1BusesInP3a=1）→P3a3a→alpha4a：[p3aTo4b]（Phases3a=1BusesInP3a=1）→P3a3a→alpha4b：（BusesInP3a=BusesInP3a−1）（Phases3a=k3a）;[p3bTo4a]（Phases3b=1BusesInP3b=1）→Phasda3b→alpha4a：（BusesInP3a=BusesInP3a−1）（Phases3a=k3a）;[p3bTo4b]（Phases3b=1BusesInP3b=1）→转换a3b转换alpha4b：（BusesInP3b<$=BusesInP3b−1）（Phases3b<$=k3b）;（BusesInP3b=BusesInP3b−1）（Phases3b=k3b）;端模图八、PRISM语言描述了一个典型的补丁（Patch 3）中的模型。我们使用的是一个动作标签、一个保护、一个速率和一个更新。守卫是强加在模块的局部变量上的条件;对于要启用的具有给定动作标签的转换，必须满足每个单独的命令都有一个相关联的速率：转换的总速率是各个速率的乘积。 在每个步骤中在系统模型的执行中，基于所启用的转换的速率来选择转换。具体地说，当选择转换时，模块中的局部变量与对应于转换的命令以使用其更新指定的方式进行更改。在我们的模型中，我们为每个单独的补丁使用一个模块图8中描述了一个典型补丁（在本例中为Patch3）的模块。局部变量对应于总线是否在补丁内以及有多少指数阶段必须在它离开之前完成。 当总线进入补丁时，选择两个Erlang分支之一。分支的选择被编码在变量中：因为每个补丁有两个Erlang分支，每个模块有两个总线变量（图8中的BusesInP3a和BusesInP3b）。由于我们对单个总线的行为感兴趣，因此这两个变量的最大值都是1。此外，我们分别对两个分支中的每一个中要完成的相位进行编码，这导致相位计数器的两个变量（相位3a和3b）。图8中的阶段3b）。每个模块都有两个内部转换，即两个Erlang分支（由带操作标签的命令D. Reijsbergen等人理论计算机科学电子笔记310（2015）157171phCom3a和phCom3b）。这些模块在总线从一个补丁到另一个补丁的转换过程中进行同步。对于每个补丁模块，存在与最多两个其它模块的同步：对应于它之前的补丁的模块（即，由于总线移动到一个补丁可能会导致两个不同Erlang分支的总线位置变量被重置，并且由于必须在下一个补丁的两个分支之间进行概率选择，因此相邻模块共有四个动作标签。对于Patch3（如图8所示），它有两个相邻的补丁，有八个命令。每个命令都有一个操作标签，该标签与对应于相邻补丁的模块中的其他命令共享：例如，Patch2中也有一个操作标签为p2aTo3a的命令。请注意，在Patch 3中，带有操作标签p2 aTo 3a的命令是被动的;即，它的速率为1（我们已经明确表示了- PRISM允许我们在此设置中省略速率指定）。 Patch2中给出了这种转换的实际速率（回想一下，总金额是个别金额的乘积）。一般来说，对于每个模块，与进入补丁的总线相对应的动作是被动的。有两个补丁的行为与补丁3略有不同。首先，最终模块（Patch15）有一个有两个动作对应于进入“sink”的总线：一个是离开Patch 15的分支a的总线（带有动作标签p15aToSink），另一个第二，贴片15的分支a没有相种类，因为该分支仅具有一个相，如表1所示。相反，当BusesInP15a变得大于零时，可以直接采取具有标签p15aToSink的动作。此外，Patch 1中的逗留时间分布由Erlang分布给出，而不是2分支超Erlang分布。原因是技术性的：为了能够使用PRISM分析模型，需要一个唯一的初始状态，而如果Patch 0中的逗留时间分布具有2分支超Erlang分布，我们希望从概率为y α 0 c的分支c∈{a，b}开始。如果我们对此补丁使用Erlang近似，则可以解决此问题。另一种可能的补救措施是创建一个虚拟补丁，从中可以以非常高的速率跳到补丁1，但这会为数值CTMC分析带来稳定性问题，因此我们不希望这样做。4.2业绩计量我们在本文中考虑的主要性能指标是准时性能[5]。具体来说，我们感兴趣的是服务是否准时，苏格兰政府将其定义为在所谓的提前一分钟和迟到五分钟之间的容忍窗口内到达请注意，政府监管机构仅衡量服务是否在预先指定的时间点准时然而，由于路线上的准时性取决于组成路线的部分的准时性，这仍然是一个有趣的度量，即使在如此短的路线上迟到超过五分钟的概率相当低。我们认为从“喀里多尼亚酒店”站出发的公共汽车的准时性172D. Reijsbergen等人理论计算机科学电子笔记310（2015）157见图9。 有轨电车沿着王子街的路线，由红线表示。 只有一个电车站在苏格兰皇家学院附近的红色标记处。我们认为的巴士 从左下角的蓝点开到右上角的橙点在补丁1到停止正如我们在前一节中所讨论的，当总线进入模块15的“接收器”时，路线的相关部分完成如果BusesInSink表示接收器中的总线数量，则提前超过一分钟的概率可以用PRISM的属性指定语言（基于CSL [ 2，3 ]）表示P=？ （trueU300 BusesInSink=1），<其中数字300对应于300秒或5分钟;我们假设这段路线计划花费6分钟，如3.3节所讨论的。同样，我们将迟到超过5分钟的概率表示为P=？ （BusesInSink = 0U> 660 BusesInSink = 1）。我们的案例研究的CTMC由164个状态和191个跃迁组成，这（舒适）使我们能够应用数值技术来评估这些公式。5案例研究：爱丁堡电车在本节中，我们讨论使用PRISM获得的结果如前所述，我们重点研究了在公共交通网络中增加有轨电车的案例，特别是在公共汽车时刻表保持不变的情况下，有轨电车对公共汽车准点性能的影响（如第4.2我们首先详细描述案例研究和几个相关的假设场景，然后再进行数值分析。5.1案例研究爱丁堡的有轨电车将服务于一条从位于城市西部的机场到位于市中心东北部的约克广场的单线。与王子街重叠的电车路线部分如图9所示。D. Reijsbergen等人理论计算机科学电子笔记310（2015）157173一个单一的电车站位于王子街，即在补丁8（看到这一点，比较图4和9）。一辆巴士从西向东（我们唯一考虑的方向）穿过补丁将两次穿过电车线：在补丁2和补丁12。虽然有轨电车不与公共汽车争夺进入站，我们investi门三个可能的其他方式，有轨电车的引入可能会影响公共汽车网络。第一个是补丁2和补丁12中额外的透光阶段的影响第二个是在8号地块增加交通灯的影响，这是因为行人需要穿过部分道路才能到达中间的电车站。第三是乘客乘坐电车而不是公交车对在补丁6和10的公交车站花费时间5.2电车横过巴士路线的影响在2号和12号线路中，有轨电车穿越公交线路的事实意味着需要增加一个额外的轻轨阶段来适应这一情况，或者需要延长现有的阶段。我们不能直接观察到这一效果是因为我们没有关于交通灯的数据来匹配AVL数据，所以我们不能准确地测量公共汽车何时在灯前等待。然而，我们可以通过比较城市相关部分的斑块来近似估计这一影响，我们知道它们在透射光行为方面有所不同;然后我们改变斑块2和斑块12中的逗留时间分布，使得平均行为相应地改变。如第3.3节所述，补丁7和补丁9之间的主要区别是透射光相位的数量。这种效应在超Erlang分布的参数中明显可见：Patch 9的μ1和μ2为了在补丁2和补丁11中加入这个效果，我们可以改变它们的hyper-Erlang参数，从而增加μ1和μ2在图10中，对此进行了研究。我们将速率λ1和λ2除以见图10。不准时的概率是x的函数，其中x是这样的，我们将补丁2和补丁12的速率λ1和λ2绿色（递减）线表示与当前时间表相比提前一分钟以上的概率。 蓝线（增加）代表与当前时间表相比，迟到超过五分钟的可能性174D. Reijsbergen等人理论计算机科学电子笔记310（2015）157补丁2和12通过常数x，并考虑准时概率作为x的函数：我们选择改变速率而不是相位数，因为速率变量可以被设置为等于任何实际值（我们目前没有速率和相位之间的差异的真实世界解释，所以我们没有改变任何一个的偏好）。 图中描述了早到一分钟以上（绿色，递减线）和晚到五分钟以上（蓝色，递增线）。这两个概率之和最低，约为1.45，这意味着，根据我们的模型，这样的阶段完成率的降低实际上有助于提高准时性能，因为准时的总概率和不提前的概率（最差的时间表偏差）都会增加。由于补丁7的μ1和μ2大约是补丁9的两倍，因此这种变化的影响大约为x= 2，这意味着公交车迟到的概率将高于公交车提前的概率;总的准时概率是相似的。5.3电车站补丁8中的电车站位于道路中间，这意味着行人需要一个交通灯，以便他们能够安全地到达或离开它。在补丁5中可以观察到系统中添加单个交通灯相位的影响。由于5号地块周