Search

• < Previous
• 1
• Next >

---

Two Variable vs. Linear Temporal Logic in Model Checking and Games

Michael Benedikt ; Rastislav Lenhardt ; James Worrell.

Model checking linear-time properties expressed in first-order logic has non-elementary complexity, and thus various restricted logical languages are employed. In this paper we consider two such restricted specification logics, linear temporal logic (LTL) and two-variable first-order logic (FO2).&nbsp;[&hellip;]

---

Definability and Interpolation within Decidable Fixpoint Logics

Michael Benedikt ; Pierre Bourhis ; Michael Vanden Boom.

We look at characterizing which formulas are expressible in rich decidable logics such as guarded fixpoint logic, unary negation fixpoint logic, and guarded negation fixpoint logic. We consider semantic characterizations of definability, as well as effective characterizations. Our algorithms revolve&nbsp;[&hellip;]

---

When Can We Answer Queries Using Result-Bounded Data Interfaces?

Antoine Amarilli ; Michael Benedikt.

We consider answering queries on data available through access methods, that provide lookup access to the tuples matching a given binding. Such interfaces are common on the Web; further, they often have bounds on how many results they can return, e.g., because of pagination or rate limits. We thus&nbsp;[&hellip;]

---

Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory

Michael Benedikt ; Cécilia Pradic ; Christoph Wernhard.

Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset O in terms of datasets I) is a logical specification involving two distinguished sets of relational symbols. One set of relations is for the "source data" I, and the other is for the "interface data" O. Such&nbsp;[&hellip;]

---