اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدReactive Bisimulation Semantics for a Process Algebra with Time-Outs
264
0
0.0
(
0
)
تأليف
Rob van Glabbeek
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
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.
قيم البحث
اقرأ أيضاً
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 f
ailures equivalence fail to be congruences for this operator; their congruence closure is characterised as failure trace equivalence.
I show that in a standard process algebra extended with time-outs one can correctly model mutual exclusion in such a way that starvation-freedom holds without assuming fairness or justness, even when one makes the problem more challenging by assuming
memory accesses to be atomic. This can be achieved only when dropping the requirement of speed independence.
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 w
hich 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 process algebras such as ACP (Algebra of Communicating Processes), parallel processes are considered to be interleaved in an arbitrary way. In the case of multi-threading as found in contemporary programming languages, parallel processes are actua
lly interleaved according to some interleaving strategy. An interleaving strategy is what is called a process-scheduling policy in the field of operating systems. In many systems, for instance hardware/software systems, we have to do with both parallel processes that may best be considered to be interleaved in an arbitrary way and parallel processes that may best be considered to be interleaved according to some interleaving strategy. Therefore, we extend ACP in this paper with the latter form of interleaving. The established properties of the extension concerned include an elimination property, a conservative extension property, and a unique expansion property.
This paper introduces an imperative process algebra based on ACP (Algebra of Communicating Processes). Like other imperative process algebras, this process algebra deals with processes of the kind that arises from the execution of imperative programs
. It distinguishes itself from already existing imperative process algebras among other things by supporting abstraction from actions that are considered not to be visible. The support of abstraction opens interesting application possibilities of the process algebra. This paper goes briefly into the possibility of information-flow security analysis of the kind that is concerned with the leakage of confidential data. For the presented axiomatization, soundness and semi-completeness results with respect to a notion of branching bisimulation equivalence are established.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
