One of the most intricate problem in the synthesis of realtime systems is the scheduling. This paper presents a formal modeling methodology based on time Petri nets (TPN) and a framework for application-specific scheduler synthesis. Finding a feasible scheduling is not an easy task because this problem, in its general form, is NP-hard. The method proposed in this paper finds a scheduling, whether one exists, using state space exploration. The problem with this approach is the space size, which can be very large for medium to large systems. This paper shows how to minimize this problem using behavior restrictions at system modeling, and a partial-order reduction method. Additionally, the algorithm proposed for .nding a feasible schedule uses a depth-first search based method. Therefore, states are only generated if strictly necessary. It is verified through real-world experimental results that a schedule is found examining a reduced number of states .