  Formal verification using the model checking paradigm has to deal with twoaspects: The system models are structured, often as products of components, andthe specification logic has to be expressive enough to allow the formalizationof reachability properties. The present paper is a study on what can beachieved for infinite transition systems under these premises. As models weconsider products of infinite transition systems with different synchronizationconstraints. We introduce finitely synchronized transition systems, i.e.product systems which contain only finitely many (parameterized) synchronizedtransitions, and show that the decidability of FO(R), first-order logicextended by reachability predicates, of the product system can be reduced tothe decidability of FO(R) of the components. This result is optimal in thefollowing sense: (1) If we allow semifinite synchronization, i.e. just in onecomponent infinitely many transitions are synchronized, the FO(R)-theory of theproduct system is in general undecidable. (2) We cannot extend the expressivepower of the logic under consideration. Already a weak extension of first-orderlogic with transitive closure, where we restrict the transitive closureoperators to arity one and nesting depth two, is undecidable for anasynchronous (and hence finitely synchronized) product, namely for the infinitegrid.
We introduce finitely synchronized transition systems, i.e. product systems which contain only finitely many (parameterized) synchronized transitions, and show that the decidability of FO(R), first-order logic extended by reachability predicates, of the product system can be reduced to the decidability of FO(R) of the components.