Specification and Analysis of Ethical Requirements in Autonomous Systems using Abstract State Machines

Abstract

Autonomous systems are increasingly required to comply with ethical norms and human values, motivating the need for rigorous methods to specify and analyze ethical requirements. Social, Legal, Ethical, Empathetic, and Cultural (SLEEC) rules provide a structured means to encode such requirements; however, ensuring their correctness and well-formedness calls for formal specification and systematic, tool-supported analysis. This paper presents an approach based on Abstract State Machines (ASMs) and the ASMETA tool set for the formal specification and well-formedness analysis of SLEEC requirements. We formally define the semantics of the SLEEC domain-specific language, enabling systematic validation of SLEEC models through conflicts and redundancies detection. Moreover, we extend the core when–then–unless structure of a SLEEC rule with response delays and with a clause unless–until to support the temporary suspension of a rule. The validated ASMETA-based SLEEC model is directly executable and can be readily adopted as a runtime model to support the subsequent phase, namely the operationalization of ethical requirements in autonomous systems

@inproceedings{ScandurraSFIMP26,
  author       = {Patrizia Scandurra and
                  Martina {De Sanctis} and
                  Gianluca Filippone and
                  Paola Inverardi and
                  Raffaela Mirandola and
                  Sara Pettinari},
  title        = {Specification and Analysis of Ethical Requirements in Autonomous Systems
                  Using Abstract State Machines},
  booktitle    = {Rigorous State-Based Methods - 12th International Conference, {ABZ}
                  2026, Tokyo, Japan, May 18-20, 2026, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {16579},
  pages        = {145--164},
  publisher    = {Springer},
  year         = {2026},
  doi          = {10.1007/978-3-032-26752-8\_9},
}