Modeling and Verification of Distributed Systems using Markov Decision Processes