Mogens Nielsen

TCS Journal 2014 Journal Article

Trust in event structures

• Mogens Nielsen

A tribute to Glynn Winskel on his 60th birthday, including some notes on the role of Winskel's event structures in computational trust.

TCS Journal 2012 Journal Article

Transfer of trust in event-based reputation systems

• Mogens Nielsen
• Karl Krukow

In the Global Computing scenario, trust-based systems have been proposed and studied as an alternative to traditional security mechanisms. A promising line of research concerns the so-called reputation-based computational trust. The approach here is that trust in a computing agent is defined in terms of evidence of future behaviour based on interactions in the past with its environment. We have previously argued how concepts and models from concurrency theory can answer some fundamental challenges in the representation of such interaction behaviour over time, using event structures as our choice of model from concurrency theory. In this paper, we continue this line of research, addressing the problem on how to transfer trust from one behavioural context to another. Our proposed frameworks build on morphisms between event structures, and we prove some generic results guaranteeing formal properties of transfers in the frameworks.

TCS Journal 2005 Journal Article

Introduction—Combined TCSA/TCSB issue—mathematical foundations of computer science 2000

• Mogens Nielsen
• Branislav Rovan

I&C Journal 2003 Journal Article

Undecidability of domino games and hhp-bisimilarity

• Marcin Jurdziński
• Mogens Nielsen
• Jiřı́ Srba

History preserving bisimilarity (hp-bisimilarity) and hereditary history preserving bisimilarity (hhp-bisimilarity) are behavioural equivalences taking into account causal relationships between events of concurrent systems. Their prominent feature is that they are preserved under action refinement, an operation important for the top-down design of concurrent systems. It is shown that, in contrast to hp-bisimilarity, checking hhp-bisimilarity for finite labelled asynchronous transition systems is undecidable, by a reduction from the halting problem of 2-counter machines. To make the proof more transparent a novel intermediate problem of checking domino bisimilarity for origin constrained tiling systems is introduced and shown undecidable. It is also shown that the unlabelled domino bisimilarity problem is undecidable, which implies undecidability of hhp-bisimilarity for unlabelled finite asynchronous systems. Moreover, it is argued that the undecidability of hhp-bisimilarity holds for finite elementary net systems and 1-safe Petri nets.

TCS Journal 1998 Journal Article

Open maps, behavioural equivalences, and congruences 1

• Allan Cheng
• Mogens Nielsen

Spans of open maps have been proposed by Joyal, Nielsen, and Winskel as a way of adjoining an abstract equivalence, ℘-bisimilarity, to a category of models of computation Ms, where ℘ is an arbitrary subcategory of observations. Part of the motivation was to recast and generalise Milner's well-known strong bisimulation in this categorical setting. An issue left open was the congruence properties of ℘-bisimilarity. We address the following fundamental question: given a category of models of computation Ms and a category of observations ℘, are there any conditions under which algebraic constructs viewed as functors preserve ℘-bisimilarity? We define the notion of functors being ℘ factorisable, show how this ensures that ℘-bisimilarity is a congruence with respect to such functors. Guided by the definition of ℘-factorisability we show how it is possible to parametrise proofs of functors being ℘-factorisable with respect to the category of observations ℘, i. e. , with respect to a behavioural equivalence.

MFCS Conference 1998 Invited Paper

Reasoning About the Past

• Mogens Nielsen

Abstract In this extended abstract, we briefly recall the abstract (categorical) notion of bisimulation from open morphisms, as introduced by Joyal, Nielsen and Winskel. The approach is applicable across a wide range of models of computation, and any such bisimulation comes automatically with characteristic logics and games, which in their general formulations treat the future and the past (of computations) on an equal footing. This raises a number of questions concerning properties of such logics and games for concrete well known models from concurrency theory, in particular questions on the power of reasoning about the past.

MFCS Conference 1998 Conference Paper

Timed Bisimulation and Open Maps

• Thomas Hune
• Mogens Nielsen

