爱丁堡巴士路线的优化研究与模型检验

可在www.sciencedirect.com在线获取理论计算机科学电子笔记310（2015）179-199www.elsevier.com/locate/entcs寻找爱丁堡巴士路线路易莎·维萨特的里雅斯特大学数学与地球科学系意大利的里雅斯特Allan Clark and Stephen Gilmore艾伦·克拉克和斯蒂芬·吉尔摩1，2爱丁堡大学计算机科学基础实验室苏格兰爱丁堡摘要我们提出了一种新的应用随机模拟和模型检查方法，以确定是否巴士服务是履行其服务水平协议，以提供准时离开巴士站succiently经常。我们使用预测的公交车到达时间的开放数据参数化的一个特定的巴士路线从爱丁堡市中心到郊区和农村地区的城市南部的随机模型。我们验证，然后分析我们的随机模型，使用模拟和模型检查方法。最后，我们完成了对模型的优化研究，并发现了一个更好的服务时间表，该时间表将使巴士服务运营商面临更小的财务风险，即监管机构对巴士服务、准时性和可靠性的标准进行了关键词：开放数据，参数拟合，相型分布，模拟，模型检验，优化。1引言在联合王国，交通委员会委员负责向重型货车、公共服务车辆和地方巴士服务的经营者颁发执照和进行监管，他们还可以对司机采取行动。他们有权在法律上获得保障，可以在法庭上进行正式的公开调查，以取得证据，协助他们作出决定，例如应否批出或拒绝批出牌照，或对巴士服务营办商或巴士、小巴或货车司机采取行动。他们出版了实务指引：本地巴士1这项工作得到了欧盟项目QUANTICOL，600708的支持2 电子邮件地址：stg@inf.ed.ac.ukhttp://dx.doi.org/10.1016/j.entcs.2014.12.0181571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/3.0/）。180L.L. Vissat等人理论计算机科学电子笔记310（2015）179概述巴士营办商须遵守的标准的服务 至[10]。在苏格兰，公共汽车运营商必须了解这些标准，苏格兰政府通过其“智慧苏格兰”倡议与他们合作，改善他们的服务。巴士准时改善伙伴关系（BPIP）报告[9]为运营商提供巴士服务设定了定义和目标。国家交通部的报告[ 2 ]中也使用了类似的关键概念定义，如我们的案例研究关注爱丁堡市公共交通系统的建模和分析爱丁堡的公共汽车完全装有GPS定位仪器，每隔30秒将其纬度和经度报告给中央服务器，该服务器使用预测模型来估计公共汽车站的到达时间。这些预测通过街道上的指示牌传达给公交车乘客，通过网站访问，并通过智能手机应用程序提供2公共汽车和准时自动车辆定位（AVL）设备与实时乘客信息系统的集成意味着信息被有效地传输给希望选择最佳巴士服务的乘客，以最快地将他们带到目的地。根据英国1985年交通法的规定，巴士经营者必须登记他们希望经营的任何巴士服务的路线和时间表。这必须包括路线上特定时间点的详细信息，这些时间点之间的间隔不应超过15分钟（除非下一个可用站点距离前一个站点的运行时间超过15分钟）。根据2001年PSV（本地服务注册）（苏格兰）法规，服务注册为频繁服务的情况除外，其中服务间隔为10分钟或更短，因此无需指定单独的时间。2.1巴士服务交通委员会委员苏格兰政府通过其“智慧苏格兰”倡议与运营商合作，通过公交车准时改善伙伴关系（BPIP）改善服务。2009年发布的BPIP报告为运营商提供巴士服务提出了定义和目标。2009年BPIP报告包括对准时的定义，这意味着公共汽车应该在提前一分钟和晚五分钟之间从公共汽车站出发，更常见的是被称为出发的容忍窗口这个窗口有意地是不对称的，以便早期运行的总线比后期运行的总线有更少的出错空间（因为有可能等待后期运行的总线，但L.L. Vissat等人理论计算机科学电子笔记310（2015）179181而不是一个早期的运行）。《2009年工商业政策和方案》报告中提供的其他定义包括准时和可靠性• 准时率：百分比数字计算为提早60秒至延迟五分钟的行车次数除以计划行车总数。• 可靠性：百分比计算为未运行的里程数除以计划运行的总里程数提供服务质素的具体目标乃根据旅程的不同阶段而定，而频密及非频密服务的具体目标亦有所不同。• 对于非频繁服务，95%的旅程应在路线开始时的“容忍窗口”内出发• 对于频繁的服务，预计在至少95%的情况下：· 在任何一段60分钟的时间内，将有六辆或以上的巴士开出;以及· 每班车之间的间隔不会超过十五分钟。区别对待频繁和非频繁服务的原因是，乘客使用频繁和非频繁服务的方式不同。乘搭班次频密的巴士（即每隔10分钟或以下一班车）的乘客，往往会在前往巴士站前，先不看时间表，因为他们在巴士站等候下一班巴士的机会不大。相比之下，使用非频繁服务的乘客（例如，服务间隔为一小时）几乎肯定会查看时间表，并期望公共汽车严格遵守时间表。对于沿巴士路线的后续计时点，标准再次略有不同。• 至于非班次班次频繁的巴士服务，交通运输署署长认为营办商应达到的最低标准，是在“容忍时间窗”内，有70%的巴士在路线上的时间点开出• 对于频繁服务，测量基于伦敦交通局的超额等待时间（EWT）概念[3]。这是从时间表中预计的平均等待时间与乘客在街上实际经历的时间· TC标准规定EWT不应超过1.25分钟。如果一项服务在一天中的部分时间只有10分钟或更少的服务间隔，那么整个服务是否应被视为频繁服务的问题尚不清楚。我们稍后将把我们的例子作为一个非频繁的服务，所以第一个规则对我们来说很重要（在2009年 BPIP报告中，对最终时间点的处理再次略有不同• 交通专员预计，95%的服务将在不超过5分钟的时间内到达最终目的地，并强调他们不会在行程结束时发现不适当的恢复时间·182L.L. Vissat等人理论计算机科学电子笔记310（2015）179• 然而，与起点和中间时间点相反，交通委员会委员并不使用到达旅程目的地的时间来评估运营商的准时表现。(It提前到达最终目的地并不被认为是一个问题2.2贸易专员2009年BPIP报告定义了不同运营条件下的预期服务水平。这些定义的严重性和严肃性在2010年得到了明确的体现，当时苏格兰交通专员对洛锡安巴士的运营进行了公开调查，以回应有关巴士过早运行的投诉。2010年7月，《苏格兰人报》报道了这一公开调查和Tra Bocc专员随后的决定Lothian Buses是一家广受尊敬的巴士公司。它是苏格兰唯一的市政巴士公司，也是英国最大的市政巴士公司。洛锡安巴士公司因其对爱丁堡和洛锡安的服务赢得了多个奖项，包括2002年和2003年的英国最佳巴士公司，2006年的苏格兰来自车辆和运营商服务局（VOSA）的检查员对洛锡安巴士4号、16号、27号和45号服务进行了监测，发现在303条服务中，23条服务出发太迟，44条服务出发太早，剩下的236条服务准时出发（根据容忍窗口的定义）。洛锡安巴士公司解释说，他们已经在时间表上增加了额外的时间，因为他们预计爱丁堡有轨电车系统需要铺设轨道的工程会然而，由于这些工程的预期滞留并没有像预期的那样糟糕，使该公司的许多苏格兰交通委员会专员罚款洛锡安巴士£ 10，500。该委员会有权将巴士公司罚款高达385，000英镑-计算如下550英镑是运营商授权水平的550倍当局在接获一宗有关巴士公司的投诉后，便为了将这一点放在上下文中，错过服务4，16，27或45巴士的客户可能不得不等待长达30分钟的下一辆巴士。2.3对公众询问2010年8月，洛锡安巴士公司在其网站上报告了对公众调查结果的回应。 该公司决定在其驾驶室自动车辆定位（AVL）系统中安装一个早期预警驾驶员警报系统。L.L. Vissat等人理论计算机科学电子笔记310（2015）179183Fig. 1.地图显示了从北桥（北部）到卡梅隆收费站、拉斯韦德路十字路口和邦尼里格收费站（南部）的四个时间点。每对计时点之间有许多巴士站。设备.如果驾驶员在到达时间点之前提前（至少一分钟）运行，则系统被激活。第一个警报是在时间点前两个公交车站触发的，并在司机的控制台上显示一条消息“减速：你来早了！“并发出警告蜂鸣器。如果车辆继续提前行驶，则会发出第二个警报并显示消息“等待时间：您提前了！” is displayed just prior to reaching the timing该系统是与法国实时乘客信息专家INEO合作开发的，INEO与Lothian巴士公司合作，为其整车配备AVL设备，并与实时乘客信息系统集成- Q-为评估公交服务而制定的正式框架，加上对这些法规的解释的日益严肃性，促使我们希望正式模拟这一运营条件系统，并询问我们是否可以确定未来对公交服务或公交正点改善伙伴关系所规定的法规的潜在变化是否会使公司在未来承担潜在责任3案例分析：31路公交车作为我们的案例研究，我们将考虑31路公交车，这是一条穿过市中心，然后向南行驶出爱丁堡市到南部农村地区的服务。我们将特别关注从市中心的北桥（NB）到卡梅伦收费站（CT），Lasswade Road Crossroads（LR）和Bonnyrigg Toll（BT）的七英里旅程。31服务的这四个时间点如图1所示。我们从提供的许多服务中选择了这项服务，因为它具有184L.L. Vissat等人理论计算机科学电子笔记310（2015）179在一条相对紧凑的路线上有许多不同的路况。在旅程开始时，公交车经历了繁忙的城市交通状况，高度拥堵，移动到交通压力较小的郊区，在旅程的最后一部分，基本上是开放的道路，几乎没有拥堵。此外，时刻表还提供了一个白天从北桥出发的简单模式，使我们能够轻松记住出发模式，并在图表和模型结果中参考。在此服务中，我们将特别关注工作日中的一段时间，该服务作为频繁服务运营，在整点从北桥出发，并在11：20至16：10之间时间表如图2所示。时刻表中对服务的描述可以解释为一个确定性的过程，时间点之间的精确行程时间为16分钟、8分钟和10分钟。这显然是一个抽象的概念，而这个系统的具体实现将是一个随机过程，会因交通情况、交通控制和信号、乘客人数和服务需求的波动、行人和其他道路使用者，甚至天气情况而引起延误。NB. CT. LR. BT（以分钟为单位的确定性持续时间：16、。8，. 10）、图二、31路巴士时刻表，显示计划从北桥（NB），卡梅伦收费（CT），Lasswade路十字路口（LR）和Bonnyrigg收费（BT）出发3.1从Bus Tracker网站获取数据时间表中使用的名称可以映射到巴士站的名称，以获得一个八位数的数字停车代码，该代码可用于访问爱丁堡巴士跟踪网站www.example.com上的实时乘客信息http://mybustracker.co。英国. 图3显示了时间表名称到公交车站的映射。八位停车代码可以作为参数传递给Bus Tracker代码时刻表/BusTracker停止代码NB北桥/北桥36234754CT金马伦收费购物中心/金马伦收费36234845LRLasswade Road十字路口/Captain36237956BTBonnyrigg收费/公园路64323292图3.第三章。 31服务路线上计时点的名称和代码L.L. Vissat等人理论计算机科学电子笔记310（2015）1791851412108642011：20：00 11：30：00 11：40：00 11：50：00 12：10：00 12：20一天见图4。将时间表模型与巴士追踪网站报道的北桥预测等待时间进行比较。如下图所示，请浏览网站，以获取有关此站离港的实时信息。http://mybustracker.co.uk/? module=consult&mode=busStopQuickSearch&busStopCode=36234754可以使用Python编程语言实现的脚本以编程方式获得此网页。该脚本检索网页并使用Beautiful SoupHTML解析库[7]提取所需的语义内容，即31路公交车下一次发车前等待的分钟数。这一信息在一天中每30秒在路线上的四个定时点上收集一次3.2时间表数据和预测等待时间该过程收集的数据可以可视化，并与时间表进行比较，如图4所示。Bus Tracker网站以一分钟的粒度报告预测等待时间，短等待时间映射到单词因此，研究BusTracker网站的观察者会期望看到值10，9，8，7，6，5，4，3，DUE的单调递减序列，在实践中，由于延迟，观察者可能会看到大于10的值，并且由于Bus Tracker服务对等待时间预测的修改，预测等待时间的序列将不总是一系列单调递减的序列。我们在2013年11月的一段时间内收集了31辆巴士服务的数据。图5显示了2013年11月19日11：10至16：20之间五个小时内的数据收集结果。从这个短暂的观察期中几乎无法得出任何结论，除了注意到最长的等待时间出现在路线的终点，最长的等待时间（超过20分钟）出现在Bonnyrigg收费站。二O一三年十一月十九日北桥时刻表北桥数据等待分钟数186L.L. Vissat等人理论计算机科学电子笔记310（2015）179北大桥卡梅伦收费站拉斯韦德路邦尼里格收费站北大桥卡梅伦收费站拉斯韦德路邦尼里格收费站北大桥卡梅伦收费站拉斯韦德路邦尼里格收费站等待分钟数等待分钟数二O一三年十一月十九日25二O一三年十一月十九日2520 2015 1510 105 5011：20：00 11：30：00 11：40：00 11：50：00 12：00：00 12：10：00 12：20：00一天（一）0十一点半十一点四十五分12：00：00十二点十五分十二点半十二点四十五分13：00：0013点15分一天（b）第（1）款二O一三年十一月十九日25二O一三年十一月十九日2520 2015 1510 105 5011：30：00 12：30：00 13：00：00 13：30：00 14：00：00一天（c）第（1）款0十一点半12：00：00十二点半13：00：0013点半14：00：0014点半15：00：00一天（d）其他事项二O一三年十一月十九日25二O一三年十一月十九日25北大桥卡梅伦收费站拉斯韦德路邦尼里格收费站北大桥卡梅伦收费站拉斯韦德路邦尼里格收费站北桥的累积平均数金马伦收费站的累积平均数Lasswade路的累积平均数Bonnyrigg收费站的累积等待分钟数等待分钟数L.L. Vissat等人理论计算机科学电子笔记310（2015）179187等待分钟数20 2015 1510 105 5011：30：00 12：00：0012：30：00 13：00：0013：30：00 14：00：0014：30：00 15：00：0015点30分16点00分一天（五）011：30：00 12：00：0012：30：00 13：00：0013：30：00 14：00：0014：30：00 15：00：0015点30分16点00分一天（f）第（1）款图五.2013年11月19日，31路公交车在各时间点的预计等待时间，一小时，（b）两小时，（c）三小时，（d）四小时，（e）五小时。累积平均等候时间见（f）。等待分钟数188L.L. Vissat等人理论计算机科学电子笔记310（2015）1793.3将等待时间数据转换为出发事件从2013年11月的一段时间内收集的数据中，我们可以检测到出发事件，因为它们包括一系列等待时间短的观察，然后等待时间突然增加（当我们从等待一辆公共汽车到等待下一辆公共汽车时）。这些事件在本质上不同于预测等待时间，因为它们表示已经发生的事件，而不是对在预测时间可能发生或可能不发生的事件的预测。丢弃预测数据并仅保留离开事件数据，我们得到了有用的数据片段。将其与时间表相关联，如图6所示，我们能够确定行程时间。收集计算出的旅行时间，我们可以编制旅行时间的分布时间17点整16点整15点整14点整13点整十二点整十一点整0 2 4 6 8距离（英里）见图6。将出发事件和距离北桥的英里数与出发相关联，时间表。Cameron Toll旅馆距离北桥有2.1英里，距离Lasswade Road Crossroads十字路口有4.7英里，距离Bonnyrigg Toll旅馆有6.9英里。4用HyperStar行程时间的经验分布用作数据集，并作为数据拟合工具的输入HyperStar [8]是一种用于将相位类型分布拟合到数据集的软件工具相位型分布具有理想的性质，它们可以任意接近地近似任何具有非负支撑的分布除此之外，它们还可以表示为连续时间马尔可夫链（CTMC），这意味着任何支持CTMC的建模工具都可以处理由相位类型分布组成的模型。我们感兴趣的建模工具包括Bio-PEPA Eclipse插件，用于执行离散事件模拟，可表示为以适合Traviando跟踪分析器的格式记录的状态事件跟踪;和PRISM概率模型检查器，用于验证连续随机逻辑（CSL）的公式。2013年11月21日，星期四×31路公交车，时刻表数据++的+的×+++×+×+×+×++×产品介绍×+×++++×+××+×+×+×++××+×+×+×++的产品介绍+×+×+×++的××+产品介绍×+++的×+××+×+×+××+++×++×+×+×++的产品介绍×+×+×+×+×+×+×+×+×+×+×+×+×+×+×+×+××++××产品××+×L.L. Vissat等人理论计算机科学电子笔记310（2015）179189每个阶段的行程时间的分布映射到一个随机过程，使用HyperStar。此过程的结果是数据的拟合CDF和拟合PDF，如图7所示。HyperStar可以自由选择任何相位类型分布来拟合数据，但在我们的每个阶段，相位类型拟合的结果都是Erlang分布。巴士路线上各时间点之间的所有行车时间未必如此，因此我们不想预先假设此分布，而是通过使用中的拟合程序为我们选择最佳拟合。Erlang分布可能会经常出现，因为时间点位置的限制意味着它们往往沿着路线相隔10交通专员条例意味着它们不应该相距太远，想要有一个简明的时间表意味着它们不应该太近。这种紧张局势往往会将它们分开，从而使整个旅程时间变得更加可预测。在其他工作[6]中，HyperStar返回了hyper-Erlang发行版。见图7。使用HyperStar安装从北桥到卡梅伦收费站的旅程HyperStar拟合程序为旅程的三个阶段产生以下结果。旅程阶段率NB. CT阶段1=105比率1= 6。47CT. LR阶段2=83速率2= 8。79LR. BT阶段3=98比率3= 10。54我们可以快速检查这些随机过程参数，这些参数来自我们从Bus Tracker网站收集的数据，与公交时刻表中公布的确定性模型之间的关系。我们使用每个指数分布的参数来计算平均持续时间，并将此平均持续时间想象为Erlang分布中每个阶段的持续时间。然后，我们乘以每个Erlang中的阶段数，以获得近似的平均持续时间。190L.L. Vissat等人理论计算机科学电子笔记310（2015）179由指数分布事件数目组成的随机过程。NB. CT1速率1 ×阶段1=十六岁24>16（时间表）CT. LR1速率2 ×阶段2=第九章44>8（时间表）LR. BT1速率3 ×阶段3=第九章30<10（时间表）我们发现，对于从我们的数据集得出的随机过程，似乎在所需的时间范围内最难完成的部分旅程这一观察结果源于这样一个事实，即根据我们的行程时间数据估计的平均总持续时间大于表中的8分钟。我们可以直观地看到由图8中的数据拟合过程产生的随机过程。它是一个由三个Erlang分布组成的系列，分别有105、83和98个相位。构成第一个Erlang的指数分布的速率为6.47。构成第二个Erlang的指数分布具有8.79. 构成第三个Erlang的指数分布的速率为10.54。NB. . . . . . . . . . . . . . . . . . . . . . . .. .. . . ... . . . . . . . . . . . . . . . . . .. . . . . .CT. . . . . . . . . . . . . . . . . . . . . . . .. .. . .. . . . . . . . . . . . . . . . . . . .. . . . .LR. . . . . . . . . . . . . . . . . . . . . . . .. .. . .. . . . . . . . . . . . . . . . . . . . .. . . .105指数。 利率6.47，83个指数 利率8.79，98指数。 比率10.54BT见图8。 随机过程建模的旅程NB。CT. LR. BT5Kolmogorov-Smirnov检验在拟合程序和编写模型之后，我们可以尝试确定MyBusTracker的真实数据和我们的模型结果是否存在显著差异。为此，我们可以部署Kolmogorov-Smirnov检验（KS检验），它用于量化样本的经验分布函数与参考分布的累积分布函数之间的距离（单样本KS检验），或比较两个分布（双样本KS检验）。 对于我们的案例，我们给出了使用Matlab计算的Kolmogorov-Smirnov检验的结果，其中h是假设检验结果，0表示接受零假设，1表示拒绝零假设，显著性水平为0。05. p表示p值，作为范围[0， 1]内的标量返回。p是在零假设下观测到与观测值一样极端或比观测值更极端的检验统计量的概率。小的p值使零假设的有效性受到ksstat表示检验统计量，cv表示临界值。L.L. Vissat等人理论计算机科学电子笔记310（2015）179191图第九章第一、第二和第三阶段的CDF和经验CDF旅程Hp克斯塔特CVNB00。37250。11830。1767CT00。69720。10690。2076LR00。60910。11640。2101在图9中，我们表示不同阶段的CDF和经验CDF 整个旅程。6Bio-PEPA编码由HyperStar计算并使用KS检验进行检查的基础随机过程可以直接在Bio-PEPA随机过程代数中进行编码[1]。每个Erlang分布的每个阶段都有一个物种• NB 1，. NB阶段1，• CT 1，... CT第2阶段，• LR 1，. LR阶段3，• BT1192L.L. Vissat等人理论计算机科学电子笔记310（2015）179动力学定律都很简单，只依赖于一种物种类型的种群，所以质量作用定律不起作用。• nbToCti=[速率1×NBi]• ctToLri= [速率2×CTi]• lrToBti= [速率3×LRi]物种反应是简单的交换。反应nbToCt1使阶段NB1的总线数量减少一个，并使阶段NB2的总线数量增加一个。• NB1 = nbToCt1↓• NB2= nbToCt1↑ +nbToCt2↓如果把它们看作是一系列的反应事件，它们中的每一个也都是简单的。在以反应为中心的观点中，我们有：• nbToCt1：NB1→ NB2这个反应表达式的含义是反应nbToCt1（对应于北桥和金马伦收费站之间的旅程的第一阶段）将停靠在旅程第一阶段的公共汽车（NB1）转换为停靠在旅程第二阶段的公共汽车（NB2）。这是一个随机模型，可以作为连续时间马尔可夫链进行分析，也可以使用MonteCarlo程序（如Gillespie直接法）进行模拟6.1执行不早退的规定早出发给洛锡安巴士公司带来了问题，导致了公众调查和罚款。与晚发车相反，早发车（原则上）可以通过指示司机在公共汽车时刻表上公布的发车时间之前不要离开公共汽车站来防止这似乎是解决问题的一个如此明显简单的解决方案，以至于人们可能会想为什么运营商没有采用它一个问题是，早跑的公共汽车，耐心地等待时间离开一个时间点，可能会导致后面的公共汽车迟到。人们可能会认为，后面的公共汽车可以让乘客离开车站，改变车道，然后超过等待的公共汽车。然而，这是不可能的，因为英国的公共汽车运营商必须在公共汽车站上车。这一要求是因为老年人、盲人和残疾人也使用公共汽车，要求他们离开公共汽车站上车对他们来说可能很困难。由于乘客的礼貌和残疾人的无障碍环境对公司很重要，为了遵守安全规定，司机可以在适当的时候提前离开巴士站。6.2尝试不早退的规则因为我们有一个系统的动态模型，我们至少可以在抽象的实验中尝试“不提前出发”的想法L.L. Vissat等人理论计算机科学电子笔记310（2015）179193BTCTLRNB数量（对数标尺）⎪100000 10000010000 100001000 1000100 10010 10101020时间（分钟）30 4050101020时间（分钟）30 40 50见图10。允许早期偏离的Bio-PEPA模型的100，000次模拟的对数标度图（左）和不允许提前离开（右）。和到达时间。这个生物PEPA模型只需要两个小的变化，以执行没有提前离开的规则。首先，改变控制离开卡梅隆收费站的动力学定律。• 替换nbToCt阶段1 =[速率1×NB阶段1]• 通过nbToCt阶段1= [H（时间-15）×速率1×NB阶段1]函数H（）是Heaviside函数，其有效地切换反应，直到允许的时间（16分钟模拟前的一分钟H（x）=0⎩0如果x 0，1否则第二，在Lasswade路做相应的改变。• 替换ctToLr阶段2= [速率2×CT阶段2]• 通过ctToLr阶段2= [H（时间-23）×速率2×CT阶段2]这些变化是紧凑的，并且相对容易理解，但是它们的后果是模型不能再被认为是时间齐次连续时间马尔可夫链，因为对时间变量（时间）在动力学定律中，意味着模型现在是时间非均匀的。这有这样的后果，该模型可以分析的模拟方法，允许离散的时间相关的事件，但它不能分析的程序，用于分析经典的马尔可夫链的概率模型检验的数值线性代数。图10给出了允许提前离场和不允许提前离场的模拟结果。图中显示了在从北桥出发后16分钟从卡梅伦收费站出发和在从北桥出发后24分钟从拉斯韦德路十字路口出发的情况下，关于可取消的出发事件（提前1分钟至延迟5分钟）的BTCTLRNB数量（对数标尺）194L.L. Vissat等人理论计算机科学电子笔记310（2015）1797使用Traviando进行Traviando [5]是一个事后仿真跟踪分析器，它以状态/事件格式读取仿真跟踪。Bio-PEPA模型可以生成Traviando格式的痕迹，允许对这些痕迹进行分析。轨迹是单一和离散的，在有限的时间范围内执行一次模型Traviando允许用户可视化跟踪，计算统计属性，并执行LTL模型检查。它的目的是让建模者检查他们的模拟是否已经执行了模型的所有方面，并寻找其他问题（7.1检查我们的Bio-PEPA模型的单个模拟我们在我们的Bio-PEPA模型上检查了LTL公式。• (ttUCT）· “eventually,· 我们所有的模拟都是如此。• (ttUBT）· “eventually,· 这并不总是正确的，一些模拟过早终止。• (ttUCT）→（ttUNB）· “You cannot reach Cameron Toll without reaching North· 我们所有的模拟都是如此。• (ttULR）→（ttUCT）· “You cannot reach Lasswade Road without reaching Cameron Toll· 我们所有的模拟都是如此。• (tt U CT）→（tt U LR）· “You cannot reach Cameron Toll without reaching Lasswade Road· 这并不总是正确的，一些模拟过早终止。完成这些测试后，我们确信在Bio-PEPA中表达模型时没有我们还为我们的模拟确定了必要的模拟时间范围。8使用PRISM进行我们使用PRISM [4]（一种著名的概率模型检查器）进行概率模型检查PRISM实现了符号数据结构和算法，并支持统计模型检查，但我们的模型是紧凑的，因此可以有效地解决，而无需求助于符号或统计方法。该模型如图11所示。Erlang分布的速率和相位数与HyperStar之前推断的一样。L.L. Vissat等人理论计算机科学电子笔记310（2015）179195−- -ctmc模块总线31stage：[0.. 3] initNB; pos1：[1.. 阶段1]初始化1;位置2：[1.. 阶段2]初始化1;位置3：[1.. 阶段3]初始化1;[nb_ to_ ct]（阶段=NB_pos1阶段1）→速率1：（posJ1= pos1+ 1）;[到达_ct]（阶段=NB_pos1=阶段1）<→速率1：（阶段J=CT）;[ct_to_lr]（分期= CT分期pos 2<阶段2） →速率2：（pos J2 = pos2+ 1）;[到达_lr]（分期= CT分期pos 2=阶段2）- 速率2：（阶段J=LR）;[lr_to_bt]（阶段=LR_pos3阶段3）-速率3：（posJ3= pos3+ 1）;[arrive_bt]（阶段=LR_pos3=阶段3）-速率3：（阶段J=BT）;<端模见图11。 PRISM模型编码NB的CTMC表示。CT. LR. BT公交车准时性改善伙伴关系的总体目标是提高公交车准时性。具体而言，在正式术语中，这可以包括对偏离事件的容忍窗口更窄的窗口对应于更好的服务，公共汽车出发的时间不那么早，也不那么晚。逻辑CSL提供了一种非常方便的方法，允许我们通过一个简单的模型检查问题来探索这个我们评估CSL有界直到公式Pr =？[（stageN<）U[l，u]（stage=N）]对于出发时间上的下界l和上界u的不同值。 公式问什么是在区间[l，u]中发生向行程的第N阶段的过渡的概率。图12显示了对旅程的三个阶段的探索结果每个曲面图的左后曲线描述了禁止延迟偏离的效果（将公差窗口从[ 1， 5]更改为[ 1， 0]）。每个曲面图的右后曲线描述了禁止早期偏离的效果（将公差窗口从[ 1， 5]更改为[0， 5]）。当然，当窗口向[0，0]从这些图表中我们可以看到，提前发车最常见于卡梅伦收费站，最不常见于拉斯韦德路（因为右后弯道在卡梅伦收费站处最陡，在拉斯韦德路处最不陡）。我们注意到，所有时间点都满足运营商的要求，即在苏格兰定义的公差窗口[-1，5]内，有（至少）70%的巴士在路线上的时间点出发。9验证独立我们将旅程建模为三个独立的阶段（NB。 CT. LR. BT）。这个决定似乎过于简单，因为旅程的各个阶段肯定不是独立的。毕竟我们追踪的是同一辆巴士196L.L. Vissat等人理论计算机科学电子笔记310（2015）179见图12。 对于不同大小的窗口，计算在公差窗口内偏离的概率。在旅程的各个阶段，几乎总是在所有三个阶段使用相同的驱动程序由于驾驶员将意识到他们早（或相应地晚）离开了站点，因此可能认为他们将尝试通过较慢（或相应地更快）驾驶来在旅程的下一阶段中如果驾驶员正在补偿偏离时间表，那么我们预计后续阶段之间会出现负相关（因为驾驶员试图平衡较慢的阶段和较快的阶段，反之亦然）。我们决定调查这个驾驶员补偿理论，看看我们是否能在现有的数据中找到证据。我们使用了一个与用于参数化模型的数据集不同的样本外数据集，以确保我们不会被重新验证。图13显示了结果。在我们现有的数据中，我们无法找到强有力的证据来支持驾驶员补偿理论，因此我们没有将其纳入模型的重大压力。10优化问题显然，有一个优化问题需要解决，即：该模拟模型已通过HyperStar拟合程序进行参数化，并使用Kolmogorov-Smirnov检验进行检查以给出合理的结果。因此，我们能够将仿真模型生成的结果视为可用于探索优化空间的可靠样本源L.L. Vissat等人理论计算机科学电子笔记310（2015）179197图十三.在BusTracker数据中寻找连续阶段的行程时间（以秒表示）之间的相关性。强相关性在散点图中会显示为一条直线。没有强烈的相关性被认为是支持理论的驱动程序补偿，从而证明模型中所代表的阶段之间的独立性。模型的。如前所述，我们优化的关键是找到一个更好的时间表，即它使服务运营商的财务责任比目前公布的时间表减少。图14示出了在定时点处的到达时间的组合的优化表面。每个曲线图比较两个定时点处的到达时间，询问曲线图中的每个点有多少到达落在公差窗口每个（x，y）对都有几个垂直点，因为这些点表示该图中未提及的停靠点中变化的到达时间的未命中例如，第一个图表绘制了Cameron Toll和Lasswade Road的结果，并且具有相同x和y坐标的垂直点对应于Bonnyrigg Toll计时点考虑的不同可能到达时间。11探索参数空间公交时刻表将到达时间表示为整分钟，没有小数部分，因此可以通过整数域上的参数扫描来搜索最佳时刻表配置以最佳拟合模型结果。我们并不是在一个稠密的领域中寻求解决方案。在探索参数空间时，模型的结构保持不变，因此在此阶段的工作中不存在状态空间生成问题的风险。在现阶段，我们所要做的，只是研究修订行车时间表是否会减低巴士公司的风险。最重要的是，这将不需要对巴士的驾驶方式进行任何操作上的改变。特别是，我们并不是建议司机在旅程的任何部分调整他们的速度，只是调整时间表，以更好地配合目前正在做的事情。我们用我们的模拟模型计算了随机模拟的集合，并计算了在到达时间的每个可能组合的时间点处有多少偏离将位于偏离的容限窗口之外图15展示了我们对可信的198L.L. Vissat等人理论计算机科学电子笔记310（2015）1793736353433322625311124121323拉斯韦德路14221521卡梅伦托尔161720见图14。在定时点处的到达时间组合的优化曲面。可能的时间表值的参数扫描图15个。探索不同行程持续时间的参数空间为三个阶段的旅程。到达下游巴士站的时间。在我们的可视化中，更少的未命中对应于更大、更红的点，更多的未命中被渲染为更小、更黑的点。越少失误越好。我们看到，当我们从盒子的中心向外辐射时，点的大小和颜色都在减少。这让我们确信，我们已经探索了足够的搜索空间，找到了最优值。到达时间的最佳配置重要的是，邦尼里格收费