No Arabic abstract
This note draws conclusions that arise by combining two recent papers, by Anuj Dawar, Erich Gradel, and Wied Pakusa, published at ICALP 2019 and by Moritz Lichter, published at LICS 2021. In both papers, the main technical results rely on the combinatorial and algebraic analysis of the invertible-map equivalences $equiv^text{IM}_{k,Q}$ on certain variants of Cai-Furer-Immerman (CFI) structures. These $equiv^text{IM}_{k,Q}$-equivalences, for a natural number $k$ and a set of primes $Q$, refine the well-known Weisfeiler-Leman equivalences used in algorithms for graph isomorphism. The intuition is that two graphs $G equiv^text{IM}_{k,Q} H$ cannot be distinguished by iterative refinements of equivalences on $k$-tuples defined via linear operators on vector spaces over fields of characteristic $p in Q$. In the first paper it has been shown that for a prime $q otin Q$, the $equiv^text{IM}_{k,Q}$ equivalences are not strong enough to distinguish between non-isomorphic CFI-structures over the field $mathbb{F}_q$. In the second paper, a similar but not identical construction for CFI-structures over the rings $mathbb{Z}_{2^i}$ has been shown to be indistinguishable with respect to $equiv^text{IM}_{k,{2}}$. Together with earlier work on rank logic, this second result suffices to separate rank logic from polynomial time. We show here that the two approaches can be unified to prove that CFI-structures over the rings $mathbb{Z}_{2^i}$ are indistinguishable with respect to $equiv^text{IM}_{k,mathbb{P}}$, for the set $mathbb{P}$ of all primes. This implies the following two results. 1. There is no fixed $k$ such that the invertible-map equivalence $equiv^text{IM}_{k,mathbb{P}}$ coincides with isomorphism on all finite graphs. 2. No extension of fixed-point logic by linear-algebraic operators over fields can capture polynomial time.
For models of concurrent and distributed systems, it is important and also challenging to establish correctness in terms of safety and/or liveness properties. Theories of distributed systems consider equivalences fundamental, since they (1) preserve desirable correctness characteristics and (2) often allow for component substitution making compositional reasoning feasible. Modeling distributed systems often requires abstraction utilizing nondeterminism which induces unintended behaviors in terms of infinite executions with one nondeterministic choice being recurrently resolved, each time neglecting a single alternative. These situations are considered unrealistic or highly improbable. Fairness assumptions are commonly used to filter system behaviors, thereby distinguishing between realistic and unrealistic executions. This allows for key arguments in correctness proofs of distributed systems, which would not be possible otherwise. Our contribution is an equivalence spectrum in which fairness assumptions are preserved. The identified equivalences allow for (compositional) reasoning about correctness incorporating fairness assumptions.
May and must testing were introduced by De Nicola and Hennessy to define semantic equivalences on processes. May-testing equivalence exactly captures safety properties, and must-testing equivalence liveness properties. This paper proposes reward testing and shows that the resulting semantic equivalence also captures conditional liveness properties. It is strictly finer than both the may- and must-testing equivalence.
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.
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.
We investigate the impact of modifying the constraining relations of a Constraint Satisfaction Problem (CSP) instance, with a fixed template, on the set of solutions of the instance. More precisely we investigate sensitive instances: an instance of the CSP is called sensitive, if removing any tuple from any constraining relation invalidates some solution of the instance. Equivalently, one could require that every tuple from any one of its constraints extends to a solution of the instance. Clearly, any non-trivial template has instances which are not sensitive. Therefore we follow the direction proposed (in the context of strict width) by Feder and Vardi (SICOMP 1999) and require that only the instances produced by a local consistency checking algorithm are sensitive. In the language of the algebraic approach to the CSP we show that a finite idempotent algebra $mathbf{A}$ has a $k+2$ variable near unanimity term operation if and only if any instance that results from running the $(k, k+1)$-consistency algorithm on an instance over $mathbf{A}^2$ is sensitive. A version of our result, without idempotency but with the sensitivity condition holding in a variety of algebras, settles a question posed by G. Bergman about systems of projections of algebras that arise from some subalgebra of a finite product of algebras. Our results hold for infinite (albeit in the case of $mathbf{A}$ idempotent) algebras as well and exhibit a surprising similarity to the strict width $k$ condition proposed by Feder and Vardi. Both conditions can be characterized by the existence of a near unanimity operation, but the arities of the operations differ by 1.