Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userOn the Decidability of Behavioral Equivalences for (P,P)-PRS
77
0
0.0
(
0
)
Added by
Irina Lomazova
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Authors
Irina Lomazova
Ask ChatGPT about the research
No Arabic abstract
We study resource similarity and resource bisimilarity -- congruent restrictions of the bisimulation equivalence for the (P,P)-class of Process Rewrite Systems (PRS). Both these equivalences coincide with the bisimulation equivalence for (1,P)-subclass of (P,P)-PRS, which is known to be decidable. While it has been shown in the literature that resource similarity is undecidable for (P,P)-PRS, decidability of resource bisimilarity for (P,P)-PRS remained an open question. In this paper, we present an algorithm for checking resource bisimilarity for (P,P)-PRS. We show that although both resource similarity and resource bisimilarity are congruences and have a finite semi-linear basis, only the latter is decidable.
rate research
Read More
We present a spectrum of trace-based, testing, and bisimulation equivalences for nondeterministic and probabilistic processes whose activities are all observable. For every equivalence under study, we examine the discriminating power of three variants stemming from three approaches that differ for the way probabilities of events are compared when nondeterministic choices are resolved via deterministic schedulers. We show that the first approach - which compares two resolutions relatively to the probability distributions of all considered events - results in a fragment of the spectrum compatible with the spectrum of behavioral equivalences for fully probabilistic processes. In contrast, the second approach - which compares the probabilities of the events of a resolution with the probabilities of the same events in possibly different resolutions - gives rise to another fragment composed of coarser equivalences that exhibits several analogies with the spectrum of behavioral equivalences for fully nondeterministic processes. Finally, the third approach - which only compares the extremal probabilities of each event stemming from the different resolutions - yields even coarser equivalences that, however, give rise to a hierarchy similar to that stemming from the second approach.
In the paper Relating Strong Behavioral Equivalences for Processes with Nondeterminism and Probabilities to appear in TCS, we present a comparison of behavioral equivalences for nondeterministic and probabilistic processes. In particular, we consider strong trace, failure, testing, and bisimulation equivalences. For each of these groups of equivalences, we examine the discriminating power of three variants stemming from three approaches that differ for the way probabilities of events are compared when nondeterministic choices are resolved via deterministic schedulers. The established relationships are summarized in a so-called spectrum. However, the equivalences we consider in that paper are only a small subset of those considered in the original spectrum of equivalences for nondeterministic systems introduced by Rob van Glabbeek. In this companion paper we we enlarge the spectrum by considering variants of trace equivalences (completed-trace equivalences), additional decorated-trace equivalences (failure-trace, readiness, and ready-trace equivalences), and variants of bisimulation equivalences (kernels of simulation, completed-simulation, failure-simulation, and ready-simulation preorders). Moreover, we study how the spectrum changes when randomized schedulers are used instead of deterministic ones.
We study the decidability of termination for two CHR dialects which, similarly to the Datalog like languages, are defined by using a signature which does not allow function symbols (of arity >0). Both languages allow the use of the = built-in in the body of rules, thus are built on a host language that supports unification. However each imposes one further restriction. The first CHR dialect allows only range-restricted rules, that is, it does not allow the use of variables in the body or in the guard of a rule if they do not appear in the head. We show that the existence of an infinite computation is decidable for this dialect. The second dialect instead limits the number of atoms in the head of rules to one. We prove that in this case, the existence of a terminating computation is decidable. These results show that both dialects are strictly less expressive than Turing Machines. It is worth noting that the language (without function symbols) without these restrictions is as expressive as Turing Machines.
Higher-order processes with parameterization are capable of abstraction and application (migrated from the lambda-calculus), and thus are computationally more expressive. For the minimal higher-order concurrency, it is well-known that the strong bisimilarity (i.e., the strong bisimulation equality) is decidable in absence of parameterization. By contrast, whether the strong bisimilarity is still decidable for parameterized higher-order processes remains unclear. In this paper, we focus on this issue. There are basically two kinds of parameterization: one on names and the other on processes. We show that the strong bisimilarity is indeed decidable for higher-order processes equipped with both kinds of parameterization. Then we demonstrate how to adapt the decision approach to build an axiom system for the strong bisimilarity. On top of these results, we provide an algorithm for the bisimilarity checking.
We show that the $p$-power maps in the first Hochschild cohomology space of finite-dimensional selfinjective algebras over a field of prime characteristic $p$ commute with stable equivalences of Morita type on the subgroup of classes represented by integrable derivations. We show, by giving an example, that the $p$-power maps do not necessarily commute with arbitrary transfer maps in the Hochschild cohomology of symmetric algebras.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
