### Higher-Order (Non-)Modularity

Claus Appel, Vincent Van Oostrom & Jakob Grue Simonsen
We show that, contrary to the situation in first-order term rewriting, almost none of the usual properties of rewriting are modular for higher-order rewriting, irrespective of the higher-order rewriting format. We show that for the particular format of simply typed applicative term rewriting systems modularity of confluence, normalization, and termination can be recovered by imposing suitable linearity constraints.

### Treewidth Reduction for Constrained Separation and Bipartization Problems

Dániel Marx, Barry O'Sullivan & Igor Razgon
We present a method for reducing the treewidth of a graph while preserving all the minimal $s-t$ separators. This technique turns out to be very useful for establishing the fixed-parameter tractability of constrained separation and bipartization problems. To demonstrate the power of this technique, we prove the fixed-parameter tractability of a number of well-known separation and bipartization problems with various additional restrictions (e.g., the vertices being removed from the graph form an independent set). These...

### Fast equivalence-checking for normed context-free processes

Wojciech Czerwinski & Slawomir Lasota
Bisimulation equivalence is decidable in polynomial time over normed graphs generated by a context-free grammar. We present a new algorithm, working in time $O(n^5)$, thus improving the previously known complexity $O(n^8 * polylog(n))$. It also improves the previously known complexity $O(n^6 * polylog(n))$ of the equality problem for simple grammars.

### Using Abstraction in Modular Verification of Synchronous Adaptive Systems

Ina Schaefer & Arnd Poetzsch-Heffter
Self-adaptive embedded systems autonomously adapt to changing environment conditions to improve their functionality and to increase their dependability by downgrading functionality in case of fail- ures. However, adaptation behaviour of embedded systems significantly complicates system design and poses new challenges for guaranteeing system correctness, in particular vital in the automotive domain. Formal verification as applied in safety-critical applications must therefore be able to address not only temporal and functional properties, but also dynamic adaptation according...

Fabio Mogavero, Aniello Murano & Moshe Y. Vardi
In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between open entities and express that the system is correct no matter how the environment behaves. An important contribution in this context is given by modal logics for strategic ability, in the setting of multi-agent games, such as ATL, ATL*, and the like. Recently, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, which we denote here by SL-CHP,...

### Optimizing mkbTT

Sarah Winkler, Haruhiko Sato, Aart Middeldorp & Masahito Kurihara
We describe performance enhancements that have been added to mkbTT, a modern completion tool combining multi-completion with the use of termination tools.

### Real Computation with Least Discrete Advice: A Complexity Theory of Nonuniform Computability

