Objective of the thesis is to describe a modeling formalism for non-zero-sum games with multiple players with reachability objectives, where the game is represented as an oriented graph with complex structure, and solve how Nash equilibria can be found and presented for each game instance. The thesis should explore multiple possibilities both with regards to the expressive power of the games (concurrent games, games with partial observability, prices on transitions), and the range of problems solved for a particular instance (restricting to equilibria satisfying specific properties, finding pareto-optimal set of equilibria, etc.). The thesis should also provide interesting modeling examples to demonstrate results of the method.