Timed Catalytic Petri Nets

We consider catalytic membrane systems (CatMS) and catalytic Petri nets (CatPN). We add discrete timers to these classes, and prove that the timed formalisms (tCatMS and tCatPN) can be expressed by their untimed versions if finite timers are used. We establish formal links between these formalisms, and characterize some subclasses in which various properties are decidable and can be analyzed using CPN Tools, i.e., a software tool for editing, simulating, and analyzing colored Petri nets.