Time-dependent formalisms have been extensively studied due to increasing demands on the reliability and safety of embedded software systems. Timed automata and various time-extensions of Petri nets are among the most studied time-dependent formalisms. Over the years, significant effort has been devoted to establishing formal relationships between different formalisms. In this respect, many translations between different formalisms have been proposed. Usually, the goal is to establish some equivalence (e.g. bisimulation) between the original system and the translated system, or show that the translation preserves some logic.

In this thesis, we study formal verification, specifically model checking, of Timed-Arc Petri Nets (TAPN), a time extension of Petri nets in which tokens are assigned a real number indicating its age and arcs from place to transitions are guarded by time intervals restricting which tokens can be used to fire a transition. We extend the basic TAPN model with transport arcs, inhibitor arcs and invariants. Further, we prove that invariants alone make the coverability and boundedness problems undecidable.

In respect to model checking, formal queries are expressed in the Timed Computation Tree Logic (TCTL), which is a popular temporal branching-time logic. Much of the work on TCTL, however, do not handle maximal runs in all details. We treat the semantics of TCTL in its full generality, taking into account finite maximal runs that appear in the presence of deadlocks and invariants (strict and non-strict).

We identify a class of translations that preserve TCTL and propose a framework for proving correctness of translations with respect to TCTL formulae. We achieve this via a one-by-many correspondence. Intuitively, when systems A and B are related by a one-by-many correspondence, we can simulate one step in A by a number of steps in B. If we can establish such a relation between the states of A and B, then that will allow us to conclude that the translation from A to B preserves the full TCTL (or only the safety fragment depending on the requirements fulfilled by the relation). Our framework works at the level of timed transition systems, making it independent of the modeling formalisms used.
Since our framework handles TCTL in its full generality, as used in state-of-the-art verification tools such as UPPAAL (www.uppaal.com),
it is directly applicable to tool developers. We give examples of translations from the literature that fit our framework and argue that there are also translations which do not fit our framework.

To illustrate the applicability of our framework, we develop two novel translations from TAPN to networks of timed automata. Using our framework, we prove that both of them preserves the full TCTL. Our translations are motivated by the recent work on the verification tool TAPAAL, where a translation was developed that could only handle liveness properties on a subclass of TAPN models where all transitions have two incoming and two outgoing arcs. To the best of our knowledge, our translations are the first efficient translations to preserve the full TCTL for arbitrary bounded TAPN models. Experiments show that the translations are rather efficient in practice.

We also add integer variables to the extended TAPN model. This allows tokens to carry an integer value which can be used in time intervals on the arcs and time invariants on places. Moreover, we introduce value guards and value invariants in the model. We sketch how to extend our translations to handle integers and conclude that the correctness of the translations still apply.

We have implemented our translations as well as support for inhibitor arcs and integers in a prototype of the verification tool TAPAAL (www.tapaal.net), as well as a number of improvements.