Publications
Years: 2025・2024・2023・2022・2019・2018
2025
Towards Responsible AI: Advances in Safety, Fairness, and Accountability of Autonomous Systems
Filip Cano Córdoba PhD Thesis, 2025. 
Abstract: Ensuring responsible use of artificial intelligence (AI) has become imperative as autonomous systems increasingly influence critical societal domains. However, the concept of trustworthy AI remains broad and multi-faceted. This thesis advances knowledge in the safety, fairness, transparency, and accountability of AI systems. In safety, we extend classical deterministic shielding techniques to become resilient against delayed observations, enabling practical deployment in real-world conditions. We also implement both deterministic and probabilistic safety shields into simulated autonomous vehicles to prevent collisions with road users, validating the use of these techniques in realistic driving simulators. We introduce fairness shields, a novel post-processing approach to enforce group fairness in sequential decision-making settings over finite and periodic time horizons. By optimizing intervention costs while strictly ensuring fairness constraints, this method efficiently balances fairness with minimal interference. For transparency and accountability, we propose a formal framework for assessing intentional behaviour in probabilistic decision-making agents, introducing quantitative metrics of agency and intention quotient. We use these metrics to propose a retrospective analysis of intention, useful for determining responsibility when autonomous systems cause unintended harm. Finally, we unify these contributions through the reactive decision-making framework, providing a general formalization that consolidates previous approaches. Collectively, the advancements presented contribute practically to the realization of safer, fairer, and more accountable AI systems, laying the foundations for future research in trustworthy AI.
BibTex:
@phdthesis{cano2025towards,
title = "Towards Responsible AI: Advances in Safety, Fairness, and Accountability of Autonomous Systems",
author = "{Cano C\'ordoba}, Filip",
year = "2025",
school = "Graz University of Technology (90000)",
}
Fairness Shields: Safeguarding against Biased Decision Makers
Filip Cano, Thomas A. Henzinger, Bettina Könighofer, Konstantin Kueffner, Kaushik Mallik.
AAAI Conference on Artificial Intelligence (AAAI) 2025. 
Abstract: As AI-based decision-makers increasingly influence decisions that affect humans, it is crucial to ensure their decisions are fair and unbiased. Most algorithms for fair decision-making provide probabilistic guarantees of fairness over the long run, not providing any guarantees at specific intervals, such as yearly or quarterly. In this paper, we introduce a novel neurosymbolic approach to guarantee fairness in every finite run through the use of a symbolic runtime enforcer called a *fairness shield*. The fairness shield monitors and minimally intervenes in the decision-maker’s decisions to ensure that fairness criteria are met either within a bounded horizon or periodically, while also minimizing the costs associated with such interventions as specified by a given cost function. Given a distribution over future decisions and their costs, we present algorithms to compute fairness shields by solving a bounded-horizon optimal control problem. We present synthesis algorithms for four types of fairness shields, each tailored to different operational settings. Our empirical evaluation demonstrates the effectiveness of these shields in ensuring fairness while maintaining cost efficiency across various scenarios.
2024
Abstraction-Based Decision Making for Statistical Properties
Filip Cano, Thomas A. Henzinger, Bettina Könighofer, Konstantin Kueffner, Kaushik Mallik.
International Conference on Formal Structures for Computation and Deduction (FSCD) 2024.
Abstract: Sequential decision-making in probabilistic environments is a fundamental problem with many applications in AI and economics. In this paper, we present an algorithm for synthesizing sequential decision-making agents that optimize statistical properties such as maximum and average response times. In the general setting of sequential decision-making, the environment is modeled as a random process that generates inputs. The agent responds to each input, aiming to maximize rewards and minimize costs within a specified time horizon. The corresponding synthesis problem is known to be PSPACE-hard. We consider the special case where the input distribution, reward, and cost depend on input-output statistics specified by counter automata. For such problems, this paper presents the first PTIME synthesis algorithms. We introduce the notion of statistical abstraction, which clusters statistically indistinguishable input-output sequences into equivalence classes. This abstraction allows for a dynamic programming algorithm whose complexity grows polynomially with the considered horizon, making the statistical case exponentially more efficient than the general case. We evaluate our algorithm on three different application scenarios of a client-server protocol, where multiple clients compete via bidding to gain access to the service offered by the server. The synthesized policies optimize profit while guaranteeing that none of the server’s clients is disproportionately starved of the service.
BibTex:
@inproceedings{cano2024abstraction,
author = {Cano, Filip and Henzinger, Thomas A. and K\"{o}nighofer, Bettina and Kueffner, Konstantin and Mallik, Kaushik},
title = {Abstraction-Based Decision Making for Statistical Properties},
booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
pages = {2:1--2:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
year = {2024},
volume = {299},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany}
}
soid: a Tool for Legal Accountability for Automated Decision Making
Samuel Judson, Matthew Elacqua, Filip Cano, Timos Antonopoulos, Bettina Könighofer, Scott J. Shapiro, Ruzica Piskac.
International Conference of Computer Aided Verification (CAV) 2024.
Abstract: We present soid, a tool for interrogating the decision making of autonomous agents using SMT-based automated reasoning. Relying on the Z3 SMT solver and KLEE symbolic execution engine, soid allows investigators to receive rigorously proven answers to factual and counterfactual queries about agent behavior, enabling effective legal and engineering accountability for harmful or otherwise incorrect decisions. We evaluate soid qualitatively and quantitatively on a pair of examples, i) a buggy implementation of a classic decision tree inference benchmark from the explainable AI (XAI) literature; and ii) a car crash in a simulated physics environment. For the latter, we also contribute the soid-gui, a domain-specific, web-based example interface for legal and other practitioners to specify factual and counterfactual queries without requiring sophisticated programming or formal methods expertise.
BibTex:
@inproceedings{judson2024soid,
title={soid: {A} Tool for Legal Accountability for Automated Decision Making},
author={Judson, Samuel and Elacqua, Matthee and Cano, Filip and Antonopoulos, Timos and K{\"o}nighofer, Bettina and Shapiro, Scott J. and Piskac, Ruzica},
booktitle = {Computer Aided Verification - 36th International Conference, {CAV}},
series = {Lecture Notes in Computer Science},
volume = {14682},
pages = {233--246},
publisher = {Springer},
year = {2024}
}
'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions
Samuel Judson, Matthew Elacqua, Filip Cano, Timos Antonopoulos, Bettina Könighofer, Scott J. Shapiro, Ruzica Piskac.
ACM Symposium on Computer Science and Law (CSLAW) 2024.
Abstract: Principled accountability in the aftermath of harms is essential to the trustworthy design and governance of algorithmic decision making. Legal theory offers a paramount method for assessing culpability: putting the agent ‘on the stand’ to subject their actions and intentions to cross-examination. We show that under minimal assumptions automated reasoning can rigorously interrogate algorithmic behaviors as in the adversarial process of legal fact finding. We use the formal methods of symbolic execution and satisfiability modulo theories (SMT) solving to discharge queries about agent behavior in factual and counterfactual scenarios, as adaptively formulated by a human investigator. We implement our framework and demonstrate its utility on an illustrative car crash scenario.
BibTex:
@inproceedings{judson2024put,
title={'Put the Car on the Stand': {SMT}-based Oracles for Investigating Decisions},
author={Judson, Samuel and Elacqua, Matthee and Cano, Filip and Antonopoulos, Timos and K{\"o}nighofer, Bettina and Shapiro, Scott J. and Piskac, Ruzica},
booktitle = {Proceedings of the Symposium on Computer Science and Law, {CSLAW}
2024, Boston, MA, USA, March 12-13, 2024},
pages = {73--85},
publisher = {ACM},
year = {2024}
}
2023
Analyzing Intentional Behavior in Autonomous Agents under Uncertainty
Filip Cano Córdoba, Samuel Judson, Timos Antonopoulos, Katrine Bjørner, Nick Shoemaker, Scott J. Shapiro, Ruzica Piskac, Bettina Könighofer.
International Joint Conference of Artificial Intelligence (IJCAI) 2023. 
Abstract: Principled accountability for autonomous decision-making in uncertain environments requires distinguishing intentional outcomes from negligent designs from actual accidents. We propose analyzing the behavior of autonomous agents through a quantitative measure of the evidence of intentional behavior. We model an uncertain environment as a Markov Decision Process (MDP). For a given scenario, we rely on probabilistic model checking to compute the ability of the agent to influence reaching a certain event. We call this the scope of agency. We say that there is evidence of intentional behavior if the scope of agency is high and the decisions of the agent are close to being optimal for reaching the event. Our method applies counterfactual reasoning to automatically generate relevant scenarios that can be analyzed to increase the confidence of our assessment. In a case study, we show how our method can distinguish between 'intentional' and 'accidental' traffic collisions.
BibTex:
@inproceedings{canocordoba2023analyzing,
title={Analyzing Intentional Behavior in Autonomous Agents under Uncertainty},
author={Cano C{\'o}rdoba, Filip and Judson, Samuel and Antonopoulos, Timos and Bj{\o}rner, Katrine and Shoemaker, Nicholas and Shapiro, Scott J and Piskac, Ruzica and K{\"o}nighofer, Bettina},
booktitle = {Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, {IJCAI} 2023},
year={2023}
}
Safety Shielding under Delayed Observation
Filip Cano Córdoba, Alexander Palmisano, Martin Fränzle, Roderick Bloem, Bettina Könighofer.
International Conference on Automated Planning and Scheduling (ICAPS) 2023.
Abstract: Agents operating in physical environments need to be able to handle delays in the input and output signals since neither data transmission nor sensing or actuating the environment are instantaneous. Shields are correct-by-construction runtime enforcers that guarantee safe execution by correcting any action that may cause a violation of a formal safety specification. Besides providing safety guarantees, shields should interfere minimally with the agent. Therefore, shields should pick the safe corrective actions in such a way that future interferences are most likely minimized. Current shielding approaches do not consider possible delays in the input signals in their safety analyses. In this paper, we address this issue. We propose synthesis algorithms to compute delay-resilient shields that guarantee safety under worst-case assumptions on the delays of the input signals. We also introduce novel heuristics for deciding between multiple corrective actions, designed to minimize future shield interferences caused by delays. As a further contribution, we present the first integration of shields in a realistic driving simulator. We implemented our delayed shields in the driving simulator Carla. We shield potentially unsafe autonomous driving agents in different safety-critical scenarios and show the effect of delays on the safety analysis.
BibTex:
@article{Cano2023,
title={Safety Shielding under Delayed Observation},
author={Cano Córdoba, Filip and Palmisano, Alexander and Fränzle, Martin and Bloem, Roderick and Könighofer, Bettina},
journal={Proceedings of the International Conference on Automated Planning and Scheduling},
volume={33},
number={1},
pages={80-85},
year={2023}
}
Formal XAI via Syntax-Guided Synthesis
Katrine Bjørner, Samuel Judson, Filip Cano, Drew Goldman, Nick Shoemaker, Ruzica Piskac, Bettina Könighofer.
Bridging the Gap Between AI and Reality (AISoLA) 2023.
Abstract: In this paper, we propose a novel application of syntax-guided synthesis to find symbolic representations of a model’s decision-making process, designed for easy comprehension and validation by humans. Our approach takes input-output samples from complex machine learning models, such as deep neural networks, and automatically derives interpretable mimic programs. A mimic program precisely imitates the behavior of an opaque model over the provided data. We discuss various types of grammars that are well-suited for computing mimic programs for tabular and image input data. Our experiments demonstrate the potential of the proposed method: wesuccessfully synthesized mimic programs for neural networks trained on the MNIST and the Pima Indians diabetes data sets. All experiments were performed using the SMT-based cvc5 synthesis tool.
BibTex:
@inproceedings{DBLP:conf/vecos/BjornerJCGSPK23,
author = {Katrine Bj{\o}rner and
Samuel Judson and
Filip Cano and
Drew Goldman and
Nicholas Shoemaker and
Ruzica Piskac and
Bettina K{\"{o}}nighofer},
title = {Formal {XAI} via Syntax-Guided Synthesis},
booktitle = {AISoLA},
series = {Lecture Notes in Computer Science},
volume = {14380},
pages = {119--137},
publisher = {Springer},
year = {2023}
}
Continuous Engineering for Trustworthy Learning-Enabled Autonomous Systems
Saddek Bensalem, Panagiotis Katsaros, Dejan Ničković, Brian Hsuan-Cheng Liao, Ricardo Ruiz Nolasco, Mohamed Abd El Salam Ahmed, Tewodros A. Beyene, Filip Cano, Antoine Delacourt, Hasan Esen, Alexandru Forrai, Weicheng He, Xiaowei Huang, Nikolaos Kekatos, Bettina Könighofer, Michael Paulitsch, Doron Peled, Matthieu Ponchant, Lev Sorokin, Son Tong, Changshun Wu
Bridging the Gap Between AI and Reality (AISoLA) 2023.
Abstract: Learning-enabled autonomous systems (LEAS) use machine learning (ML) components for essential functions of autonomous operation, such as perception and control. LEAS are often safety-critical. The development and integration of trustworthy ML components present new challenges that extend beyond the boundaries of system’s design to the system’s operation in its real environment. This paper introduces the methodology and tools developed within the frame of the FOCETA European project towards the continuous engineering of trustworthy LEAS. Continuous engineering includes iterations between two alternating phases, namely: (i) design and virtual testing, and (ii) deployment and operation. Phase (i) encompasses the design of trustworthy ML components and the system’s validation with respect to formal specifications of its requirements via modeling and simulation. An integral part of both the simulation-based testing and the operation of LEAS is the monitoring and enforcement of safety, security and performance properties and the acquisition of information for the system’s operation in its environment. Finally, we show how the FOCETA approach has been applied to realistic continuous engineering workflowsfor three different LEAS from automotive and medical application domains.
BibTex:
@inproceedings{DBLP:conf/vecos/BensalemKNLNABCDEFHHKKPPPSTW23,
author = {Saddek Bensalem and
Panagiotis Katsaros and
Dejan Nickovic and
Brian Hsuan{-}Cheng Liao and
Ricardo Ruiz Nolasco and
Mohamed Abd El Salam Ahmed and
Tewodros A. Beyene and
Filip Cano and
Antoine Delacourt and
Hasan Esen and
Alexandru Forrai and
Weicheng He and
Xiaowei Huang and
Nikolaos Kekatos and
Bettina K{\"{o}}nighofer and
Michael Paulitsch and
Doron Peled and
Matthieu Ponchant and
Lev Sorokin and
Son Tong and
Changshun Wu},
title = {Continuous Engineering for Trustworthy Learning-Enabled Autonomous
Systems},
booktitle = {AISoLA},
series = {Lecture Notes in Computer Science},
volume = {14380},
pages = {256--278},
publisher = {Springer},
year = {2023}
}
2022
Search-Based Testing of Reinforcement Learning
Martin Tappler, Filip Cano Córdoba, Bernhard K. Aichernig, Bettina Könighofer.
International Joint Conference of Artificial Intelligence (IJCAI) 2022.
Abstract: Evaluation of deep reinforcement learning (RL) is inherently challenging. Especially the opaqueness of learned policies and the stochastic nature of both agents and environments make testing the behavior of deep RL agents difficult. We present a search-based testing framework that enables a wide range of novel analysis capabilities for evaluating the safety and performance of deep RL agents. For safety testing, our framework utilizes a search algorithm that searches for a reference trace that solves the RL task. The backtracking states of the search, called boundary states, pose safety-critical situations. We create safety test-suites that evaluate how well the RL agent escapes safety-critical situations near these boundary states. For robust performance testing, we create a diverse set of traces via fuzz testing. These fuzz traces are used to bring the agent into a wide variety of potentially unknown states from which the average performance of the agent is compared to the average performance of the fuzz traces. We apply our search-based testing approach on RL for Nintendo's Super Mario Bros.
BibTex:
@inproceedings{ijcai2022p0072,
title = {Search-Based Testing of Reinforcement Learning},
author = {Tappler, Martin and Cano Córdoba, Filip and Aichernig, Bernhard K. and Könighofer, Bettina},
booktitle = {Proceedings of the Thirty-First International Joint Conference on
Artificial Intelligence, {IJCAI-22}},
publisher = {International Joint Conferences on Artificial Intelligence Organization},
editor = {Lud De Raedt},
pages = {503--510},
year = {2022},
month = {7},
note = {Main Track},
doi = {10.24963/ijcai.2022/72},
url = {https://doi.org/10.24963/ijcai.2022/72},
}
2019
An Introduction to Polytope Theory through Ehrhart's Theorem
Filip Cano Córdoba Master Thesis, 2019.
Abstract: A classic introduction to polytope theory is presented, serving as the foundation to develop more advanced theoretical tools, namely the algebra of polyhedra and the use of valuations. The main theoretical objective is the construction of the so called Berline-Vergne valuation. Most of the theoretical development is aimed towards this goal. A little survey on Ehrhart positivity is presented, as well as some calculations that lead to conjecture that generalized permutohedra have positive coefficients in their Ehrhart polynomials. Throughout the thesis three different proofs of Ehrhart's theorem are presented, as an application of the new techniques developed.
BibTex:
@mastersthesis{cano2019introduction,
title={An Introduction to Polytope Theory through Ehrhart's Theorem},
author={Cano C{\'o}rdoba, Filip},
type={M.S. thesis},
year={2019},
school={Universitat Polit{\`e}cnica de Catalunya}
}
2018
Theoretical study of artificial neural networks
Filip Cano Córdoba Bachelor Thesis, 2018.
Abstract: The basic structure and definitions of artificial neural networks are exposed, as an introduction to Machine Learning algorithms. The theoretical description is emphasized and representation power of both shallow and deep networks is studied, proving the so called \textit{Universality Theorem}. Then the properties and limitations of learning algorithms are studied. More specifically, the \textit{No Free Lunch Theorem} is presented and proven, and then some recent approaches to the open problem of convergence of Stochastic Gradient Descent applied to neural networks are presented. Finally, a concept of forgetting in neural networks is introduced and some results on this model are given throughout the thesis.
BibTex:
@mastersthesis{cano2018theoretical,
title={Theoretical study of artificial neural networks},
author={Cano C{\'o}rdoba, Felipe},
type={B.S. thesis},
year={2018},
school={Universitat Polit{\`e}cnica de Catalunya}
}