Research

The group Algorithmics focuses on the Algorithm Engineering of Combinatorial Optimization problems. Algorithm Engineering deals with the development and implementation of algorithms for problems appearing in interdisciplinary projects. Thus, the projects require the theoretical development of algorithms and their practical implementation. The studied issues mostly come from the field of Combinatorial Optimization.

 

Real Time Scheduling

Real-time systems are systems that interact with their environment in such a way that for certain inputs the corresponding outputs have to occur within given time bounds. Many embedded systems, in particular those in safety critical applications, are of this type.The practical importance of this class of systems has led to a large body of research on the specification, verification and analysis of real-time systems. We develop distribution and scheduling techniques taking the constraints of distributed computer architectures into account, in particular the combination of caches and pipelines.

Verification of Hybrid Systems

Many embedded systems operate within or even comprise coupled networks of both discrete and continuous components. The behavior of such hybrid discrete-continuous systems cannot be fully understood without explicitly modeling the interaction of discrete and continuous dynamics.Tools for building such models and for simulating their dynamics are commercially available. Simulation is, however, inherently incomplete and has to be complemented by verification, which amounts to showing that the coupled dynamics of the embedded system and its environment is well-behaved, e.g. that it may never reach an undesirable state or that it will converge to a desirable state, regardless of the actual disturbance. Unfortunately, theories and tool support for verifying hybrid systems are not yet mature. Recent industrial trials, e.g. performed by Ford in the context of the Mobies initiative, indicate that current verification tools fall short with respect to both the dimensionality of the continuous state spaces and the size of the discrete state spaces they can handle. Breakthrough in both directions, thereby reconciling the seemingly contradictory demands placed by these dimensions with respect to fully symbolic representations facilitating symbolic model checking, is thus needed.

Dense Subgraphs and Steiner Tree Problems

Graphs are frequently used to model problems that arise in chip design, bioinformatics, social network analysis, and other areas of research. We develop algorithms to identify dense regions in a graph, often with connectivity or cardinality restrictions. An application which is easy to grasp is a social network where persons can be friends with each other. One might be interested in finding a group of at most k persons (cardinality restriction) where every person knows all others at least indirectly, i.e. through a sequence of friends (connectivity). The total number of friendships among the selected persons should be as high as possible (maximization objective).

Some problems, such as the densest subgraph problem, can be solved in polynomial time, e.g. with flow algorithms. Certain restrictions make the problem NP-hard. We employ mixed integer linear programming (MILP) with cutting planes and dynamic programming on tree decompositions for these problems, as well as heuristics and preprocessing steps to improve practicability.

http://www.avacs.org/fileadmin/templates/multiflex4/img/avacslogo.big.gif
AVACS - Automatic Verification And Analysis of Complex Systems