Model checking of time Petri nets using the state class timed automaton
scientific article; zbMATH DE number 5116458