Integrating trace logic and Petri nets specifications