819414
Sort Order Problems in Relational Databases
A relation of degree k can be sorted lexicographically in k! different ways, i.e., according to any one of the possible permutations of the schema of the relation. Such permutations are referred to as sort orders. When evaluating unary and binary relational algebra operators using sort-merge algorithms, sort orders fulfilling the constraints enforced by the operators are chosen for the operand relations. The relations are then sorted according to their assigned sort orders, and the result is obtained by merging. Should the operands already be sorted according to one of the permissible sort orders, then only a merging is required. The sort order of the result will depend on the sort orders of the operands. When evaluating whole relational algebra expressions, the result of one operation will be used as an operand to the next. It is desirable to choose sort orders in such a way that the result of one operation will automatically fulfill the requirements of the next. In general, one would like to find a minimal number of operators in the expression for which this cannot be obtained, bearing in mind the overall goal of minimizing the total work. We show that this problem is NP-hard, and that the corresponding decision problem is NP-complete. However, most simplifications of the original problem give rise to efficient algorithms. In fact, most frequently occurring queries can be analyzed in linear time in the size of the query. This is due to the fact that only a very limited number of subsets of all permutations of schemas can be encountered in the algorithms, which means that compact representations for these subsets can be found.
34233329
Search Trees with Relaxed Balance and Near-Optimal Height
We introduce the relaxed k-tree, a search tree with relaxed balance and a height bound, when in balance, of (1 + Ɛ) log2 n + 1, for any Ɛ > 0. The rebalancing work is amortized O(1/Ɛ) per update. This is the first binary search tree with relaxed balance having a height bound better than c ċ log2 n for a fixed constant c. In all previous proposals, the constant is at least 1/ log2 Φ > 1.44, where Φ is the golden ratio. 
 
As a consequence, we can also define a standard (non-relaxed) k-tree with amortized constant rebalancing per update, which is an improvement over the original definition. 
 
Search engines based on main-memory databases with strongly fluctuating workloads are possible applications for this line of work.
80794
Efficient Rebalancing of Chromatic Search Trees
Chromatic trees were defined by Nurmi and Soisalon-Soininen, as a new type of binary search tree for databases. The aim is to improve runtime performance by allowing a greater degree of concurrency, which, in turn, is obtained by uncoupling updating from rebalancing. This also allows rebalancing to be postponed completely or partially until after peak working hours. The advantages of the proposal of Nurmi and Soisalon-Soininen are quite significant, but there are definite problems with it. First, they give no explicit upper bound on the complexity of their algorithm. Second, some of their rebalancing operations can be applied many more times than necessary. Third, some of their operations, when removing one problem, create another. We define a new set of rebalancing operations which we prove give rise to at most @?log"2(N+1)@?-1 rebalancing operations per insertion and at most @?log"2(N+1)@?-2 rebalancing operations per deletion, where N is the maximum size the tree could ever have, given its initial size and the number of insertions performed. Most of these rebalancing operations, in fact, do no restructuring; they simply move weights around. The number of operations which actually change the structure of the tree is at most one per update.
19914316
Extending the Accommodating Function
The applicability of the accommodating function, a relatively new measure for the quality of on-line algorithms, is extended. If a limited amount n of some resource is available, the accommodating function A(?) is the competitive ratio when input sequences are restricted to those for which the amount ?n of resources suffices for an optimal off-line algorithm. The accommodating function was originally used only for ? ? 1. We focus on ? < 1, observe that the function now appears interesting for a greater variety of problems, and use it to make new distinctions between known algorithms and to find new ones.
6986183
Efficient Simplification of Bisimulation Formulas
The problem of checking or optimally simplifying bisimulation formulas is likely to be computationally very hard. We take a different view at the problem: we set out to define a very fast algorithm, and then see what we can obtain. Sometimes our algorithm can simplify a formula perfectly, sometimes it cannot. However, the algorithm is extremely fast and can, therefore, be added to formula-based bisimulation model checkers at practically no cost. When the formula can be simplified by our algorithm, this can have a dramatic positive effect on the better, but also more time consuming, theorem provers which will finish the job.
30882911
Complexity of Layered Binary Search Trees with Relaxed Balance
When search trees are made relaxed, balance constraints are weakened such that updates can be made without immediate rebalancing. This can lead to a speed-up in some circumstances. However, the weakened balance constraints also make it more challenging to prove complexity results for relaxed structures.In our opinion, one of the simplest and most intuitive presentations of balanced search trees has been given via layered trees. We show that relaxed layered trees are among the best of the relaxed structures. More precisely, rebalancing is worst-case logarithmic and amortized constant per update, and restructuring is worst-case constant per update.
9332520
Compact Data Structures and State-Space Reduction for Model-Checking Real-Time Systems
During the past few years, a number of verification tools have been developed for real-time systems in the framework of timed automata. One of the major problems in applying these tools to industrial-sized systems is the huge memory-usage for the exploration of the state-space of a network (or product) of timed automata, as the model-checkers must keep information about not only the control structure of the automata but also the clock values specified by clock constraints. In this paper, we present a compact data structure for representing clock constraints. The data structure is based on an O(n3) algorithm which, given a constraint system over real-valued variables consisting of bounds on differences, constructs an equivalent system with a minimal number of constraints. In addition, we have developed an on-the-fly reduction technique to minimize the space-usage. Based on static analysis of the control structure of a network of timed automata, we are able to compute a set of symbolic states that cover all the dynamic loops of the network in an on-the-fly searching algorithm, and thus ensure termination in reachability analysis. The two techniques and their combination have been implemented in the tool UPPAAL. Our experimental results demonstrate that the techniques result in truly significant space-reductions: for six examples from the literature, the space saving is between 75% and 94%, and in (nearly) all examples time-performance is improved. Noteworthy is also the observation that the two techniques are completely orthogonal.
8987497
Efficient Timed Reachability Analysis Using Clock Difference Diagrams
One of the major problems in applying automatic verification tools to industrial-size systems is the excessive amount of memory required during the state-space exploration of a model. In the setting of real-time, this problem of state-explosion requires extra attention as information must be kept not only on the discrete control structure but also on the values of continuous clock variables. 
 
