Over the past decade BitTorrent has established itself as the virtual standard for P2P file sharing in the Internet. However, it is currently not possible to investigate BitTorrent with ns-3 due to the unavailability of an according application model. In this paper we eliminate this burden. We present a highly modular BitTorrent model which allows for the easy simulation of different BitTorrent systems such as file sharing as well as present and future BitTorrent-based Video-on-Demand systems.

Formal verification using the model checking paradigm has to deal with two aspects: The system models are structured, often as products of components, and the specification logic has to be expressive enough to allow the formalization of reachability properties. The present paper is a study on what can be achieved for infinite transition systems under these premises. As models we consider products of infinite transition systems with different synchronization constraints. We introduce finitely synchronized transition systems, i.e. product systems which contain only finitely many (parameterized) synchronized transitions, and show that the decidability of FO(R), first-order logic extended by reachability predicates, of the product system can be reduced to the decidability of FO(R) of the components. This result is optimal in the following sense: (1) If we allow semifinite synchronization, i.e. just in one component infinitely many transitions are synchronized, the FO(R)-theory of the product system is in general undecidable. (2) We cannot extend the expressive power of the logic under consideration. Already a weak extension of firstorder logic with transitive closure, where we restrict the transitive closure operators to arity one and nesting depth two, is undecidable for an asynchronous (and hence finitely synchronized) product, namely for the infinite grid.

The extension of formal verification methods to infinite models requires classes of graphs which are finitely representable and for which the model checking problem is decidable. We consider three approaches to define classes of finitely representable graphs: internal representations as configuration graphs of higher-order pushdown systems, transformational representations by application of operations which preserve the decidability of the model checking problem, and by composition from components using synchronized products.

We prove an existential version of Gaifman's locality theorem and show how it can be applied algorithmically to evaluate existential first-order sentences in finite structures.

Formal verification using the model-checking paradigm has to deal with two aspects. The systems models are structured, often as products of components, and the specification logic has to be expressive enough to allow the formalization of reachability properties. The present paper is a study on what can be achieved for infinite transition systems under these premises. As models we consider products of infinite transition systems with different synchronization constraints. We introduce finitely synchronized transition systems, i.e. product systems which contain only finitely many synchronized transitions, and show that the decidability of FO(R), first-order logic extended by reachability predicates, of the product system can be reduced to the decidability of FO(R) of the components in a Feferman-Vaught like style. This result is optimal in the following sense. (1) If we allow semifinite synchronization, i.e. just in one component infinitely many transitions are synchronized, the FO(R)-theory of the product system is in general undecidable. (2) We cannot extend the expressive power of the logic under consideration. Already a weak extension of first-order logic with transitive closure, where we restrict the transitive closure operators to arity one and nesting depth two, is undecidable for an asynchronous (and hence finitely synchronized) product, namely for the infinite grid.

Languages of infinite two-dimensional words (infinite omega-pictures) are studied in the automata theoretic setting of tiling systems. We show that a hierarchy of acceptance conditions as known from the theory of omega-languages can be established also over pictures. Since the usual pumping arguments fail, new proof techniques are necessary. Finally, we show that (unlike the case of omega-languages) none of the considered acceptance conditions leads to a class of infinitary picture languages which is closed under complementation.

In this paper we give two equivalent characterizations of the Caucal hierarchy, a hierarchy of infinite graphs with a decidable monadic second-order (MSO) theory. It is obtained by iterating the graph transformations of unfolding and inverse rational mapping. The first characterization sticks to this hierarchical approach, replacing the language-theoretic operation of a rational mapping by an MSO-transduction and the unfolding by the treegraph operation. The second characterization is non-iterative. We show that the family of graphs of the Caucal hierarchy coincides with the family of graphs obtained as the epsilon-closure of configuration graphs of higher-order pushdown automata. While the different characterizations of the graph family show their robustness and thus also their importance, the characterization in terms of higher-order pushdown automata additionally yields that the graph hierarchy is indeed strict.

Gaifman's locality theorem (1981) states that every first-order sentence is equivalent to a Boolean combination of sentences saying: There exist elements a₁,...,a_k that are far apart from one another, and each a_i satisfies some local condition described by a first-order formula. We prove that every existential first-order sentence is equivalent to a positive Boolean combination of sentences saying: There exist elements a₁,...,a_k that are far apart from one another, and each a_i satisfies some local condition described by an existential first-order formula. We then show how a variant of this existential locality theorem can be applied to evaluate existential first-order sentences in certain finite structures, such as planar graphs or graphs of bounded degree, improving a result of Frick and Grohe (1999) for the special case of existential sentences.