From ATL to Stit
I present a technical embedding of alternating-time temporal logic into stit theory.
cs.LO↗
arXiv subjects
Aldo Iván Ramírez Abarca
Publications and source records attributed to Aldo Iván Ramírez Abarca.
A Deontic Stit Logic Based on Beliefs and Expected Utility
The formalization of action and obligation using logic languages is a topic of increasing relevance in the field of ethics for AI. Having an expressive syntactic and semantic framework to reason about agents' decisions in moral situations allows for unequivocal representations of components of behavior that are relevant when assigning blame (or praise) of outcomes to said agents. Two very important components of behavior in this respect are belief and belief-based action. In this work we present a logic of doxastic oughts by extending epistemic deontic stit theory with beliefs. On one hand, the semantics for formulas involving belief operators is based on probability measures. On the other, the semantics for doxastic oughts relies on a notion of optimality, and the underlying choice rule is maximization of expected utility. We introduce an axiom system for the resulting logic, and we address its soundness, completeness, and decidability results. These results are significant in the line of research that intends to use proof systems of epistemic, doxastic, and deontic logics to help in the testing of ethical behavior of AI through theorem-proving and model-checking.
cs.LO↗
Stit Semantics for Epistemic Notions Based on Information Disclosure in Interactive Settings
We characterize four types of agentive knowledge using a stit semantics over branching discrete-time structures. These are \emph{ex ante} knowledge, \emph{ex interim} knowledge, \emph{ex post} knowledge, and know-how. The first three are notions that arose from game-theoretical analyses on the stages of information disclosure across the decision making process, and the fourth has gained prominence both in logics of action and in deontic logic as a means to formalize ability. In recent years, logicians in AI have argued that any comprehensive study of responsibility attribution and blameworthiness should include proper treatment of these kinds of knowledge. This paper intends to clarify previous attempts to formalize them in stit logic and to propose alternative interpretations that in our opinion are more akin to the study of responsibility in the stit tradition. The logic we present uses an extension with knowledge operators of the Xstit language, and formulas are evaluated with respect to branching discrete-time models. We also present an axiomatic system for this logic, and address its soundness and completeness.
cs.LO↗
A Logic of Objective and Subjective Oughts (full paper with proofs)
The relation between agentive action, knowledge, and obligation is central to the understanding of responsibility --a main topic in Artificial Intelligence. Based on the view that an appropriate formalization of said relation would contribute to the development of ethical AI, we point out the main characteristics of a logic for objective and subjective oughts that was recently introduced in the literature. This logic extends the traditional stit paradigm with deontic and epistemic operators, and provides a semantics that deals with Horty's puzzles for knowledge and obligation. We provide an axiomatization for this logic, and address its soundness and completeness with respect to a class of relevant models.
math.LO↗