Integrating Formal Methods and Machine Learning for Smart Cities:

Conflict Detection and Resolution

Learn more »


Smart Newark:

Socially Informed Services Conflict Governance through Specification, Detection, Resolution and Prevention


Smart services are deeply embedded in modern cities aiming to enhance various aspects of citizens' lives, including safety, wellness, and quality of life. Examples include intelligent traffic control by Intel and air quality control by BreezoMeter. Given these services, monitoring a city's safety and performance collectively is crucial, yet also challenging due to many potential conflicts among the number increasing of services deployed. Researchers have accumulated abundant knowledge on how to design these services independently. However, underlying expected or unexpected couplings among services due to complex interactions of social and physical activities are under-explored, which lead to potential conflicts. Developing ways of reducing conflicts is essential for ensuring social inclusion and equity of city services because when conflicts occur, their impacts are likely to be concentrated in some sub-communities (e.g., specific geographic locations, specific user groups like patients with respiratory illness, etc.) meaning that some citizens will experience lower quality services than others due to the diversity. Put differently, service conflicts contribute to a digital divide in service provision.
Our real-world implementation of this theory by working with our partners in Newark NJ will show its effectiveness. The novelty of this theory is that it is first grounded in social science results where new insights were drawn from social data collection to better understand community diversity, inclusion, and equity in city service provisions to specify city requirement to build a consensus on the definition of a service conflict. It is then materialized with a set of sequential socially-informed technological merits for conflict detection, resolution, and prevention, and is further evaluated with both technological and social experiments. It finally creates societal impacts through social interventions (e.g., educational outreach, training session, etc.) to inclusively and equitably benefit a diverse set of stakeholders of conflict management from city operators, to service providers, to citizens.


A Watchdog for Safety-Aware Conflict Detection and Resolution in Smart Cities


Increasingly, cities are deploying smart services. IoT platforms are available to integrate smart services and city devices and improve city performance in the domains of transportation, emergency, environment, public safety, etc. Despite the increasing intelligence of smart services and the sophistication of platforms, the safety issues in smart cities are not addressed adequately, especially the safety issues arising from the integration of smart services. Therefore, CityGuard, a safety-aware watchdog architecture is developed. To the best of our knowledge, it is the first architecture that detects and resolves conflicts among actions of different services considering both safety and performance requirements. To start with, safety and performance requirements and a spectrum of conflicts are specified. Sophisticated models are used to analyze secondary effects, and detect device and environmental conflicts. A simulation based on New York City is used for the evaluation. The results show that CityGuard (i) identifies unsafe actions and thus helps to prevent the city from safety hazards, (ii) detects and resolves two major types of conflicts, i.e., device and environmental conflicts, and (iii) improves the overall city performance.

View details »

CityGuard Architecture



A Decision Support System for Conflict Resolution in Smart Cities


Resolution of conflicts across services in smart cities is an important yet challenging problem. We present CityResolver -- a decision support system for conflict resolution in smart cities. CityResolver uses an Integer Linear Programming based method to generate a small set of resolution options, and a Signal Temporal Logic based verification approach to compute these resolution options' impact on city performance. The trade-offs between resolution options are shown in a dashboard to support decision makers in selecting the best resolution. We demonstrate the effectiveness of CityResolver by comparing the performance with two baselines: a smart city without conflict resolution, and CityGuard which uses a priority rule-based conflict resolution. Experimental results show that CityResolver can reduce the number of requirement violations and improve the city performance significantly.

View details »

Violation Degree and Dashboard

violationdegree dashboard


Spatial Aggregation Signal Temporal Logic for Runtime Monitoring in Smart Cities


We present SaSTL---a novel Spatial Aggregation Signal Temporal Logic---for the efficient runtime monitoring of safety and performance requirements in smart cities. We first describe a study of over 1,000 smart city requirements, some of which can not be specified using existing logic such as Signal Temporal Logic (STL) and its variants. To tackle this limitation, we develop two new logical operators in SaSTL to augment STL for expressing spatial aggregation and spatial counting characteristics that are commonly found in real city requirements. We also develop efficient monitoring algorithms that can check a SaSTL requirement in parallel over multiple data streams (e.g., generated by multiple sensors distributed spatially in a city). We evaluate our SaSTL monitor by applying to two case studies with large-scale real city sensing data (e.g., up to 10,000 sensors in one requirement). The results show that SaSTL has a much higher coverage expressiveness than other spatial-temporal logics, and with a significant reduction of computation time for monitoring requirements. We also demonstrate that the SaSTL monitor can help improve the safety and performance of smart cities via simulated experiments.

