Edinburgh Research Archive >
Informatics, School of >
Informatics thesis and dissertation collection >
Please use this identifier to cite or link to this item:
|Title: ||On bisimulation and model-checking for concurrent systems with partial order semantics|
|Authors: ||Gutierrez, Julian|
|Supervisor(s): ||Bradfield, Julian|
|Issue Date: ||30-Jun-2011|
|Publisher: ||The University of Edinburgh|
|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 interleaving or with partial order semantics.
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
primitive notion rather than a derived concept as in the interleaving framework.
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 bisimulation and model-checking problems;
the theories and techniques herein apply, in a uniform way, to different classes of Petri nets,
event structures, and transition system with independence (TSI) models.
Some results of this work are: a number of mu-calculi (in this case, fixpoint extensions of
modal logic) that, in certain classes of systems, induce exactly the same identifications as some
of the standard bisimulation equivalences used in concurrency. Secondly, the introduction of
(infinite) higher-order logic games for bisimulation and for model-checking, where the players
of the games are given (local) monadic second-order power on the sets of elements they are
allowed to play. And, finally, the formalization of a new order-theoretic concurrent game
model that provides a uniform approach to bisimulation and model-checking and bridges some
mathematical concepts in order theory with the more operational world of games.
In particular, we show that in all cases the logic games for bisimulation and model-checking
developed in this thesis are sound and complete, and therefore, also determined—even when
considering models of infinite state systems; moreover, these logic games are decidable in the
finite case and underpin novel decision procedures for systems verification.
Since the mu-calculi and (infinite) logic games studied here generalise well-known fixpoint
modal logics as well as game-theoretic decision procedures for analysing concurrent systems
with interleaving semantics, this thesis provides some of the groundwork for the design of a
logic-based, game-theoretic framework for studying, in a uniform manner, several concurrent
systems regardless of whether they have an interleaving or a partial order semantics.|
|Sponsor(s): ||Engineering and Physical Sciences Research Council (EPSRC)|
Overseas Research Studentship (ORS) Award
School of Informatics PhD Scholarship of the University of Edinburgh
|Keywords: ||mathematical logic|
fixpoint modal logics
|Appears in Collections:||Informatics thesis and dissertation collection|
Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.