Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 1905.11733

Confluence by Critical Pair Analysis Revisited (Extended Version)

Nao Hirokawa·Julian Nagele·Vincent van Oostrom·Michio Oyamaguchi
View original source ↗Read source document ↗Export metadata ↓

Abstract

We present two methods for proving confluence of left-linear term rewrite systems. One is hot-decreasingness, combining the parallel/development closedness theorems with rule labelling based on a terminating subsystem. The other is critical-pair-closing system, allowing to boil down the confluence problem to confluence of a special subsystem whose duplicating rules are relatively terminating.

Explore related subjects

cs.LOcs.SC

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Nao Hirokawa, Julian Nagele, Vincent van Oostrom, Michio Oyamaguchi. 2019-06-03. Confluence by Critical Pair Analysis Revisited (Extended Version). https://arxiv.org/abs/1905.11733

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

JustAct: A Framework for Auditable Multi-Agent Systems Regulated by Inter-Organisational Policies

In open multi-agent agent systems that cross organisational boundaries, agent actions must be regulated by complex policies. Consider medical data processing systems, which must observe generic laws (e.g., EU data protection regulations) and also specific participants' resource conditions (e.g., Bob consents to sharing his X-Rays with EU hospitals). Presently, we address the implementation of these systems as distributed software. Solutions to key sub-problems are available: existing policy languages capture the necessary normative concepts and formalise the computational representation and reasoning about policies, and existing distributed algorithms and protocols coordinate agents' changing actions and policies. But which policies and protocols are useful in application? With the JustAct framework, we characterise a class of multi-agent systems where actors justify their actions with sufficient policy information collected from dynamic policy statements and agreements. We prove key properties of these systems, e.g., any decision that an action is permitted now cannot be refuted later, regardless of any added statements or updated agreements. We study a particular instance of the framework by specifying (in Rocq) and implementing (in Rust) a particular policy language and runtime system for mediating agent communications. We demonstrate and assess JustAct via a case study of this implementation: we reproduce the usage scenarios of Brane, an existing policy-regulated, inter-domain, medical data processing system.

cs.LO↗
arXiv2026

Undefinability of Approximation of 2-to-2 Games

Recent work by Atserias and Dawar (J. Log. Comp 2019) and Tucker-Foltz (LMCS 2024) has established undefinability results in fixed-point logic with counting (FPC) corresponding to many classical complexity results from the hardness of approximation. In this line of work, NP-hardness results are turned into unconditional FPC undefinability results. We extend this work by showing the FPC undefinability of any constant factor approximation of weighted 2-to-2 games, based on the NP-hardness results of Khot, Minzer and Safra. Our result shows that the completely satisfiable 2-to-2 games are not FPC-separable from those that are not epsilon-satisfiable, for arbitrarily small epsilon. The perfect completeness of our inseparability is an improvement on the complexity result, as the NP-hardness of such a separation is still only conjectured. This perfect completeness enables us to show the FPC undefinability of other problems whose NP-hardness is conjectured. In particular, we are able to show that no FPC formula can separate the 3-colourable graphs from those that are not t-colourable, for any constant t.

cs.LO↗
arXiv2026

Possibilistic Computation Tree Logic over Finitely-Valued Kripke Structures: Decidability and Complete Axiomatization

Possibilistic computation tree logic (PoCTL) is a branching-time temporal logic for specifying and verifying systems whose behavior is described by possibility theory. Although the model-checking problem for PoCTL has been investigated, its satisfiability problem and proof-theoretic foundations, particularly the development of a sound and complete axiomatization,remain largely unexplored. We investigate these problems over normalized possibilistic Kripke structures whose transition possibilities take finitely many values; their state spaces may be countably infinite. A counterexample shows that unrestricted countable structures do not have the finite-model property, thereby distinguishing the semantic scope of the present results. For the finitely-valued class, we extract a finite threshold scale from the input formula and define canonical admissible transitions by the set $D(s,t)$. Independent eventuality ranks guide the selection of local witnesses. Finite supported fragments are then spliced cyclically to obtain a model, without requiring the ranks of different eventualities to decrease simultaneously. This yields a finite-model property. Satisfiability for the unbounded language over this class is EXPTIME-complete, and the tableau procedure runs in time $2^{O(n^2)}$. Bounded operators are handled by explicit finite unfolding, with complexity measured after this preprocessing. Finally, we establish a sound and weakly complete finitary axiomatization by translating tableau deletion into formal refutations.

cs.LO↗