Abstract
In a previous paper, we developed an algebraic theory about threads and
a form of concurrency where some deterministic interleaving strategy
determines how threads that exist concurrently are interleaved.
The interleaving of different threads constitutes a multi-thread.
Several multi-threads may exist concurrently on a single host in a
network, several host behaviours may exist concurrently in a single
network on the internet, etc.
In the current paper, we assume that the above-mentioned kind of
interleaving is also present at those other levels.
We extend the theory developed so far with features to cover the
multi-level case.
We employ the resulting theory to develop a simplified, formal
representation schema of the design of systems that consist of several
multi-threaded programs on various hosts in different networks and to
verify a property of all systems designed according to that schema.
View-only version of article
Preprint available here.