-
Concurrency Models with Causality and Events as Psi-calculi
Authors:
Håkon Normann,
Cristian Prisacariu,
Thomas Hildebrandt
Abstract:
Psi-calculi are a parametric framework for nominal calculi, where standard calculi are found as instances, like the pi-calculus, or the cryptographic spi-calculus and applied-pi. Psi-calculi have an interleaving operational semantics, with a strong foundation on the theory of nominal sets and process algebras. Much of the expressive power of psi-calculi comes from their logical part, i.e., asserti…
▽ More
Psi-calculi are a parametric framework for nominal calculi, where standard calculi are found as instances, like the pi-calculus, or the cryptographic spi-calculus and applied-pi. Psi-calculi have an interleaving operational semantics, with a strong foundation on the theory of nominal sets and process algebras. Much of the expressive power of psi-calculi comes from their logical part, i.e., assertions, conditions, and entailment, which are left quite open thus accommodating a wide range of logics. We are interested in how this expressiveness can deal with event-based models of concurrency. We thus take the popular prime event structures model and give an encoding into an instance of psi-calculi. We also take the recent and expressive model of Dynamic Condition Response Graphs (in which event structures are strictly included) and give an encoding into another corresponding instance of psi-calculi. The encodings that we achieve look rather natural and intuitive. Additional results about these encodings give us more confidence in their correctness.
△ Less
Submitted 27 October, 2014;
originally announced October 2014.
-
Extensions of Configuration Structures
Authors:
Cristian Prisacariu
Abstract:
The present paper defines ST-structures (and an extension of these, called STC-structures). The main purpose is to provide concrete relationships between highly expressive concurrency models coming from two different schools of thought: the higher dimensional automata, a \textit{state-based} approach of Pratt and van Glabbeek; and the configuration structures and (in)pure event structures, an \tex…
▽ More
The present paper defines ST-structures (and an extension of these, called STC-structures). The main purpose is to provide concrete relationships between highly expressive concurrency models coming from two different schools of thought: the higher dimensional automata, a \textit{state-based} approach of Pratt and van Glabbeek; and the configuration structures and (in)pure event structures, an \textit{event-based} approach of van Glabbeek and Plotkin. In this respect we make comparative studies of the expressive power of ST-structures relative to the above models. Moreover, standard notions from other concurrency models are defined for ST(C)-structures, like steps and paths, bisimilarities, and action refinement, and related results are given. These investigations of ST(C)-structures are intended to provide a better understanding of the \textit{state-event duality} described by Pratt, and also of the (a)cyclic structures of higher dimensional automata.
△ Less
Submitted 3 June, 2014;
originally announced June 2014.
-
Higher Dimensional Modal Logic
Authors:
Cristian Prisacariu
Abstract:
Higher dimensional automata (HDA) are a model of concurrency that can express most of the traditional partial order models like Mazurkiewicz traces, pomsets, event structures, or Petri nets. Modal logics, interpreted over Kripke structures, are the logics for reasoning about sequential behavior and interleaved concurrency. Modal logic is a well behaved subset of first-order logic; many variants of…
▽ More
Higher dimensional automata (HDA) are a model of concurrency that can express most of the traditional partial order models like Mazurkiewicz traces, pomsets, event structures, or Petri nets. Modal logics, interpreted over Kripke structures, are the logics for reasoning about sequential behavior and interleaved concurrency. Modal logic is a well behaved subset of first-order logic; many variants of modal logic are decidable. However, there are no modal-like logics for the more expressive HDA models. In this paper we introduce and investigate a modal logic over HDAs which incorporates two modalities for reasoning about "during" and "after". We prove that this general higher dimensional modal logic (HDML) is decidable and we define an axiomatic system for it. We also show how, when the HDA model is restricted to Kripke structures, a syntactic restriction of HDML becomes the standard modal logic. Then we isolate the class of HDAs that encode Mazurkiewicz traces and show how HDML, with natural definitions of corresponding Until operators, can be restricted to LTrL (the linear time temporal logic over Mazurkiewicz traces) or the branching time ISTL. We also study the expressiveness of the basic HDML language wrt. bisimulations and conclude that HDML captures the split-bisimulation.
△ Less
Submitted 16 May, 2014;
originally announced May 2014.
-
Actor Network Procedures as Psi-calculi for Security Ceremonies
Authors:
Cristian Prisacariu
Abstract:
The actor network procedures of Pavlovic and Meadows are a recent graphical formalism developed for describing security ceremonies and for reasoning about their security properties. The present work studies the relations of the actor network procedures (ANP) to the recent psi-calculi framework. Psi-calculi is a parametric formalism where calculi like spi- or applied-pi are found as instances. Psi…
▽ More
The actor network procedures of Pavlovic and Meadows are a recent graphical formalism developed for describing security ceremonies and for reasoning about their security properties. The present work studies the relations of the actor network procedures (ANP) to the recent psi-calculi framework. Psi-calculi is a parametric formalism where calculi like spi- or applied-pi are found as instances. Psi-calculi are operational and largely non-graphical, but have strong foundation based on the theory of nominal sets and process algebras. One purpose of the present work is to give a semantics to ANP through psi-calculi. Another aim was to give a graphical language for a psi-calculus instance for security ceremonies. At the same time, this work provides more insight into the details of the ANPs formalization and the graphical representation.
△ Less
Submitted 7 April, 2014;
originally announced April 2014.
-
The Glory of the Past and Geometrical Concurrency
Authors:
Cristian Prisacariu
Abstract:
This paper contributes to the general understanding of the geometrical model of concurrency that was named higher dimensional automata (HDAs) by Pratt. In particular we investigate modal logics for such models and their expressive power in terms of the bisimulation that can be captured. The geometric model of concurrency is interesting from two main reasons: its generality and expressiveness, and…
▽ More
This paper contributes to the general understanding of the geometrical model of concurrency that was named higher dimensional automata (HDAs) by Pratt. In particular we investigate modal logics for such models and their expressive power in terms of the bisimulation that can be captured. The geometric model of concurrency is interesting from two main reasons: its generality and expressiveness, and the natural way in which autoconcurrency and action refinement are captured. Logics for this model, though, are not well investigated, where a simple, yet adequate, modal logic over HDAs was only recently introduced. As this modal logic, with two existential modalities, during and after, captures only split bisimulation, which is rather low in the spectrum of van Glabbeek and Vaandrager, the immediate question was what small extension of this logic could capture the more fine-grained hereditary history preserving bisimulation (hh)? In response, the work in this paper provides several insights. One is the fact that the geometrical aspect of HDAs makes it possible to use for capturing the hh-bisimulation, a standard modal logic that does not employ event variables, opposed to the two logics (over less expressive models) that we compare with. The logic that we investigate here uses standard past modalities and extends the previously introduced logic (called HDML) that had only forward, action-labelled, modalities. Besides, we try to understand better the above issues by introducing a related model that we call ST-configuration structures, which extend the configuration structures of van Glabbeek and Plotkin. We relate this model to HDAs, and redefine and prove the earlier results in the light of this new model. These offer a different view on why the past modalities and geometrical concurrency capture the hereditary history preserving bisimulation. Additional correlating insights are also gained.
△ Less
Submitted 14 June, 2012;
originally announced June 2012.
