# Analyzing and Debugging Normative Requirements via Satisfiability Checking

arXiv: https://arxiv.org/abs/2401.05673 · HTML: https://mlsanity.com/paper/2401.05673/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Jan 2024.

## Built on by (most cited first, 5 of 5)

- [RobEthiChor: Automated Context-aware Ethics-based Negotiation for Autonomous Robots](https://mlsanity.com/paper/2507.22664/) (2025)
- [Fuzzy Representation of Norms](https://mlsanity.com/paper/2601.04249/) (2026)
- [Do You Understand How I Feel?: Towards Verified Empathy in Therapy Chatbots](https://mlsanity.com/paper/2601.08477/) (2026)
- [Social, Legal, Ethical, Empathetic and Cultural Norm Operationalisation for AI Agents](https://mlsanity.com/paper/2603.11864/) (2026)
- [Regret Dominates Surprise: Design-Time Requirements Engineering for Agentic-AI Safety](https://mlsanity.com/paper/2609.05692/) (2026)

## Abstract (arXiv)

As software systems increasingly interact with humans in application domains such as transportation and healthcare, they raise concerns related to the social, legal, ethical, empathetic, and cultural (SLEEC) norms and values of their stakeholders. Normative non-functional requirements (N-NFRs) are used to capture these concerns by setting SLEEC-relevant boundaries for system behavior. Since N-NFRs need to be specified by multiple stakeholders with widely different, non-technical expertise (ethicists, lawyers, regulators, end users, etc.), N-NFR elicitation is very challenging. To address this challenge, we introduce N-Check, a novel tool-supported formal approach to N-NFR analysis and debugging. N-Check employs satisfiability checking to identify a broad spectrum of N-NFR well-formedness issues (WFI), such as conflicts, redundancy, restrictiveness, insufficiency, yielding diagnostics which pinpoint their causes in a user-friendly way that enables non-technical stakeholders to understand and fix them. We show the effectiveness and usability of our approach through nine case studies in which teams of ethicists, lawyers, philosophers, psychologists, safety analysts, and engineers used N-Check to analyse and debug 233 N-NFRs comprising 62 issues for the software underpinning the operation of systems ranging from assistive-care robots and tree-disease detection drones to manufacturing collaborative robots.