16. A method comprising: detecting, by a first processor, at least one complexity in a model including executable semantics, the at least one complexity interfering with a verification of the model; identifying a source for the at least one complexity, the source including a temporal operation in the model, the temporal operation being between an update to an input of an element of the model and an update to an output of the element of the model; reducing the source for the at least one complexity, by the first or a second processor, the reducing including: abstracting the temporal operation; and performing verification of the model.
17. The method of claim 16 wherein the abstracting the temporal operation includes: generating an updated model, the updated model based on the model; and including a stub input configured to trigger the update to the output of the element at an unspecified time.