Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA process algebra based framework for promise theory
252
0
0.0
(
0
)
Added by
Inge Bethke
Publication date
2007
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We present a process algebra based approach to formalize the interactions of computing devices such as the representation of policies and the resolution of conflicts. As an example we specify how promises may be used in coming to an agreement regarding a simple though practical transportation problem.
rate research
Read More
In standard process algebra, parallel components do not share a common state and communicate through synchronisation. The advantage of this type of communication is that it facilitates compositional reasoning. For modelling and analysing systems in which parallel components operate on shared memory, however, the communication-through-synchronisation paradigm is sometimes less convenient. In this paper we study a process algebra with a notion of global variable. We also propose an extension of Hennessy-Milner logic with predicates to test and set the values of the global variables, and prove correspondence results between validity of formulas in the extended logic and stateless bisimilarity and between validity of formulas in the extended logic without the set operator and state-based bisimilarity. We shall also present a translation from the process algebra with global variables to a fragment of mCRL2 that preserves the validity of formulas in the extended Hennessy-Milner logic.
In the case of multi-threading as found in contemporary programming languages, parallel processes are interleaved according to what is known as a process-scheduling policy in the field of operating systems. In a previous paper, we extend ACP with this form of interleaving. In the current paper, we do so with the variant of ACP known as ACP$_epsilon$. The choice of ACP$_epsilon$ stems from the need to cover more process-scheduling policies. We show that a process-scheduling policy supporting mutual exclusion of critical subprocesses is now covered.
This paper extends a standard process algebra with a time-out operator, thereby increasing its absolute expressiveness, while remaining within the realm of untimed process algebra, in the sense that the progress of time is not quantified. Trace and failures equivalence fail to be congruences for this operator; their congruence closure is characterised as failure trace equivalence.
This paper introduces the counterpart of strong bisimilarity for labelled transition systems extended with time-out transitions. It supports this concept through a modal characterisation, congruence results for a standard process algebra with recursion, and a complete axiomatisation.
Meta SOS is a software framework designed to integrate the results from the meta-theory of structural operational semantics (SOS). These results include deriving semantic properties of language constructs just by syntactically analyzing their rule-based definition, as well as automatically deriving sound and ground-complete axiomatizations for languages, when considering a notion of behavioural equivalence. This paper describes the Meta SOS framework by blending aspects from the meta-theory of SOS, details on their implementation in Maude, and running examples.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
