Search ACM DL

Search Issue

enter search term and/or author name

**Robust Vacuity for Branching Temporal Logic**

Arie Gurfinkel, Marsha Chechik

Article No.: 1

DOI: 10.1145/2071368.2071369

There is a growing interest in techniques for detecting whether a logic specification is satisfied too easily, or *vacuously*. For example, the specification “every request is eventually followed by an acknowledgment” is satisfied...

**Least and Greatest Fixed Points in Linear Logic**

David Baelde

Article No.: 2

DOI: 10.1145/2071368.2071370

The first-order theory of MALL (multiplicative, additive linear logic) over only equalities is a well-structured but weak logic since it cannot capture unbounded (infinite) behavior. Instead of accounting for unbounded behavior via the addition of...

**Topological and Simplicial Models of Identity Types**

Benno van den Berg, Richard Garner

Article No.: 3

DOI: 10.1145/2071368.2071371

In this paper we construct new categorical models for the identity types of Martin-Löf type theory, in the categories **Top** of topological spaces and **SSet** of simplicial sets. We do so building on earlier work of Awodey and Warren...

**Succinctness of the Complement and Intersection of Regular Expressions**

Wouter Gelade, Frank Neven

Article No.: 4

DOI: 10.1145/2071368.2071372

We study the succinctness of the complement and intersection of regular expressions. In particular, we show that when constructing a regular expression defining the complement of a given regular expression, a double exponential size increase...

**The Complexity of Positive First-Order Logic without Equality**

Florent Madelaine, Barnaby Martin

Article No.: 5

DOI: 10.1145/2071368.2071373

We study the complexity of evaluating positive equality-free sentences of first-order (FO) logic over a fixed, finite structure *B*. This may be seen as a natural generalisation of the nonuniform quantified constraint satisfaction problem...

**On the Expressive Power of Multiple Heads in CHR**

Cinzia Di Giusto, Maurizio Gabbrielli, Maria Chiara Meo

Article No.: 6

DOI: 10.1145/2071368.2071374

Constraint Handling Rules (CHR) is a committed-choice declarative language that has been originally designed for writing constraint solvers and is nowadays a general purpose language. CHR programs consist of multiheaded guarded rules which allow...

**Reachability Problems in Piecewise FIFO Systems**

Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, Richard Trefler

Article No.: 7

DOI: 10.1145/2071368.2071375

Systems consisting of several finite components that communicate via unbounded perfect FIFO channels (i.e., FIFO systems) arise naturally in modeling distributed systems. Despite well-known difficulties in analyzing such systems, they are of...

**Structural Analysis of Boolean Equation Systems**

Jeroen J. A. Keiren, Michel A. Reniers, Tim A. C. Willemse

Article No.: 8

DOI: 10.1145/2071368.2071376

We analyze the problem of solving Boolean equation systems through the use of *structure graphs*. The latter are obtained through an elegant set of Plotkin-style deduction rules. Our main contribution is that we show that equation systems...

**The Complexity of Proving the Discrete Jordan Curve Theorem**

Phuong Nguyen, Stephen Cook

Article No.: 9

DOI: 10.1145/2071368.2071377

The Jordan curve theorem (JCT) states that a simple closed curve divides the plane into exactly two connected regions. We formalize and prove the theorem in the context of grid graphs, under different input settings, in theories of bounded...