# 2006

## Network Discovery and Verification with Distance Queries

CS-06-002 T. Erlebach, A. Hall, M. Hoffmann & M. Mihaľák.

The network discovery (verification) problem asks for a minimum subset $Q\subseteq V$ of queries in an undirected graph $G=(V,E)$ such that these queries discover all edges and non-edges of the graph. This is motivated by the common approach of combining local measurements in order to obtain maps of the Internet or other dynamically growing networks. In the distance query model, a query at node $q$ returns the distances from $q$ to all other nodes in the graph. We describe how the existence of an individual edge or non-edge in $G$ can be deduced by potentially combining the results of several queries. This leads to a characterization of when a set of queries $Q$ "discovers" the graph $G$. In the on-line network discovery problem, the graph is initially unknown, and the algorithm has to select queries one by one based only on the results of the previous ones. We study the problem using competitive analysis and give a randomized on-line algorithm with competitive ratio $O(\sqrt{n\log n})$ for graphs on~$n$ nodes. We also show lower bounds $\Omega(\sqrt{n})$ and $\Omega(\log n)$ on competitive ratios of deterministic on-line algorithms and randomized on-line algorithms, respectively. In the off-line network verification problem, the graph is known in the beginning and the problem asks for a minimum number of queries to verify all edges and non-edges. We show that the problem is NP-hard and present an $O(\log n)$-approximation algorithm.

Available as: Adobe™ PDF (.pdf)

## Semantic Web Services Composition via Planning as Model Checking

CS-06-003 H. Yu & S. Reiff-Marganiec.

The ability to automatically compose services is one essential aspect of service oriented architecture. It can reduce time and cost in development and maintenance of complex services and software systems. We are developing a technique to realize this aim by combining the "planning as model checking" approach with Semantic Web Service concepts. We have modified a current planning as model checking algorithm by using a bounded on-the-fly depth-first search algorithm. The result allows for service execution plans to be generated on the fly. One of the challenges is to model a web service as a state transition system. The approach will be suitable in the context of ontologies, but for now we are simply using dictionaries for mapping operations and parameters. The planning as model checking approach forms part of a larger framework to automatically compose services, which addresses several drawbacks of current composition approaches.

Available as: Adobe™ PDF (.pdf)

## Variable sized online interval coloring with bandwidth

CS-06-004 L. Epstein, T. Erlebach & A. Levin.

We consider online coloring of intervals with bandwidth in a setting where colors have variable capacities. Whenever the algorithm opens a new color, it must choose the capacity for that color and cannot change it later. The goal is to minimize the total capacity of all the colors used. We consider the bounded model, where all capacities must be chosen in the range (0,1], and the unbounded model, where the algorithm may use colors of any positive capacity. For the absolute competitive ratio, we give an upper bound of 14 and a lower bound of 4.59 for the bounded model, and an upper bound of 4 and a matching lower bound of 4 for the unbounded model. We also consider the offline version of these problems and show that whereas the unbounded model is polynomially solvable, the bounded model is NP-hard in the strong sense and admits a 3.6-approximation algorithm.

Available as: Adobe™ PDF (.pdf)

## Constant-factor approximation for minimum-weight (connected) dominating sets in unit disk graphs

CS-06-008 C. Ambühl, T. Erlebach, M. Mihaľák & M. Nunkesser.

For a given graph with weighted vertices, the goal of the minimum-weight dominating set problem is to compute a vertex subset of smallest weight such that each vertex of the graph is contained in the subset or has a neighbor in the subset. A unit disk graph is a graph in which each vertex corresponds to a unit disk in the plane and two vertices are adjacent if and only if their disks have a non-empty intersection. We present the first constant-factor approximation algorithm for the minimum-weight dominating set problem in unit disk graphs, a problem motivated by applications in wireless ad-hoc networks. The algorithm is obtained in two steps: First, the problem is reduced to the problem of covering a set of points located in a small square using a minimum-weight set of unit disks. Then, a constant-factor approximation algorithm for the latter problem is obtained using enumeration and dynamic programming techniques exploiting the geometry of unit disks. Furthermore, we show how to obtain a constant-factor approximation algorithm for the minimum-weight connected dominating set problem in unit disk graphs.

