Two-Variable Logic with Counting and Trees

We consider the two-variable logic with counting quantifiers (C-2) interpreted over finite structures that contain two forests of ranked trees. This logic is strictly more expressive than standard C-2 and it is no longer a fragment of first-order logic. In particular, it can express that a structure is a ranked tree, a cycle, or a connected graph of bounded degree. It is also strictly more expressive than first-order logic with two variables and two successor relations of two finite linear orders. We present a decision procedure for the satisfiability problem for this logic. The procedure runs in NEXPTTME, which is optimal since the satisfiability problem for plain C-2 is NEXPTARE-complete.