<p>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.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Solving the Decision Problem of Group Achievement Stit Logics with Refref Equivalence

  • Yan Zhang

摘要

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.