Abstract Open maps have been used for defining bisimulations for a range of models, but none of these have modelled real-time. We define a category of timed transition systems, and use the general framework of open maps to obtain a notion of bisimulation. We show this to be equivalent to the standard notion of timed bisimulation. Thus the abstract results from the theory of open maps apply, e. g. the existence of canonical models and characteristic logics. Here, we provide an alternative proof of decidability of bisimulation for finite timed transition systems in terms of open maps, and illustrate the use of open maps in presenting bisimulations.

I&C Journal 1996 Journal Article

Bisimulation from Open Maps

• André Joyal
• Mogens Nielsen
• Glynn Winskel

An abstract definition of bisimulation is presented. It makes possible a uniform definition of bisimulation across a range of different models for parallel computation presented as categories. As examples, transition systems, synchronisation trees, transition systems with independence (an abstraction from Petri nets), and labelled event structures are considered. On transition systems the abstract definition readily specialises to Milner's strong bisimulation. On event structures it explains and leads to a strengthening of the history-preserving bisimulation of Rabinovitch and Traktenbrot and van Glabeek and Goltz. A tie-up with open maps in a (pre)topos, as they appear in the work of Joyal and Moerdijk, brings to light a new model, presheaves on categories of pomsets, into which the usual category of labelled event structures embeds fully and faithfully. As an indication of its promise, this new presheaf model has “refinement” operators. The general approach yields a logic, generalising Hennessy–Milner logic, which is characteristic for the generalised notion of bisimulation.

TCS Journal 1996 Journal Article

Foreword

• Peter D. Mosses
• Mogens Nielsen
• Michael I. Schwartzbach

TCS Journal 1996 Journal Article

Models for concurrency: towards a classification

• Vladimiro Sassone
• Mogens Nielsen
• Glynn Winskel

Models for concurrency can be classified with respect to three relevant parameters: behaviour/ system, interleaving/noninterleaving, linear/branching time. When modelling a process, a choice concerning such parameters corresponds to choosing the level of abstraction of the resulting semantics. In this paper, we move a step towards a classification of models for concurrency based on the parameters above. Formally, we choose a representative of any of the eight classes of models obtained by varying the three parameters, and we study the formal relationships between them using the language of category theory.

TCS Journal 1996 Journal Article

Petri nets and bisimulation

• Mogens Nielsen
• Glynn Winskel

Several categorical relationships (adjunctions) between models for concurrency have been established, allowing the translation of concepts and properties from one model to another. A central example is a coreflection between Petri nets and asynchronous transition systems. The purpose of the present paper is to illustrate the use of such relationships by transferring to Petri nets a general concept of bisimulation.

MFCS Conference 1993 Conference Paper

Deterministic Behavioural Models for Concurrency

• Vladimiro Sassone
• Mogens Nielsen
• Glynn Winskel

Abstract This paper offers three candidates for a deterministic, noninterleaving, behaviour model which generalizes Hoare traces to the noninterleaving situation. The three models are all proved equivalent in the rather strong sense of being equivalent as categories. The models are: deterministic labelled event structures, generalized trace languages in which the independence relation is context-dependent, and deterministic languages of pomsets.

MFCS Conference 1991 Invited Paper

Models for Concurrency

• Mogens Nielsen

TCS Journal 1981 Journal Article

Petri nets, event structures and domains, part I

• Mogens Nielsen
• Gordon Plotkin
• Glynn Winskel

The general aim of this paper is to find a theory of concurrency combining the approaches of Petri and Scott (and others). In part I we introduce our formalisms. To connect the abstract ideas of events and domains of information, we show how casual nets induce certain kinds of domains where the information points are certain sets of events. This allows translations between the languages of net theory and domain theory. Following the idea that events of causal nets are occurrences, we generalise causal nets to occurrence nets, by adding forwards conflict. Just as infinite flow charts unfold finite ones, so transition nets can be unfolded into occurrence nets. Next we extend the above connections between nets and domains to these new nets. Event structures which are intermediate between nets and domains play an important part in all our work. Finally, as an example of how concepts translate from one formalism to the other, we show how Petri's notion of confusion ties up with Kahn and Plotkin's concrete domains. In part II we shall continue the job of connecting up notions within net theory and the theory of domains. In particular, we shall examine the idea of states of computations.