اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدKeep it Fair: Equivalences
67
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
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.
قيم البحث
اقرأ أيضاً
In this paper, we study cache policies for cloud-based caching. Cloud-based caching uses cloud storage services such as Amazon S3 as a cache for data items that would have been recomputed otherwise. Cloud-based caching departs from classical caching:
cloud resources are potentially infinite and only paid when used, while classical caching relies on a fixed storage capacity and its main monetary cost comes from the initial investment. To deal with this new context, we design and evaluate a new caching policy that minimizes the overall cost of a cloud-based system. The policy takes into account the frequency of consumption of an item and the cloud cost model. We show that this policy is easier to operate, that it scales with the demand and that it outperforms classical policies managing a fixed capacity.
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 test
ing and shows that the resulting semantic equivalence also captures conditional liveness properties. It is strictly finer than both the may- and must-testing equivalence.
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 combina
torial 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.
This work presents Keep it Simple (KiS), a new approach to unsupervised text simplification which learns to balance a reward across three properties: fluency, salience and simplicity. We train the model with a novel algorithm to optimize the reward (
k-SCST), in which the model proposes several candidate simplifications, computes each candidates reward, and encourages candidates that outperform the mean reward. Finally, we propose a realistic text comprehension task as an evaluation method for text simplification. When tested on the English news domain, the KiS model outperforms strong supervised baselines by more than 4 SARI points, and can help people complete a comprehension task an average of 18% faster while retaining accuracy, when compared to the original text. Code available: https://github.com/tingofurro/keep_it_simple
Two of the most studied extensions of trace and testing equivalences to nondeterministic and probabilistic processes induce distinctions that have been questioned and lack properties that are desirable. Probabilistic trace-distribution equivalence di
fferentiates systems that can perform the same set of traces with the same probabilities, and is not a congruence for parallel composition. Probabilistic testing equivalence, which relies only on extremal success probabilities, is backward compatible with testing equivalences for restricted classes of processes, such as fully nondeterministic processes or generative/reactive probabilistic processes, only if specific sets of tests are admitted. In this paper, n
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
