ACM DL

ACM Transactions on

Computational Logic (TOCL)

Menu
Latest Articles

Typing Messages for Free in Security Protocols

Security properties of cryptographic protocols are typically expressed as reachability or equivalence properties. Secrecy and authentication are examples of reachability properties, while privacy properties such as untraceability, vote secrecy, or anonymity are generally expressed as behavioral equivalence in a process algebra that models security... (more)

Verification Methods for the Computationally Complete Symbolic Attacker Based on Indistinguishability

In recent years, a new approach has been developed for verifying security protocols with the aim of... (more)

Reason-maintenance Belief Logic with Uncertain Information

In this article, we propose a logic for reasoning about belief based on fusion of uncertain information. The resultant reason-maintenance... (more)

Fixed-point Elimination in the Intuitionistic Propositional Calculus

It follows from known results in the literature that least and greatest fixed-points of monotone polynomials on Heyting algebras—that is, the... (more)

Runtime Verification over Out-of-order Streams

We present an approach for verifying systems at runtime. Our approach targets distributed systems whose components communicate with monitors over unreliable channels, where messages can be delayed, reordered, or even lost. Furthermore, our approach handles an expressive specification language that extends the real-time logic MTL with freeze... (more)

Monadic Datalog, Tree Validity, and Limited Access Containment

We reconsider the problem of containment of monadic datalog (MDL) queries in unions of conjunctive queries (UCQs). Prior work has dealt with special... (more)

Satisfiability of Modal Inclusion Logic: Lax and Strict Semantics