Our techniques also yield a constant-factor approximation algorithm for the weighted disk cover problem (covering a set of points in the plane with unit disks of minimum total weight) and a 3-approximation algorithm for the weighted forwarding set problem (covering a set of points in the plane with weighted unit disks whose centers are all contained in a given unit disk).

Available as: Adobe™ PDF (.pdf) gzipped PostScript (.ps.gz)

## Towards a Task-Oriented, Policy-Driven Business Requirements Specification for Web Services

CS-06-009 S. Gorton & S Reiff-Marganiec.

Dynamic assembly of complex software is possible through automated composition of web services. Coordination scripts identify and orchestrate a number of services to fulfil a user or business goal. The automated process begins at the business requirement stage, this there exists a need for expressing high level business requirements. Current solutions (such as BPMN and UML) fail to include specifications at the appropriate level of abstraction. Our approach defines a graphical notation to depict a business goal in terms of objectives, which are refined by tasks, where the specifics of each task as well as overarching business constraints are encapsulated in a descriptive way in policies.

Available as: Adobe™ PDF (.pdf)

## Hybrid Adequacy

CS-06-011 Roy L. Crole.

The Hybrid system, implemented within Isabelle-HOL, allows object logics to be represented using higher order abstract syntax (HOAS), and reasoned about using tactical theorem proving in general and principles of (co)induction in particular. The form of HOAS provided by Hybrid is essentially lambda calculus with constants.

In this paper, we present a particular logical framework which can be viewed as a model of Hybrid, and state and prove that the model is representationally adequate for the lambda calculus with constants.

Of fundamental interest is the form of lambda abstractions provided by Hybrid---each abstraction is actually a definition of a de Bruijn expression---and hence the formal system contains a hybrid of named and nameless bound variable notation. In particular the proof of adequacy involves a number of proofs by induction which involve higher order symbolic computations.

Available as: Adobe™ PDF (.pdf)

## Optimization Problems in Communication Networks (Ph.D. Thesis)

CS-06-013 M. Mihaľák.

We study four problems arising in the area of communication networks. The minimum-weight dominating set problem in unit disk graphs asks, for a given set D of weighted unit disks, to find a minimum-weight subset D' of D such that the disks D' intersect all disks in D. The problem is NP-hard and we present the first constant-factor approximation algorithm. Applying our techniques to other geometric graph problems, we can obtain better (or new) approximation algorithms.

The network discovery problem asks for a minimum number of queries that discover all edges and non-edges of an unknown network (graph). A query at node v discovers a certain portion of the network. We study two different query models and show various results concerning the complexity, approximability and lower bounds on competitive ratios of online algorithms.

The OVSF-code assignment problem deals with assigning communication codes (nodes) from a complete binary tree to users. Users ask for codes of a certain depth and the codes have to be assigned such that (i) no assigned code is an ancestor of another assigned code and (ii) the number of (previously) assigned codes that have to be reassigned (in order to satisfy (i)) is minimized. We present hardness results and several algorithms (optimal, approximation, online and fixed-parameter tractable).

The joint base station scheduling problem asks for an assignment of users to base stations (points in the plane) and for an optimal colouring of the resulting conflict graph: user u with its assigned base station b is in conflict with user v, if a disk with center at b, and u on its perimeter, contains v. We study the complexity, and present and analyse optimal, approximation and greedy algorithms for general and various special cases.

Available as: Adobe™ PDF (.pdf)

## Software Reengineering at the Architectural Level: Transformation of Legacy Systems

CS-06-014 R. Correia, C. Matos, M. El-Ramly, R. Heckel, G. Koutsoukos & L. Andrade.

In this paper, we put forward a methodology for reengineering the architecture of a legacy software system. The proposed approach is not restricted to any specific source and target architectures, or programming language. It consists in (1) achieving a representation of the source code through its categorization and structuring, (2) transforming it into the new intended architecture, and (3) generating the code for the target platform. First, the code is categorized according to its purpose by pre-defined rules and represented as a model that is an instance of a type graph. Then, this representation is transformed into the intended target architectural paradigm using graph transformation techniques. The generation of the target code is not covered in this report but will be studied in the near future. The approach attempts to address problems that are repeatedly encountered in legacy reengineering industry projects.

Available as: Adobe™ PDF (.pdf)