ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 15 Issue 4, August 2014

Refining the Process Rewrite Systems Hierarchy via Ground Tree Rewrite Systems
Stefan Göller, Anthony Widjaja Lin
Article No.: 26
DOI: 10.1145/2629679

In his seminal paper, Mayr introduced the well-known process rewrite systems (PRS) hierarchy, which contains many well-studied classes of infinite-state systems including pushdown systems (PDS), Petri nets, and PA-processes. A separate development...

Temporal Specifications with Accumulative Values
Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman
Article No.: 27
DOI: 10.1145/2629686

Recently, there has been an effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions.

At the heart of quantitative...

Identifying Efficient Abductive Hypotheses Using Multicriteria Dominance Relation
Maciej Komosinski, Adam Kups, Dorota Leszczyńska-Jasion, Mariusz Urbański
Article No.: 28
DOI: 10.1145/2629669

In this article, results of the automation of an abductive procedure are reported. This work is a continuation of our earlier research [Komosinski et al. 2012], where a general scheme of the procedure has been proposed. Here, a more advanced...

The Ordering Principle in a Fragment of Approximate Counting
Albert Atserias, Neil Thapen
Article No.: 29
DOI: 10.1145/2629555

The ordering principle states that every finite linear order has a least element. We show that, in the relativized setting, the surjective weak pigeonhole principle for polynomial time functions does not prove a Herbrandized version of the...

Fuzzy Time in Linear Temporal Logic
Achille Frigeri, Liliana Pasquale, Paola Spoletini
Article No.: 30
DOI: 10.1145/2629606

In the past years, the adoption of adaptive systems has increased in many fields of computer science, such as databases and software engineering. These systems are able to automatically react to events by collecting information from the external...

A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures
Gerhard Schellhorn, John Derrick, Heike Wehrheim
Article No.: 31
DOI: 10.1145/2629496

Efficient implementations of data structures such as queues, stacks or hash-tables allow for concurrent access by many processes at the same time. To increase concurrency, these algorithms often completely dispose with locking, or only lock small...

Terminating Evaluation of Logic Programs with Finite Three-Valued Models
Fabrizio Riguzzi, Terrance Swift
Article No.: 32
DOI: 10.1145/2629337

As evaluation methods for logic programs have become more sophisticated, the classes of programs for which termination can be guaranteed have expanded. From the perspective of ar set programs that include function symbols, recent work has...

Inference of Field-Sensitive Reachability and Cyclicity
Damiano Zanardini, Samir Genaim
Article No.: 33
DOI: 10.1145/2629478

In heap-based languages, knowing that a variable x points to an acyclic data structure is useful for analyzing termination. This information guarantees that the depth of the data structure to which x points is greater than the depth of the...

Reasoning About Strategies: On the Model-Checking Problem
Fabio Mogavero, Aniello Murano, Giuseppe Perelli, Moshe Y. Vardi
Article No.: 34
DOI: 10.1145/2631917

In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between agents and express the correctness of the system no matter how the environment behaves. An important contribution...

A General Theory of Barbs, Contexts, and Labels
Filippo Bonchi, Fabio Gadducci, Giacoma Valentina Monreale
Article No.: 35
DOI: 10.1145/2631916

Barbed bisimilarity is a widely used behavioral equivalence for interactive systems: given a set of predicates (denoted “barbs” and representing basic observations on states) and a set of contexts (representing the possible execution...