Solving the Decision Problem of Group Achievement Stit Logics with Refref Equivalence
摘要
In the paper, we consider the decision problem of two group achievement stit logics: the super-additive group achievement stit logic and the additive group achievement stit logic, both with refref equivalence. They are the sets of formulas that are valid on two distinct classes of branching time and agent choice structures with instants, respectively. In one class, all structures are super-additive, and in the other class, all structures are additive. Moreover, neither of these structures contains busy choice sequences. We establish the decidability of the super-additive group achievement stit logic with refref equivalence, whereas the additive group achievement stit logic with refref equivalence is shown to be undecidable whenever the number of agents exceeds 2. As additional results, we obtain an alternative but more straightforward semantics for the group achievement stit logics and an embedding of the group Chellas stit logics into the group achievement stit logics with refref equivalence.