We introduce Bifurcation Logic, BL, which combines a basic classical modality with separating conjunction * together with its naturally associated multiplicative implication, that is defined using the modal ordering. Specifically, a formula A*B is true at a world w if and only if each of A,B holds at worlds that are each above w, on separate branches of the order, and have no common upper bound. We provide a labelled tableaux calculus for BL and establish soundness and completeness relative to its relational semantics. The standard finite model property fails for BL. However, we show that, in the absence of multiplicative implication, but in the presence of *, every model has an equivalent finite representation and that this is sufficient to obtain decidability. We illustrate the use of BL through an example of modelling multi-agent access control that is quite generic in its form, suggesting many applications.

翻译：我们引入了分叉逻辑（Bifurcation Logic，BL），该逻辑将经典基本模态与分离合取*及其通过模态序关系自然定义的相关乘性蕴涵相结合。具体而言，公式A*B在世界w中为真，当且仅当A和B分别在序关系中高于w、位于不同分支且无公共上界的世界中成立。我们为BL提出了一种带标签的表列演算，并基于其关系语义证明了可靠性与完备性。BL不具备标准的有穷模型性质。然而，我们证明在缺少乘性蕴涵但保留*的情况下，每个模型都存在等价的有穷表示，且这足以获得可判定性。我们通过一个形式较为通用的多智能体访问控制建模示例，展示了BL的应用潜力，表明其具有广泛的应用前景。