Bisimulation and Logical Preservation for Continuous-Time Markov Decision
Processes
Martin Neuhäußer, Joost-Pieter Katoen
AIB 2007-10
This paper introduces strong bisimulation for continuous-time Markov
decision processes (CTMDPs), a stochastic model which allows for a
nondeterministic choice between exponential distributions, and shows that
bisimulation preserves the validity of CSL. To that end, we interpret the
semantics of CSL - a stochastic variant of CTL for continuous-time Markov
chains - on CTMDPs and show its measure-theoretic soundness. The main
challenge faced in this paper is the proof of logical preservation that
is substantially based on measure theory.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Temporal assertions for sequential and current programs
Volker Stolz
AIB 2007-15
In this thesis, we present an extension to the well-known concept of
assertions: temporal assertions allow the specification and validation of
modal safety properties of an application at runtime. We see this as a
necessary step in enforcing the growing number of implicit requirements
of software specifications, which are often only informally defined in
the documentation of application program interfaces (API) and are beyond
the reach of type checkers, compilers, or model checkers.
Also, we show how our techniques can be applied to existing programs
without modifying the source code. Although, like assertions, our
approach cannot prove the absence of errors, it gives the programmer
a more powerful means of automatically checking assumptions about his
program at runtime.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Adaptive Channel Assignment to Support QoS and Load Balancing for Wireless
Mesh Networks
Sadeq Ali Makram, Mesut Güneç, Martin Wenig, Alexander Zimmermann
AIB 2007-16
One of the most promising wireless technologies are Wireless Mesh
Networks (WMN). The aggregate capacity of wireless mesh networks
can be improved significantly be equipping each node with several
Wireless Network Interfaces (WNICs) and by using multiple channels in
order to minimize the interference and to provide high performance in
such networks. To achieve these benefits it requires a good channel
assignment planning. The channels have to be assigned in such a way,
that interference is decreased and performance is increased at the same
time. Since the number of available channels is limited, it is desired
to allocate and reallocate channels dynamically on-demand.
In this paper, a dynamic channel assignment, is proposed to the
aforementioned problem which is adaptive to the load in the wireless
mesh network. The algorithm add or select a channel for those heavy
loaded nodes, based on the local informations of the neighbor nodes.
The selected or the added channel that minimizes the interference and
insure the network connectivity. The simulation results show that our
algorithm improve the network capacity by approximately 50% in comparison
to a static channel assignment.