We investigate the computational complexity of the satisfiability problem of modal inclusion logic. We distinguish two variants of the problem: one for the strict and another one for the lax semantics. Both problems turn out to be EXPTIME-complete on general structures. Finally, we show how for a specific class of structures NEXPTIME-completeness... (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

Finite Open-World Query Answering With Number Restrictions

Open-world query answering is the problem of deciding, given a set of facts, conjunction of constraints, and query, whether the facts and constraints imply the query. This amounts to reasoning over all instances that include the facts and satisfy the constraints. We study \emph{finite open-world query answering} (FQA), which assumes that the underlying world is finite and thus only considers the finite completions of the instance. The major known decidable cases of FQA derive from the following: the guarded fragment of first-order logic, which can express referential constraints (data in one place points to data in another) but cannot express number restrictions such as functional dependencies; and the guarded fragment with number restrictions but on a signature of arity only two. In this paper, we give the first decidability results for FQA that combine both referential constraints and number restrictions for arbitrary signatures: we show that, for unary inclusion dependencies and functional dependencies, the finiteness assumption of FQA can be lifted up to taking the finite implication closure of the dependencies. Our result relies on new techniques to construct finite universal models of such constraints, for any bound on the maximal query size.

Adding successor: A transfer theorem for separation and covering

Given a class C of word languages, the C-separation problem asks for an algorithm that, given as input two regular languages, decides whether there exists a third language in C containing the first language, while being disjoint from the second. Separation is usually investigated as a means to obtain a deep understanding of the class C. In the paper, we are mainly interested in classes defined by logical formalisms. Such classes are often built on top of each other: given some logic, one builds a stronger one by adding new predicates to its signature. A natural construction is to enrich a logic with the successor relation. In this paper, we present a transfer result applying to this construction: we show that for suitable logically defined classes, separation for the logic enriched with the successor relation reduces to separation for the original logic. Our theorem also applies to a problem that is stronger than separation: covering. Moreover, we actually present two reductions: one for languages of finite words and the other for languages of infinite words.

A First-Order Logic for Reasoning about Knowledge and Probability

We present a first-order probabilistic epistemic logic, which allows combining operators of knowledge and probability within a group of possibly infinitely many agents. The proposed framework is the first order extension of the logic of Fagin and Halpern from (J.ACM 41:340-367,1994). We define its syntax and semantics, and prove the strong completeness property of the corresponding axiomatic system.

Dynamic QBF Dependencies in Reduction and Expansion

We provide the first proof complexity results for QBF dependency calculi. By showing that the reflexive resolution path dependency scheme admits exponentially shorter Q-resolution proofs on a known family of instances, we answer a question first posed by Slivovsky and Szeider in 2014. Further, we conceive a method of QBF solving in which dependency recomputation is utilised as a form of inprocessing. Formalising this notion, we introduce a new version of Q-resolution in which a dependency scheme is applied dynamically. We demonstrate the further potential of this approach beyond that of the existing static system with an exponential separation. Lastly, we show that the same picture emerges in an analogous approach to the universal expansion paradigm.

Model-Checking on Ordered Structures

We study the model-checking problem for first- and monadic second-order logic on finite relational structures. The problem of verifying whether a formula of these logics is true on a given structure is considered intractable in general, but it does become tractable on interesting classes of structures, such as on classes whose Gaifman graphs have bounded treewidth. In this paper we continue this line of research and study model-checking for first- and monadic second-order logic in the presence of an ordering on the input structure. We do so in two settings: the general ordered case, where the input structures are equipped with a fixed order or successor relation, and the order invariant case, where the formulas may resort to an ordering, but their truth must be independent of the particular choice of order. In the first setting we show very strong intractability results for most interesting classes of structures. In contrast, in the order invariant case we obtain tractability results for order-invariant monadic second-order formulas on the same classes of graphs as in the unordered case. For first-order logic, we obtain tractability of successor-invariant formulas on classes whose Gaifman graphs have bounded expansion. Furthermore, we show that model-checking for order-invariant first-order formulas is tractable on coloured posets of bounded width.

Extending Liquid Types to Arrays

A liquid type is an ordinary Hindley-Milner type annotated with a logical predicate that states the properties satisfied by the elements of that type. Liquid types are a powerful tool for program verification, since programmers can use them to specify pre- and postconditions of their programs, while the predicates of intermediate variables and auxiliary functions are inferred automatically. Type inference is feasible in this context, since the logical predicates within liquid types are constrained to a quantifier-free logic in order to maintain decidability. In this paper we extend liquid types by allowing them to contain quantified properties on arrays, so that they can be used to infer invariants on array-related programs (for example, implementations of sorting algorithms). Although quantified logic is, in general, undecidable, we restrict properties on arrays to a decidable subset introduced by Bradley et al. We describe in detail the extended type system, the verification condition generator, and the iterative weakening algorithm for inferring invariants. After proving the correctness and completeness of these two algorithms, we apply them to find invariants on a set of algorithms involving array manipulations.

Idempotent Anti-Unification

In this paper we address two problems related to idempotent anti-unification. First, we show that there exists an anti-unification problem with a single idempotent symbol which has an infinite minimal complete set of generalizations. It means that anti-unification with a single idempotent symbol has infinitary or nullary generalization type, similar to anti-unification with two idem- potent symbols, shown earlier by Loı?c Pottier. Next, we develop an algorithm, which takes an arbitrary idempotent anti-unification problem and computes a representation of its solution set in the form of a regular tree grammar. The algorithm does not depend on the number of idempotent function symbols in the input terms. The language generated by the grammar is the minimal complete set of generalizations of the given anti-unification problem, which implies that idem- potent anti-unification is infinitary.

Intuitionistic Linear Temporal Logics

We consider intuitionistic variants of linear temporal logic with `next', `until' and `release' based on {\em expanding posets:} partial orders equipped with an order-preserving transition function. This class of structures gives rise to a logic which we denote $ITL^e$, and by imposing additional constraints we obtain the logics $ITL^p$ of {\em persistent posets} and $ITL^{ht}$ of {\em here-and-there temporal logic,} both of which have been considered in the literature. We prove that $ITL^e$ has the effective finite model property and hence is decidable, while $ITL^p$ does not have the finite model property. We also introduce notions of bounded bisimulations for these logics and use them to show that the `until' and `release' operators are not definable in terms of each other, even over the class of persistent posets.

All ACM Journals | See Full Journal Index

Search TOCL
enter search term and/or author name