**On Bisimulation and Model-Checking for Concurrent Systems with Partial Order Semantics**

**Abstract**
In concurrency theory---the branch of (theoretical) computer science that studies the logical and mathematical foundations of parallel computation---there are two main formal ways of modelling the behaviour of systems where multiple actions or events can happen independently and at the same time: either with

On the one hand, the interleaving semantics approach proposes to reduce concurrency to the nondeterministic, sequential computation of the events the system can perform independently. On the other hand, partial order semantics represent concurrency explicitly by means of an independence relation on the set of events that the system can execute in parallel; following this approach, the so-called `true concurrency' approach, independence or concurrency is a

Using interleaving or partial order semantics is, however, more than a matter of taste. In fact, choosing one kind of semantics over the other can have important implications---both from theoretical and practical viewpoints---as making such a choice can raise different issues, some of which we investigate here. More specifically, this thesis studies concurrent systems with partial order semantics and focuses on their

Some results of this work are: a number of

In particular, we show that in all cases the logic games for bisimulation and model-checking developed in this thesis are

Since the mu-calculi and (infinite) logic games studied here

This thesis appears in the Edinburgh Research Archive (ERA). LFCS, School of Informatics, University of Edinburgh (PDF , ERA online version)