In this paper, we exploit Clock Difference Diagrams, CDD's, a BDD-like data-structure for representing and effectively manipulating certain nonconvex subsets of the Euclidean space, notably those encountered during verification of timed automata. 
 
A version of the real-time verification tool Uppaal using CDD's as a compact data-structure for storing explored symbolic states has been implemented. Our experimental results demonstrate significant spacesavings: for eight industrial examples, the savings are in average 42% with moderate increase in runtime. 
 
We further report on how the symbolic state-space exploration itself may be carried out using CDD's.
12303667
Formal Verification of a Power Controller Using the Real-Time Model Checker UPPAAL
A real-time system for power-down control in audio/video components is modeled and verified using the real-time model checker UPPAAL. The system is supposed to reside in an audio/video component and control (read from and write to) links to neighbor audio/video components such as TV, VCR and remote-control. In particular, the system is responsible for the powering up and down of the component in between the arrival of data, and in order to do so in a safe way without loss of data, it is essential that no link interrupts are lost. Hence, a component system is a multitasking system with hard real-time requirements, and we present techniques for modeling time consumption in such a multitasked, prioritized system. The work has been carried out in a collaboration between Aalborg University and the audio/video company B&O. By modeling the system, 3 design errors were identified and corrected, and the following verification confirmed the validity of the design but also revealed the necessity for an upper limit of the interrupt frequency. The resulting design has been implemented and it is going to be incorporated as part of a new product line.
7965507
Reduction and Refinement Strategies for Probabilistic Analysis
We report on new strategies for model checking quantitative reachability properties of Markov decision processes by successive refinements. In our approach, properties are analyzed on abstractions rather than directly on the given model. Such abstractions are expected to be significantly smaller than the original model, and may safely refute or accept the required property. Otherwise, the abstraction is refined and the process repeated. As the numerical analysis involved in settling the validity of the property is more costly than the refinement process, the method profits from applying such numerical analysis on smaller state spaces. The method is significantly enhanced by a number of novel strategies: a strategy for reducing the size of the numerical problems to be analyzed by identification of so-called essential states, and heuristic strategies for guiding the refinement process.
406624
Model Checking Timed Automata with Priorities Using DBM Subtraction
In this paper we describe an extension of timed automata with priorities, and efficient algorithms to compute subtraction on DBMs (difference bounded matrices), needed in symbolic model-checking of timed automata with priorities. The subtraction is one of the few operations on DBMs that result in a non-convex set needing sets of DBMs for representation. Our subtraction algorithms are efficient in the sense that the number of generated DBMs is significantly reduced compared to a naive algorithm. The overhead in time is compensated by the gain from reducing the number of resulting DBMs since this number affects the performance of symbolic model-checking. The uses of the DBM subtraction operation extend beyond timed automata with priorities. It is also useful for allowing guards on transitions with urgent actions, deadlock checking, and timed games.