Martin Ziegler
It is folklore particularly in numerical and computer sciences that, instead of solving some general problem $f:A\to B$, additional structural information about the input $x\in A$ (that is any kind of promise that $x$ belongs to a certain subset $A'\subseteq A$) should be taken advantage of. Some examples from real number computation show that such discrete advice can even make the difference between computability and uncomputability. We turn this into a both topological and combinatorial...

### Beyond omega-Regular Languages

Mikolaj Bojanczyk
The paper presents some automata and logics on $\omega$-words, which capture all $\omega$-regular languages, and yet still have good closure and decidability properties.

### One size does not fit all - how to approach intrusion detection in wireless sensor networks

Andriy Stetsko & Václav Matyá
A wireless sensor network (WSN) is a highly distributed network of resource constrained and wireless devices called sensor nodes. In the work we consider intrusion detection systems as they are proper mechanisms to defend internal attacks on WSNs. A wide diversity of WSN applications on one side and limited resources on other side implies that "one-fit-all" intrusion detection system is not optimal. We present a conceptual proposal for a suite of tools that enable an...

### WCET 2008 Abstracts Collection -- 8th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis

Raimund Kirner
The workshop on Worst-Case Execution Time Analysis is a satellite event to the annual Euromicro Conference on Real-Time Systems. It brings together people that are interested in all aspects of timing analysis for real-time systems. In the 2008 edition, 13 papers were presented, organized into four sessions: methods for WCET computation, low-level analysis, system-level analysis and flow-analysis. The workshop was also the opportunity to report from the 2007 WCET tool challenge.

### Computer-based decision support for railway traffic scheduling and dispatching: A review of models and algorithms

Johanna Törnquist
This paper provides an overview of the research in railway scheduling and dispatching. A distinction is made between tactical scheduling, operational scheduling and re-scheduling. Tactical scheduling refers to master scheduling, whereas operational scheduling concerns scheduling at a later stage. Re-scheduling focuses on the re-planning of an existing timetable when deviations from it have occurred. 48 approaches published between 1973 and 2005 have been reviewed according to a framework that classifies them with respect to problem...

### A Dichotomy Theorem for the General Minimum Cost Homomorphism Problem

Rustem Takhanov
In the constraint satisfaction problem ($CSP$), the aim is to find an assignment of values to a set of variables subject to specified constraints. In the minimum cost homomorphism problem ($MinHom$), one is additionally given weights $c_{va}$ for every variable $v$ and value $a$, and the aim is to find an assignment $f$ to the variables that minimizes $\sum_{v} c_{vf(v)}$. Let $MinHom\left( \Gamma \right)$ denote the $MinHom$ problem parameterized by the set of predicates allowed...

### 07. Solving Large Scale Crew Scheduling Problems by using Iterative Partitioning

Erwin Abbink, Joel Van't Wout & Dennis Huisman
This paper deals with large-scale crew scheduling problems arising at the Dutch railway operator, Netherlands Railways (NS). We discuss several methods to partition large instances into several smaller ones. These smaller instances are then solved with the commercially available crew scheduling algorithm TURNI. In this paper, we compare several partitioning methods with each other. Moreover, we report some results where we applied different partitioning methods after each other. With this approach, we were able to...

### Safe measurement-based WCET estimation

Jean-François Deverge & Isabelle Puaut
This paper explores the issues to be addressed to provide safe worst-case execution time (WCET) estimation methods based on measurements. We suggest to use structural testing for the exhaustive exploration of paths in a program. Since test data generation is in general too complex to be used in practice for most real-size programs, we propose to generate test data for program segments only, using program clustering. Moreover, to be able to combine execution time of...

### Traffic Signal Optimization Using Cyclically Expanded Networks

Ekkehard Köhler & Martin Strehler
Traditionally, the coordination of multiple traffic signals and the traffic assignment problem in an urban street network are considered as two separate optimization problems. However, it is easy to see that the traffic assignment has an influence on the optimal signal coordination and, vice versa, a change in the signal coordination changes the optimal traffic assignment. In this paper we present a cyclically time-expanded network and a corresponding mixed integer linear programming formulation for simultaneously...

### A Privacy-Aware Protocol for Sociometric Questionnaires

Marián Novotný
In the paper we design a protocol for sociometric questionnaires, which serves the privacy of responders. We propose a representation of a sociogram by a weighted digraph and interpret individual and collective phenomena of sociometry in terms of graph theory. We discuss security requirements for a privacy-aware protocol for sociometric questionnaires. In the scheme we use additively homomorphic public key cryptosystem, which allows single multiplication. We present the threshold version of the public key system...

### WCET Analysis for Preemptive Scheduling

Sebastian Altmeyer & Gernot Gebhard
Hard real-time systems induce strict constraints on the timing of the task set. Validation of these timing constraints is thus a major challenge during the design of such a system. Whereas the derivation of timing guarantees must already be considered complex if tasks are running to completion, it gets even more complex if tasks are scheduled preemptively -- especially due to caches, deployed to improve the average performance. In this paper we propose a new...

### Inductive Logic Programming as Abductive Search

Domenico Corapi, Alessandra Russo & Emil Lupu
We present a novel approach to non-monotonic ILP and its implementation called TAL (Top-directed Abductive Learning). TAL overcomes some of the completeness problems of ILP systems based on Inverse Entailment and is the first top-down ILP system that allows background theories and hypotheses to be normal logic programs. The approach relies on mapping an ILP problem into an equivalent ALP one. This enables the use of established ALP proof procedures and the specification of richer...

### On the Complexity of the Interlace Polynomial

Markus Bläser & Christian Hoffmann
We consider the two-variable interlace polynomial introduced by Arratia, Bollob`as and Sorkin (2004). We develop two graph transformations which allow us to derive point-to-point reductions for the interlace polynomial. Exploiting these reductions we obtain new results concerning the computational complexity of evaluating the interlace polynomial at a fixed point. Regarding exact evaluation, we prove that the interlace polynomial is #P-hard to evaluate at every point of the plane, except at one line, where it is...

### AMS Without 4-Wise Independence on Product Domains

Vladimir Braverman, Kai-Min Chung, Zhenming Liu, Michael Mitzenmacher & Rafail Ostrovsky
In their seminal work, Alon, Matias, and Szegedy introduced several sketching techniques, including showing that $4$-wise independence is sufficient to obtain good approximations of the second frequency moment. In this work, we show that their sketching technique can be extended to product domains $[n]^k$ by using the product of $4$-wise independent functions on $[n]$. Our work extends that of Indyk and McGregor, who showed the result for $k = 2$. Their primary motivation was the...

### Weighted Dynamic Pushdown Networks

Alexander Wenner
We develop a generic framework for the analysis of programs with recursive procedures and dynamic process creation. To this end we combine the approach of weighted pushdown systems (WPDS) with the model of dynamic pushdown networks (DPN). Weighted dynamic pushdown networks (WDPN) describe processes running in parallel. Each process may perform pushdown actions and spawn new processes. Transitions are labelled by weights to carry additional information. We derive a method to determine meet-over-all-paths values for...

### Subsumer: A Prolog theta-subsumption engine

Jose Santos & Stephen Muggleton
State-of-the-art theta-subsumption engines like Django (C) and Resumer2 (Java) are implemented in imperative languages. Since theta-subsumption is inherently a logic problem, in this paper we explore how to efficiently implement it in Prolog. theta-subsumption is an important problem in computational logic and particularly relevant to the Inductive Logic Programming (ILP) community as it is at the core of the hypotheses coverage test which is often the bottleneck of an ILP system. Also, since most of...

### Proving Productivity in Infinite Data Structures

Hans Zantema & Matthias Raffelsieper
For a general class of infinite data structures including streams, binary trees, and the combination of finite and infinite lists, we investigate the notion of productivity. This generalizes stream productivity. We develop a general technique to prove productivity based on proving context-sensitive termination, by which the power of present termination tools can be exploited. In order to treat cases where the approach does not apply directly, we develop transformations extending the power of the basic...

### WCET 2008 -- Report from the Tool Challenge 2008 -- 8th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis

Niklas Holsti, Jan Gustafsson, Guillem Bernat, Clément Ballabriga, Armelle Bonenfant, Roman Bourgade, Hugues Cassé, Daniel Cordes, Albrecht Kadlec, Raimund Kirner, Jens Knoop, Paul Lokuciejewski, Nicholas Merriam, Marianne De Michiel, Adrian Prantl, Bernhard Rieder, Christine Rochange, Pascal Sainrat & Markus Schordan
Following the successful WCET Tool Challenge in 2006, the second event in this series was organized in 2008, again with support from the ARTIST2 Network of Excellence. The WCET Tool Challenge 2008 (WCC'08) provides benchmark programs and poses a number of "analysis problems" about the dynamic, run-time properties of these programs. The participants are challenged to solve these problems with their program analysis tools. Two kinds of problems are defined: WCET problems, which ask for...

### ATMOS 2005 Abstracts Collection -- Selected Papers from the 5th Workshop on Algorithmic Methods and Models for Optimization of Railways

Leo G. Kroon & Rolf H. Möhring
This issue contains six papers that were presented in preliminary form at the 5th Workshop on Algorithmic Methods and Models for Optimization of Railways (ATMOS 2005), held at Palma de Mallorca, Spain, October 7, 2005 in conjunction with ALGO 2005. These papers are representative of several areas of research within the scope of ATMOS: rolling stock circulation and engine assignment, station location, line planning, railway traffic scheduling and dispatching, transfer optimization within network design, and...

• 2010
453

• Text
453

• Dagstuhl
453