ACM DL

ACM Transactions on

Computational Logic (TOCL)

Menu
Latest Articles

Modularisation of Sequent Calculi for Normal and Non-normal Modalities

In this work, we explore the connections between (linear) nested sequent calculi and ordinary sequent calculi for normal and non-normal modal logics.... (more)

The Complexity of Minimal Inference Problem for Conservative Constraint Languages

We study the complexity of the inference problem for propositional circumscription (the minimal inference problem) over arbitrary finite domains. The... (more)

Tight Bounds on the Asymptotic Descriptive Complexity of Subgraph Isomorphism

Let v(F) denote the number of vertices in a fixed connected pattern graph F. We show an infinite family of patterns F such that the existence of a... (more)

Reasoning about Strategic Abilities: Agents with Truly Perfect Recall

In alternating-time temporal logic ATL*, agents with perfect recall assign choices to sequences of states, i.e., to possible finite histories of the game. However, when a nested strategic modality is interpreted, the new strategy does not take into account the previous sequence of events. It is as if agents collect their observations in the... (more)

Synchronizing Data Words for Register Automata

Register automata (RAs) are finite automata extended with a finite set of registers to store and compare data from an infinite domain. We study the concept of synchronizing data words in RAs: does there exist a data word that sends all states of the RA to a single state? For deterministic RAs with k registers (k-DRAs), we prove that inputting data... (more)

Fast Query Answering over Existential Rules

Enhancing Datalog with existential quantification gives rise to Datalog∃, a powerful knowledge representation language widely used in ontology-based query answering. In this setting, a conjunctive query is evaluated over a Datalog∃ program consisting of extensional data paired with so-called “existential” rules. Owing to... (more)

NEWS

About
TOCL welcomes submissions related to all aspects of logic as it pertains to topics in computer science. The journal is published quarterly. The first issue appeared in July 2000, and the journal is indexed by ISI beginning with the 2006 volume. About

Forthcoming Articles

Pure Sequent Calculi: Analyticity and Decision Procedure

