Markov Decision Processes (MDPs) serve as a foundational framework for decision-making under uncertainty, widely applied in model checking and reinforcement learning (RL). This study investigates the integration of Deep Q-Learning (DQL) into model checking for MDPs, with a focus on evaluating various state and action space encoding methods. Traditional Q-learning approaches rely on Q-tables to store state-action values, but as model complexity increases, storing these values becomes impractical. Deep Q-Learning addresses this by leveraging a neural network to approximate Q-values, enabling scalability to large state and action spaces. This paper explores the effects of different state encoding techniques, such as one-hot and ordinal encoding, on the learning efficiency and accuracy of the model checker. Additionally, the impact of using Double Q-Learning, which separates target and policy networks, is examined for improved stability and convergence. The findings provide insights into applying DQL to formal verification and optimization, extending the scope of reinforcement learning in model checking beyond traditional domains.