Trustworthy and Explainable AI

Leverage the rigor of logic and translate verified logic evidence into faithful, human-centered explanations for complex AI outcomes.

We developed a Computation Tree Logic (CTL)-based explainer for Monte Carlo Tree Search (MCTS) in sequential transit planning. The method converts user queries into formal logic specifications, evaluates them over the search tree using CTL semantics, and returns semantically grounded explanations.

Building on this, we introduced LogiEx, a logic-integrated explanation framework that combines formal verification with large language models (LLMs) to interpret complex MCTS trees. LogiEx supports free-form queries, human-guided search exploration, and logic-grounded explanations, while ensuring faithfulness by validating responses against the underlying planning process.

My research further establishes a framework for reliable, verifiable, and human-centered explanations in complex planning systems across additional real-time domains. Future work will focus on deploying and evaluating this framework in collaboration with the Williamson County Department of Transportation, with the goal of addressing community concerns regarding school bus routing and scheduling decisions and assessing its effectiveness in real-world operational settings.

Related Publications

  • LogiEx: Integrating Formal Logic and LLMs for Explainable Transit Planning
    Ziyan An, Xia Wang, Hendrik Baier, Zirong Chen, Abhishek Dubey, Taylor T. Johnson, Jonathan Sprinkle, and Meiyi Ma
    Proceedings of the 17th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS), 2026
  • X-CPS: A Top-Down Hierarchical Framework for Explaining Learning-enabled Cyber-Physical Systems
    Guocheng He, Lingwen Deng, Ziyan An, and Meiyi Ma
    The 3rd International Workshop on Foundation Models for Cyber-Physical Systems & Internet of Things (FMSys'26), CPS-IoT Week, 2026
  • Combining LLMs with Logic-Based Framework to Explain MCTS
    Ziyan An, Xia Wang, Hendrik Baier, Zirong Chen, Abhishek Dubey, Taylor T. Johnson, Jonathan Sprinkle, Ayan Mukhopadhyay, and Meiyi Ma
    The 24th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS), 2025
  • Enabling MCTS Explainability for Sequential Planning through Computation Tree Logic
    Ziyan An, Hendrik Baier, Abhishek Dubey, Ayan Mukhopadhyay, and Meiyi Ma
    European Conference on Artificial Intelligence (ECAI), 2024
Logic-guided explanation for transit planning
Figure 1: A domain expert selects from a set of predefined checkbox queries about a transit plan. A CTL-based framework then evaluates the selected query over the planning search tree through a CTL checking process, and the explanation framework converts the CTL checking outputs into templated, human-readable results.
LogiEx Planning Explainer overview
Figure 2: The LogiEx Planning Explainer sits between the MCTS-based transit planner and a domain expert, interpreting the search process to answer free-form questions with logic-grounded, faithful responses validated against the underlying plan.