TY - GEN
T1 - Statistical Verification of Traffic Systems with Expected Differential Privacy
AU - Yen, Mark
AU - Dullerud, Geir E.
AU - Wang, Yu
N1 - Publisher Copyright:
© 2023 American Automatic Control Council.
PY - 2023
Y1 - 2023
N2 - 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.
AB - 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.
KW - differential privacy
KW - statistical verification
KW - traffic case study
UR - http://www.scopus.com/inward/record.url?scp=85167789939&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85167789939&partnerID=8YFLogxK
U2 - 10.23919/ACC55779.2023.10156637
DO - 10.23919/ACC55779.2023.10156637
M3 - Conference contribution
AN - SCOPUS:85167789939
T3 - Proceedings of the American Control Conference
SP - 3496
EP - 3501
BT - 2023 American Control Conference, ACC 2023
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 2023 American Control Conference, ACC 2023
Y2 - 31 May 2023 through 2 June 2023
ER -