Search

• < Previous
• 1
• Next >

---

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;]

---

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;]

---