Complete partial orders have been used for a long time for defining semantics of programming languages. In the context of concurrency de Bakker and Zucker (1982) proposed a metric setting for handling concurrency, recursion and nontermination, which has proved to be very successful in many applications. Starting with a semantic domain D for ‘finite behaviour’ we investigate the relation between the ideal completion Idl(D) and the metric completion which are both suitable to model recursion and infinite behaviour. We also consider the properties of semantic operators.
Consider a distributed system in which processes exchange information by passing messages. The gossip problem is the following: Whenever a process q receives a message from another process p, q must be able to decide which of p and q has more recent information about r, for every other process r in the system. With this data, q is in a position to update its knowledge about the global state of the system.
The linear time mu-calculus vTL is a language extending standard linear time temporal logic with fixpoint operators. We present a method for deciding whether a given vTZ-formula is satisfiable, and give a direct proof of its completeness. Although simpler than the existing methods, it gives rise to an algorithm working in the same 2O( n 2 log n ) time as these, or alternatively, to a polynomial space, singly exponential time algorithm. What is more important, the method allows us to devise a tableau system to support manual or computer-aided (as opposed to fully automated) satisfiability checking.
The notion of action refinement has been studied intensively in the past few years. It is usually introduced in the form of an operator in a process algebraic language, for which a denotational semantics in a suitable model is then given. In this paper we complement this approach by defining a corresponding operational semantics for refinement, in the form of derivation rules for a transition relation. Because of the (well-known) fact that ordinary transition systems are not expressive enough to capture the effects of refinement, we use an event-based transition system model described elsewhere in the literature. The operational semantics of refinement thus defined is equivalent (in fact event isomorphic) to the usual denotational semantics.
The algebra of A-nets, a high level class of labelled Petri nets introduced in the Petri Box Calculus in order to cope with structured data, is extended with a general refinement operator and, based thereon, a general recursion operator; their properties may directly be derived from the corresponding operators for the low level Petri Boxes.
We present a transformational approach to the design of real-time systems. The starting point are requirements formulated in a subset of Duration Calculus called implementables and the target are program specifications in a language SL that combines regular expressions with action systems and time conditions. While Duration Calculus is state-based, SL is event-based and can be seen as a stepping stone towards a timed OCCam-like programming language. The approach is illustrated by the example of a computer controlled gas burner.
In a previous paper we had defined the notion of an efficiency preorder for concurrent systems. In this paper, we present a coarser relation, called the elaboration preorder, which is finer than observational equivalence. Further, this preorder is incomparable with the almost-weak bisimulation preorder of Sangiorgi and Milner. In particular, the elaboration preorder is preserved under all contexts except summation. The largest precongruence contained in it, which we call conformance, is obtained by the usual means and a complete axiomatization for conformance of finite processes is given. The paper ends with an example to show the use of this relation.
In this paper we address the issue of understanding sequential and parallel composition of agents from a logical viewpoint. In particular we use methods of abstract logic programming in linear logic, i.e. computations are modeled as proof searches in a suitable fragment of linear logic. While parallel composition has a straightforward treatment in this setting, sequential composition is much more difficult to be obtained. We study a case, directly inspired by Mon- teiro’s distributed logic, in which the causality relation among agents forms a series-parallel order; top agents may be recursively rewritten by series-parallel structures of new agents. We show a very declarative and simple treatment of sequentialization, which smoothly integrates with parallelization, by translating our formal system into linear logic in a complete way. This means that we obtain a full two ways correspondence between proofs and computations; thus we have full correspondence between the two formalisms. Our case study is very general per se, but it should be clear that the methodology adopted should be extensible to orderings more general than the series-parallel ones. The expected outcomes of this research are at least twofold: having some new insights in the design of concurrent languages and formalisms and having a strong starting point for relating linear logic semantics to concurrency semantics.
A fundamental problem in debugging and monitoring distributed computations is to detect whether a state of the system satisfies some predicate. Cooper and Marzullo defined this problem as Possibly(Φ).
Using a class of high level Petri nets, M-nets, endowed with composition operators resembling those of CCS, we give the compositional semantics of B(PN)2 - a syntactically simple but semantically powerful concur-rent programming language. We also give an associated low level net semantics and show the consistency of these high and low level semantics, as well as consistency with a previously defined low level semantics of B(PN)2.
identifying, comparing and unifying the control flow principles of present day programming languages L
We study systems of sequential agents which communicate by synchronization, whose behaviours are given by a subclass of event structures. Transition system models for such structures typically require global state information which cannot be obtained by taking products of local transition systems. We offer a presentation whereby the notion of local state is modified, and an appropriate product operation precisely captures this class of behaviours. This is shown using a back-and-forth construction.
We present a new solution of the mutual exclusion problem, which is modelled as a Petri net. In order to present a concise model of the algorithm, we extend Petri nets by the concepts of progress and non-progress transitions and fair arcs.
This paper describes the results of the Esprit Basic Research Working Group 6067 CALIBAN (Causal Calculi Based on Nets).
Mazurkiewicz traces form a model suitable for the investigation of some aspects of concurrency. We want to investigate one of its generalization based on the weakening of the condition that the equivalence relation is a congruence. The (quasi-)prefix ordering is then compared with the configuration graph induced by the partial ordering of symbol occurrences. We point out differences and exhibit necessary and/or sufficient conditions for them to be isomorphic: this is settled with the help of diamond properties.
As part of an effort to give a "truly concurrent" semantics to process algebra, we propose a framework of refinements of the failures model for CSP with concurrency, conflict and causality relations on traces. These relations are defined by induction over syntax of CSP processes. We study in detail two new semantics: the possible concurrency (where two traces are said to be concurrent if they may be observations of the same concurrent run) and the possible conflict (two traces are said to be in conflict if they may be observations of two different runs). The guaranteed concurrency is obtained from the possible conflict semantics. Although the expansion law is necessarily weakened to an inequality, we show that most of the CSP laws are preserved, the exception being the idempotency of choice for the possible conflict refinement. Finally, we show that our semantics is well-founded by demonstrating a strong connection with the existing event structures semantics for CSP. The latter results show that, in a certain sense, concurrency distinctions can be made at the level of syntax, without resorting to reasoning about event occurrences.
New results on structural analysis of well-formedness, that is, structural boundedness and structural liveness, of Place/Transition net systems, based on the rank of the incidence matrix, are introduced and related to previously known ones.
Causality-based partial order semantics allows an easy formulation of weak fairness. It is demonstrated that this is true also for other partial order semantics, namely for partial words and interval semiwords.
Net Theory was introduced in the early sixties by Carl Adam Petri [1] as a form of general system theory based on the notion of concurrency. Net Theory has been widely developed during these years, becoming very popular as a framework for the analysis and specification of concurrent systems. Among the basic notions of the theory, stands the synchronic structure of a system. It characterizes dependencies between sets of its events in terms of a distance measuring their degree of synchronization. In this paper we show that a natural generalization of regions introduced by Ehrenfeucht and Rozenberg exactly corresponds to synchronic distances and that this notion of region can be used to axiomatise a class of transition systems corresponding to bounded place/transition nets without loops.
Linda has just four primitives, all of which are devoted to coordinating the interactions among programs by sharing information maintained in a common data space. To write programs manipulating data, it is necessary to embed Linda in a (functional, imperative, logic, etc.) programming language; this leads to a family of languages based on Linda. We define syntax and semantics for a member of the Linda family, L, that is obtained by embedding Linda in a “simple” sequential language. The semantics of this concurrent programming language is formalized by applying techniques developed within the framework of process algebras. A two-level semantics for L is provided: an operational one in Plotkin’s style, based on a transition system, and an observational one, based on three behavioural preorders, obtained by applying the testing framework to L.
