Protocols for distributed systems make often use of random transitions to achieve a common goal. A popular example are randomized leader election protocols. We introduce probabilistic product automata (PPA) as a natural model for this kind of systems. To reason about these systems, we propose to use a product version of linear temporal logic (LTL⊗ ). The main result of the paper is a model-checking procedure for PPA and LTL⊗ . With its help, it is possible to check qualitative properties of distributed systems automatically.