An Adaptive Storage Manager for XML Documents
Effective and efficient management and manipulation of XML documents requires stable decisions at the time a document enters the XML DBMS to provide for storage structures which are adjusted to the document characteristics and which reflect the future processing needs. While some of the critical parameters require a kind of pre-specification, others can be determined by pre-analysis or sampling of the incoming document or by just making experience-driven “educated guesses”. Important parameters are related to node labeling, path synopsis, document container layout, and indexing. In this paper, we discuss approaches to achieve an adaptive behavior of the storage manager to provide tailor-made native XML storage structures to the extent possible.

title: Autonomes Index Tuning - DBMS-integrierte Verwaltung von Soft Indexen
abstract: Das Self Management in DBMS, und das Self Tuning als wichtiger Teil davon, gewinnt auf Grund der wachsenden Komplexitat von Systemen und Anwendungen und den daraus resultierenden steigenden Betriebskosten zunehmend an Beachtung. Der Stand der Technik bezuglich des Index Tunings sind AdministrationsTools, die aus einem gegebenen Workload eine empfohlene Indexkonfiguration ableiten. Diese muss jedoch bei Anderungen des Systems, dessen Umgebung oder der Zugriffsmuster wiederholt angepasst werden. Wir stellen in diesem Beitrag einen dynamischen Ansatz zum Index Tuning vor, der zur Laufzeit das Systemverhalten und die -nutzung uberwacht, Entscheidungen bezuglich moglicher Verbesserungen der aktuellen Indexkonfiguration trifft und diese integriert mit der Anfrageverarbeitung umsetzt. Fur den zuletzt genannten Aspekt fuhren wir mit IndexBuildScan und SwitchPlan neue Operatoren zur Erzeugung von Indexen wahrend der Bearbeitung einer Anfrage sowie deren sofortiger Nutzung ein. Die Beschreibung der Implementierung der vorgestellten Konzepte als Erweiterung des PostgreSQL-Systems, sowie eine Evaluierung an Hand eines von TPC-H abgeleiteten Benchmarks beschliesen den Beitrag.

title: How to calculate symmetries of Petri nets
abstract: Symmetric net structure yields symmetric net behaviour. Thus, knowing the symmetries of a net, redundant calculations can be skipped. We present a framework for the calculation of symmetries for several net classes including place/transition nets, timed nets, stochastic nets, self–modifying nets, nets with inhibitor arcs, and many others. Our approach allows the specification of different symmetry groups. Additionally it provides facilities either to calculate symmetries on demand while running the actual analysis algorithm, or to calculate them in advance. For the latter case we define and calculate a ground set of symmetries. Such a set has polynomial size and is sufficient for an efficient implementation of the for all symmetries loop and the partition of net elements into equivalence classes. These two constructions are the usual way to integrate symmetries into an analysis algorithm.

title: Integrating Low Level Symmetries into Reachability Analysis
abstract: We present three methods for the integration of symmetries into reachability analysis. Two of them lead to maximal reduction but their runtime depends on the symmetry structure. The third one works always fast but does not always yield maximal reduction.

title: Using Petri net invariants in state space construction
abstract: The linear algebraic invariant calculus is a powerful technique for the verification of Petri nets. Traditionally it is used for structural verification, i.e. for avoiding the explicit construction of a state space. In this paper, we study the use of Petri net invariants for reducing the memory resources required during state space construction. While place invariants help to reduce the amount of memory needed for each single state (without reducing the number of states as such), transition invariants can be used to reduce the number of states to be stored. Interestingly, our approach does not require computing invariants in full, let alone storing them permanently. All information we need can be deduced from an upper triangular form of the Petri net's incidence matrix. Experiments prove that the place invariant technique leads to improvements in both memory and run time costs while transition invariants lead to a space/time tradeoff that can be controlled heuristically.

title: Model-Checking with Coverability Graphs
abstract: We show that several formulas of a temporal logic can be verified using the coverability graph of the underlying system. Of course, the procedure is not capable of verifying all formulae, since already the reachability problem for (unbounded) Petri nets is computationally hard. Thus, the procedure returns true, false, or unknown for a query. The formulae that can be verified cover most of the well known standard properties which have been listed in the context of coverability graph analysis so far.

title: Automated generation of a progress measure for the sweep-line method
abstract: In the context of Petri nets, we propose an automated construction of a progress measure which is an important pre-requisite for a state space reduction technique called the sweep-line method. Our construction is based on linear-algebraic techniques concerning the transition vectors of the Petri net under consideration. We further discuss the possible combination of the sweep-line method with other state space reduction techniques (partial order reduction, the symmetry method).