Formal Logic-Guided Harnessing Heterogeneous Fairness Rules in Smart Cities

Smart cities operate on computational predictive frameworks that collect, aggregate, and utilize data from large-scale sensor networks. However, these frameworks are prone to multiple sources of data and algorithmic bias, which often lead to unfair prediction results. In this work, we first demonstrate that bias persists at a micro-level both temporally and spatially by studying real city data from Chattanooga, TN. To alleviate the issue of such bias, we introduce FairGuard, a micro-level temporal logic-based approach for fair smart city policy adjustment and generation in complex temporal-spatial domains. The FairGuard framework consists of two phases. First, we develop a static generator that is able to reduce data bias based on temporal logic conditions by minimizing correlations between selected attributes. Second, to ensure fairness in predictive algorithms, we design a dynamic component to regulate prediction results and generate future fair predictions by harnessing logic rules. To navigate potential conflicts among these single fairness rules, including logical contradictions and data interference, we formulate detection strategies grounded in satisfiability modulo theories (SMT) across both logic and data levels. Furthermore, acknowledging the limitations of fairness rules focused on a single attribute, we enhance the static FairGuard to accommodate heterogeneous fairness rules that simultaneously consider multiple protected attributes. In addition, we develop an interactive online visualizer that displays the adjustments made to correct unfair city states, thereby improving fairness, alongside the prediction outcomes from the dynamic component. Evaluations showcase that logic-enabled static FairGuard can effectively reduce the biased correlations while dynamic FairGuard can guarantee fairness on protected groups at run-time with minimal impact on overall performance.

ACM Transaction on Cyber-Physical Systems