Bifurcation Logic: Separation Through Ordering

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 1 * 2 is true at a world w if and only if each i holds at worlds w i 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 - * , 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.