View details »

City Requirements Analysis



Demo 1: Normal City without any service

A simulation for a normal city without any smart service is shown below. It is a part of Manhattan, New York City, NY. Traffic data is generated based on the real data from New York city. In the simulation, the yellow objectives are normal vehicles (e.g. cars, buses, trucks), and the red objectives are emergency vehicles. There are traffic signals in each intersection. The red lane is a blocked lane. As shown in the video, there are traffic congestions, blocked emergency vehicles and high air pollution emission when there is no smart service.


Demo 2: Comparison between without and with smart traffic service

Performances of a smart city without and with a smart traffic service are compared in the below videos. The initial states are the same for the two simulations. As it is shown in the videos, the city with the smart traffic service has a much better traffic performance. However, as shown in the zoom-in pictures below, pedestrians are blocked in the intersection because of the smart traffic service, i.e. the secondary effect of this smart service.

City without Smart Traffic Service

City with Smart Traffic Service

CityGuardStructure CityGuardStructure

Demo 3: Smart city without CityGuard

A smart city with 5 smart services are deployed in the simulation below. (S1: Traffic Congestion Service; S2: Pedestrian Service; S3: Air Pollution Service; S4: Noise Service; S5: Emergency Service). Without CityGuard, the performance of services is affected by the conflicts among them. It has a worse performance than the simulation with single service running. As a result, high traffic congestion, blocked emergency vehicles and air pollution are caused.

Demo 4: Smart city with CityGuard

A smart city with 5 smart services and CityGuard are deployed in the simulation below. (S1: Traffic Congestion Service; S2: Pedestrian Service; S3: Air Pollution Service; S4: Noise Service; S5: Emergency Service). Comparing with the previous simulation, it is shown that with CityGuard, (i) conflicts among services are detected and resolved, (ii) traffic has a much better performance, (iii) emergency vehicles have a shorter travel time, and most importantly, (iv) fewer conflicts happened when the previous conflicts are resolved by CityGuard. Therefore, overall city performance is improved by CityGuard.


  • Meiyi Ma, S. Masud Preum, W. Tärneberg, M. Ahmed, M. Ruiters, and J. Stankovic. Detection of Runtime Conflicts among Services in Smart Cities, Smart Computing (SMARTCOMP), 2016 IEEE International Conference on. IEEE, 2016. [pdf] [link]

  • Meiyi Ma, Sarah Masud Preum, and John A. Stankovic. "CityGuard: A Watchdog for Safety-Aware Conflict Detection in Smart Cities." Proceedings of the Second International Conference on Internet-of-Things Design and Implementation. ACM, 2017.[pdf] [link] [Slides]

  • Meiyi Ma, John A. Stankovic and Lu Feng. "CityResolver: A desicion support system for conflict resolution in smart cities" The 9th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS). ACM/IEEE, 2018.
    [pdf] [link] [Slides]

  • Meiyi Ma, John A. Stankovic, and Lu Feng. "Runtime Monitoring of Safety and Performance Requirements in Smart Cities." Proceedings of the 1st ACM Workshop on the Internet of Safe Things. ACM, 2017.[pdf] [link] [Slides]

  • Meiyi Ma, Ezio Bartocci, Eli Lifland, John Stankovic, and Lu Feng. "SaSTL: Spatial Aggregation Signal Temporal Logic for Runtime Monitoring in Smart Cities" The 9th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS). ACM/IEEE, 2018.
    [pdf] [link] [Talk]

  • Ma, Meiyi, Preum, S. M., Stankovic, J. A. (2017, April). Demo Abstract: Simulating Conflict Detection in Heterogeneous Services of a Smart City. In Internet-of-Things Design and Implementation (IoTDI), 2017 IEEE/ACM Second International Conference on (pp. 275-276). IEEE.[link]


John A. Stankovic (PI)

BP America Professor, Director, Link Lab

Department of Computer Science

University of Virginia

Meiyi Ma

Ph.D. Candidate

Department of Computer Science

University of Virginia