Finite and Circular Path Models for Branching Time Logics

We define various kinds of branching time logic consisting of path quantifiers and second-order (<o-regular) linear time logic which are extensions of CTL * (computation tree logic). These logics are decidable for the computation tree semantics. However, if we adopt the non-tree semantics reflecting the possible computations of a looping program eventually returning to the same state of computation, the picture is quite different, and one of the logics under consideration becomes highly undecidable. Nevertheless, this semantics allows a simpler model definition, including finite models corresponding to a finite state machine (program), and circular path finite models reflecting programs which are really determinis-tic finite state machines, but the model's view does not include all the details of program state. Since circular path finite model may have only countably many possible paths (com-putations), this semantics is much simpler than the usual one based on sets of all infinite paths in computation tree. We show that for the finite models the circular path semantics is equivalent to the usual one, i.e. that for a finite structure a formula is true in the model of all the possible paths if and only if it is true in the model of all the circular paths. 1