Advances in verification of time Petri nets and timed automata. A temporal logic approach. (Q2493434)

This monograph presents a comprehensive introduction to timed automata and timed Petri nets. It presents some of the existing methods of translating time Petri nets into timed automata and focuses on translations that associate clocks to various net components. Both timed and untimed temporal specification languages are introduced and model abstraction methods based on both state classes of timed Petri nets and partition refinement of timed automata are discussed. The book also presents two model checking methods, one based on exploiting abstract state spaces and the other which applies SAT-based symbolic techniques.