ACM DL

ACM Transactions on

Computational Logic (TOCL)

Menu
Latest Articles

Proof Complexity Meets Algebra

We analyze how the standard reductions between constraint satisfaction problems affect their proof complexity. We show that, for the most studied propositional, algebraic, and semialgebraic proof systems, the classical constructions of pp-interpretability, homomorphic equivalence, and addition of constants to a core preserve the proof complexity of... (more)

Checking Admissibility Using Natural Dualities

This article presents a new method for obtaining small algebras to check the admissibility—equivalently, validity in free algebras—of quasi-identities in a finitely generated quasivariety. Unlike a previous algebraic approach of Metcalfe and Röthlisberger, which is feasible only when the relevant free algebra is not too... (more)

Generalized Eilenberg Theorem: Varieties of Languages in a Category

For finite automata as coalgebras in a category C, we study languages they accept and varieties of such languages. This generalizes Eilenberg’s concept of a variety of languages, which corresponds to choosing as C the category of Boolean algebras. Eilenberg established a bijective correspondence between pseudovarieties of monoids and... (more)

Interval vs. Point Temporal Logic Model Checking: An Expressiveness Comparison

In recent years, model checking with interval temporal logics is emerging as a viable alternative to model checking with standard point-based temporal logics, such as LTL, CTL, CTL*, and the like. The behavior of the system is modeled by means of (finite) Kripke structures, as usual. However, while temporal logics which are interpreted... (more)

A Higher-Order Calculus of Computational Fields

The complexity of large-scale distributed systems, particularly when deployed in physical space, calls for new mechanisms to address composability and reusability of collective adaptive behaviour. Computational fields have been proposed as an effective abstraction to fill the gap between the macro-level of such systems (specifying a... (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

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 words with 2k+1 distinct data, from the infinite data domain, is sufficient to synchronize. We show that the synchronizing problem for DRAs is in general PSPACE-complete, and is NLOGSPACE-complete for 1-DRAs. For nondeterministic RAs (NRAs), we show that Ackermann(n) distinct data (where n is the size of the RA) might be necessary to synchronize. The synchronizing problem for NRAs is in general undecidable, however, we establish Ackermann-completeness of the problem for 1-NRAs. Our most substantial achievement is proving NEXPTIME-completeness of the length-bounded synchronizing problem for NRAs (length encoded in binary). A variant of this last construction allows to prove that the bounded universality problem for NRAs is coNEXPTIME-complete.

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 subgraph isomorphic to F is expressible by a first-order sentence of quantifier depth (2/3)v(F)+1, assuming that the host graph is sufficiently large and connected. On the other hand, this is impossible for any F with using less than (2/3)v(F)-2 first-order variables.

Fast Query Answering over Existential Rules

Enhancing Datalog with existential quantification gives rise to Datalog^E, a powerful knowledge representation language widely used in ontology-based query answering. In this setting, a conjunctive query is evaluated over a Datalog^E program consisting of extensional data paired with so-called existential rules. Due to their high expressiveness, such rules make the evaluation of queries undecidable, even when the latter are atomic. Decidable Datalog^E fragments have been proposed in the literature (e.g., weakly-acyclic and weakly-guarded); but they pay the price of a higher computational complexity, hindering the implementation of effective systems. Conversely, the results in this paper demonstrate that it is definitely possible to enable fast yet powerful query answering over existential rules, ensuring decidability without any complexity overhead. On the theoretical side, we define the class of parsimonious programs which guarantees decidability of atomic queries. We then strengthen this class to strongly parsimonious programs ensuring decidability also for conjunctive queries. Since parsimony is an undecidable property, we single out Shy, an easily recognizable class of strongly parsimonious programs that generalizes Datalog while preserving its complexity even under conjunctive query evaluation. Shy generalizes also the class of linear existential programs, while it is uncomparable to the other main classes ensuring decidability. On the practical side, we exploit our results to implement DLV^E, an effective system for query answering over parsimonious existential rules. To asses its efficiency, we carry out an experimental analysis, comparing DLV^E against state-of-the-art systems for ontology-based query answering. The results confirm the effectiveness of DLV^E, which outperforms all other systems.

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 nested game again from scratch, thus effectively forgetting what they observed before. Intuitively, it does not fit the assumption of agents having perfect recall of the past. In this paper, we investigate the alternative semantics for ATL* where the past is not forgotten in nested games. We show that the standard semantics of ATL* coincides with the truly perfect recall semantics in case of agents with perfect information. On the other hand, the two semantics differ significantly if agents have imperfect information about the state of the game. The same applies to the standard vs. truly perfect recall semantics of ATL* with persistent strategies. We compare the relevant variants of ATL* by looking at their their expressive power, sets of validities, and feasibility of model checking.

All ACM Journals | See Full Journal Index

Search TOCL
enter search term and/or author name