Traffic systems are multi-agent cyber-physical systems whose performance is closely related to human welfare. They work in open environments and are subject to uncertainties from various sources, making their performance hard to verify by traditional model-based approaches. Alternatively, statistical model checking (SMC) can verify their performance by sequentially drawing sample data until the correctness of a performance specification can be inferred with desired statistical accuracy. This work aims to verify traffic systems with privacy, motivated by the fact that the data used may include personal information (e.g., daily itinerary) and get leaked unintendedly by observing the execution of the SMC algorithm. To formally capture data privacy in SMC, we introduce the concept of expected differential privacy (EDP), which constrains how much the algorithm execution can change in the expectation sense when data change. Accordingly, we introduce an exponential randomization mechanism for the SMC algorithm to achieve the EDP. Our case study on traffic intersections by Vissim simulation shows the high accuracy of SMC in traffic model verification without significantly sacrificing computing efficiency. The case study also shows EDP successfully bounding the algorithm outputs to guarantee privacy.

翻译：交通系统是一种多智能体信息物理系统，其性能与人类福祉密切相关。这些系统在开放环境中运行，并受到来自多种来源的不确定性影响，使得传统基于模型的方法难以验证其性能。作为替代方案，统计模型检验（SMC）可通过顺序抽取样本数据来验证系统性能，直至能以所需统计精度推断出性能规范的正确性。本研究旨在验证具有隐私保护的交通系统，其动机在于所使用的数据可能包含个人信息（例如日常行程），并且通过观察SMC算法的执行过程可能意外泄露这些信息。为在SMC中形式化刻画数据隐私，我们引入了期望差分隐私（EDP）的概念，该概念约束了当数据发生变化时，算法执行在期望意义上可改变的程度。据此，我们为SMC算法引入了一种指数随机化机制以实现EDP。基于Vissim仿真对交通交叉口的案例研究表明，SMC在交通模型验证中具有高精度，且未显著牺牲计算效率。该案例同时表明，EDP成功限定了算法输出，从而保障了隐私。