Analyticity, a.k.a. the subformula property, typically guarantees decidability of derivability in propositional sequent calculi. To utilize this fact, two substantial gaps have to be filled: $(i)$ what makes a sequent calculus analytic? and $(ii)$ how to obtain an efficient decision procedure for derivability in an analytic calculus? In the first part of this paper we address these gaps for \emph{pure calculi}---a general family of fully structural propositional sequent calculi whose rules allow arbitrary context formulas. We provide a sufficient syntactic criterion for analyticity in these calculi, as well as a fruitful method to construct new analytic calculi from given ones. We further introduce a scalable decision procedure for derivability in analytic pure calculi, by showing that it can be (uniformly) reduced to classical satisfiability. In the second part of the paper, we study the extension of pure sequent calculi with rules for modal operators. We show that such extensions preserve the analyticity of the calculus, and identify certain restricted operators (which we call `Next' operators) that are also amenable for a general reduction of derivability to classical satisfiability. Our proofs are all semantic, utilizing several strong general soundness and completeness theorems with respect to non-deterministic semantic frameworks: bivaluations (for pure calculi) and Kripke models (for their extension with modal operators).

1-Safe Petri nets and special cube complexes: equivalence and applications

Nielsen, Plotkin, and Winskel (1981) proved that every 1-safe Petri net $N$ unfolds into an event structure $\mathcal{E}_N$. By a result of Thiagarajan (1996 and 2002), these unfoldings are exactly the trace regular event structures. Thiagarajan (1996 and 2002) conjectured that regular event structures correspond exactly to trace regular event structures. In a recent paper (Chalopin and Chepoi, 2017, 2018), we disproved this conjecture, based on the striking bijection between domains of event structures, median graphs, and CAT(0) cube complexes. On the other hand, we proved that Thiagarajan's conjecture is true for regular event structures whose domains are principal filters of universal covers of (virtually) finite special cube complexes. In the current paper, we prove the converse: to any finite 1-safe Petri net $N$ one can associate a finite special cube complex ${X}_N$ such that the domain of the event structure $\mathcal{E}_N$ (obtained as the unfolding of $N$) is a principal filter of the universal cover $\widetilde{X}_N$ of $X_N$. This establishes a bijection between 1-safe Petri nets and finite special cube complexes and provides a combinatorial characterization of trace regular event structures. Using this bijection and techniques from graph theory and geometry (MSO theory of graphs, bounded treewidth, and bounded hyperbolicity) we disprove yet another conjecture by Thiagarajan (from the paper with S. Yang from 2014) that the monadic second order logic of a 1-safe Petri net is decidable if and only if its unfolding is grid-free.

A SAT Approach to Branchwidth

Branch decomposition is a prominent method for structurally decomposing a graph, hypergraph or CNF formula. The width of a branch decomposition provides a measure of how well the object is decomposed. For many applications it is crucial to compute a branch decomposition whose width is as small as possible. We propose a SAT approach to finding branch decompositions of small width. The core of our approach is an efficient SAT encoding which determines with a single SAT-call whether a given hypergraph admits a branch decomposition of certain width. For our encoding we developed a novel partition-based characterization of branch decomposition. The encoding size imposes a limit on the size of the given hypergraph. In order to break through this barrier and to scale the SAT approach to larger instances, we developed a new heuristic approach where the SAT encoding is used to locally improve a given candidate decomposition until a fixed-point is reached. This new method scales now to instances with several thousands of vertices and edges.

Polarised Nominal Quantifiers Model Private Names in Non-Commutative Logic

This paper explores the proof theory necessary for recommending an expressive but decidable first-order system, named MAV1, featuring a de Morgan dual pair of nominal quantifiers. These nominal quantifiers called `new' and `wen' are distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of these nominal quantifiers is they are polarised in the sense that `new' distributes over positive operators while `wen' distributes over negative operators. This greater control of bookkeeping enables private names to be modelled in processes embedded as predicates in MAV1. The technical challenge is to establish a cut elimination result, from which essential properties including the transitivity of implication follow. Since the system is defined using the calculus of structures, a generalisation of the sequent calculus, novel techniques are employed. The proof relies on an intricately designed multiset-based measure of the size of a proof, which is used to guide a normalisation technique called splitting. The presence of equivariance, which swaps successive quantifiers, induces complex inter-dependencies between nominal quantifiers, additive conjunction and multiplicative operators in the proof of splitting. Every rule is justified by an example demonstrating why the rule is necessary for soundly embedding processes and ensuring that cut elimination holds.

On the Verification of Livelock-Freedom and Self-Stabilization on Parameterized Rings

This paper investigates the verification of livelock-freedom and self-stabilization on parameterized rings consisting of symmetric, constant space, deterministic and self-disabling processes. The results of this paper have a significant impact on several fields including scalable distributed systems, resilient and self-* systems, and verification of parameterized systems. First, we identify necessary and sufficient local conditions for the existence of global livelocks in parameterized unidirectional rings with unbounded (but finite) number of processes under the interleaving semantics. Using a reduction from the periodic domino problem, we show that, in general, verifying livelock-freedom of parameterized unidirectional rings is undecidable even for constant space, deterministic and self-disabling processes. This result implies that verifying self-stabilization for parameterized rings of self-disabling processes is also undecidable. We also show that verifying livelock-freedom and self-stabilization remain undecidable under (1) synchronous execution semantics; (2) the FIFO consistency model, and (3) unfair and weak scheduling policies. We then present a new scope-based method for detecting and constructing livelocks in parameterized rings. The proposed semi-algorithm behind our scope-based verification is based on a novel paradigm for the detection of livelocks that totally circumvents state space exploration. The results of this paper have significant implications for scalable distributed systems with cyclic topologies.

Binary reachability of timed-register pushdown automata, and branching vector addition systems

All ACM Journals | See Full Journal Index

Search TOCL
enter search term and/or author name