Matching observed behavior and modeled behavior: An approach based on Petri nets and integer programming