In computer-implemented methods to validate process models, the models carry semantic information that is related to the process steps, including pre-conditions that indicate whether a step would be executable under certain conditions and post-conditions relating to results from executing a step. Steps are related as predecessor/successor so that a post-condition of the predecessor step can be the pre-condition of a successor step. During model validation, variables are exchanged and propagated between the step conditions. Instead of validating the model for potentially all initial values of variables and conditions, the system identifies portions of the model that can be validated separately for a reduced set of initial states.