2737251
Better Bounds on the Accommodating Ratio for the Seat Reservation Problem
We investigate the problem of giving seat reservations on-line. We assume that a train travels from a start station to an end station, stopping at k stations, including the first and last. Passengers may attempt to make reservations at any point before they get on the train, and reservations can be made going from any station to any later station. All algorithms under consideration must be "fair", i.e., they are not allowed to reject a request for a reservation which could be made at the time. The "accommodating ratio" compares the performance of an on-line algorithm to that of the optimal off-line algorithm, under the assumption that the only sequences of requests allowed are sequences for which the optimal off-line algorithm could accommodate all requests. The train has a fixed number of seats, and we first consider the case in which all tickets have the same cost, and the seat reservation system attempts to maximize income. We prove improved upper bounds on the performance of First-Fit and Best-Fit, showing that in the worst case, neither algorithm does significantly better than any fair deterministic algorithm would. We also improve the upper bounds on the possible performance of any "fair" deterministic or randomized algorithm. A specific randomized algorithm is also considered. Finally, we consider the case in which the cost of a ticket is proportional to the distance traveled.
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.
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.
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.
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.
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.
9243889
Generality in design and compositional verification usingTav
It is a well recognised fact that design errors in parallel systems are often hard to identify—due to their non-deterministic nature. It is therefore important that designs are analysedbefore the implementation phase begins. Even small parallel systems often have an intrinsic structure which is hard to fully understand, and the support of automated tools is therefore indispensable. In order to be of any practical use, the computations of such tools must be (polynomially) effective in terms of the system size, and furthermore it must be possible to reason about the system in terms of the properties of its (parallel) components—in order to avoid state-space explosion. Finally, the well-establishedstepwise refinement design strategy must be supported.The tools of theTav-system fulfil the above requirements, and in this paper we present its features by analysing a simple transmission protocol. The cornerstone of the system is the theory ofmodal transition systems, which allows for efficient decidability, stepwise refinement, and compositionality. The theory also supports a unique feature ofTav, namely the ability to provide explanations in case of design errors.
11147632
Lower and upper bounds in zone-based abstractions of timed automata
Timed automata have an infinite semantics. For verification purposes, one usually uses zone-based abstractions w.r.t. the maximal constants to which clocks of the timed automaton are compared. We show that by distinguishing maximal lower and upper bounds, significantly coarser abstractions can be obtained. We show soundness and completeness of the new abstractions w.r.t. reachability and demonstrate how information about lower and upper bounds can be used to optimise the algorithm for bringing a difference bound matrix into normal form. Finally, we experimentally demonstrate that the new techniques dramatically increase the scalability of the real-time model checker UPPAAL.
39576178
Resource-Efficient Scheduling for Real Time Systems
For embedded systems efficient utilization of resources is an acute problem arising from the increasing computational demands in all sorts of applications. The consumers constantly demand better functionality and flexibility of embedded products which imply an increase in the resources needed for their realization. In several areas – e.g. portable devices such as PDAs, mobile phones and laptops as well as mission critical systems such as space applications – the ability to design resource efficient solutions is crucial.
8766873
Synthesis of Optimal Strategies Using HyTech
Priced timed (game) automata extend timed (game) automata with costs on both locations and transitions. The problem of synthesizing an optimal winning strategy for a priced timed game under some hypotheses has been shown decidable in P. Bouyer, F. Cassez, E. Fleury, and K.G. Larsen. Optimal strategies in priced timed game automata. Research Report BRICS RS-04-4, Denmark, Feb. 2004. Available at http://www.brics.dk/RS/04/4/]. In this paper, we present an algorithm for computing the optimal cost and for synthesizing an optimal strategy in case there exists one. We also describe the implementation of this algorithm with the tool HyTech and present an example.
16545835
UPPAAL Implementation Secrets
In this paper we present the continuous and on-going development of datastructures and algorithms underlying the verification engine of the tool UPPAAL. In particular, we review the datastructures of Difference Bounded Matrices, Minimal Constraint Representation and Clock Difference Diagrams used in symbolic state-space representation and -analysis for real-time systems.In addition we report on distributed versions of the tool, and outline the design and experimental results for new internal datastructures to be used in the next generation of UPPAAL.Finally, we mention work on complementing methods involving acceleration, abstraction and compositionality.