The Compositional Method and Regular Reachability

The compositional method, introduced by Feferman and Vaught in 1959, allows to reduce the model-checking problem for a product structure to the model-checking problem for its factors. It applies to first-order logic, and limitations for its use have recently been revealed by Rabinovich (2007). We sharpen the results of Rabinovich by showing that the composition method is applicable to the asynchronous product (and the finitely synchronized product) for an extended modal logic in which the reachability modality is enhanced by a (semi-linear) condition on path lengths. We show that a slight extension leads to the failure of the composition theorem. We add comments on extensions of the result and open questions.