A discrete-time temporal deontic STIT logic based on interpreted systems
Shuge Rong, Yifeng Ding
TL;DR
We address normative reasoning in multiagent settings using a discrete-time STIT language with per-agent deontic operators, formalized as the logic L_DTDS. The framework combines interpreted-systems semantics with a filtration based completeness proof to obtain decidability. The paper introduces general semantic variants, namely super-additive interpreted systems and DTDS Kripke premodels, and shows how to translate these into standard interpreted systems while preserving truth for relevant formulas. This work provides a rigorous foundation for formal legal and normative reasoning in AI and multi-agent systems, enabling robust analysis of persistent duties and dynamic power over time.
Abstract
We present a STIT ('see to it that') logic with discrete temporal operators and deontic operators in which we can formalize and reason about legal concepts such as persistent duty and the dynamic concept of power from Hohfeld. As our main technical contribution, we show that this logic is sound and complete with respect to the semantics based on interpreted systems and is decidable.