The following technical report is available from
http://aib.informatik.rwth-aachen.de:
On Compositional Failure Detection in Structured Transition Systems
Ingo Felscher, Wolfgang Thomas
AIB 2011-12
In model-checking, systems are often given as products. We propose an
approach that is built on a preprocessing of specifications in terms
of appropriate automata. This allows to incorporate information about
the local behaviour and synchronization of the system components into
the specification. We develop a framework of (partially) synchronized
automaton products and a format of corresponding specification
automata that allows for a compositional failure detection of linear
regular properties (either for finite or for infinite behaviour). As
a result we obtain an algorithm which separates the local and the
non-local segments of system runs, resulting in improved complexity
bounds in typical specifications.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Introducing Timers to pi-Calculus
Kamal Barakat
AIB 2011-18
Modeling systems of concurrent processes can be improved if the
concept of time is represented in the model. Pi-calculus is a
suitable process algebra for modeling communicating processes
that exchange messages and is able to model mobility through
dynamic channel setup and through privatizing names using
restriction. Therefore, it is beneficial to extend pi-calculus
to embrace the notion of time.
