A Stable Model Semantics for eFLINT Norm Specifications and Model Checking Scenarios

Since its introduction at GPCE2020, the eFLINT norm specification language has been used in academic and industrial applications to specify and automate compliance for various norms, such as privacy regulations and data processing agreements. The eFLINT interpreter has been used to automate the analysis of real-time or historical cases by computing logical consequences and reporting normative violations. 

To support future language and tooling developments, we contribute a formal definition of the language as a translation to first-order logic programming with stable model semantics. The described semantics aligns with the previous semi-formal descriptions of the language, but resolves issues relating to logical inference with negative antecedent and aggregation operators. Specifically, we formalise the connection between eFLINT's derivation rules and Horn clauses under the stable model semantics. Secondly, by repurposing the Clingo answer-set solver as a highly-optimised eFLINT interpreter, we extend the toolset for eFLINT with model-checking abstract properties in addition to case analysis. 

We evaluate the new semantics and interpreter via an empirical comparison of the existing implementation to our prototype implementation. We observe that the expected subset of our tests have the equivalent behaviours.