Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Metric Temporal Equilibrium Logic over Timed Traces

Arvid Becker, Pedro Cabalar, Martín Diéguez, Torsten Schaub, Anna Schuhmann

TL;DR

This work defines a translation of metric formulas into monadic first-order formulas and gives a correspondence between their models in MEL and Monadic Quantified Equilibrium Logic, respectively, which provides a blue print for implementation in terms of ASP modulo difference constraints.

Abstract

In temporal extensions of Answer Set Programming (ASP) based on linear-time, the behavior of dynamic systems is captured by sequences of states. While this representation reflects their relative order, it abstracts away the specific times associated with each state. However, timing constraints are important in many applications like, for instance, when planning and scheduling go hand in hand. We address this by developing a metric extension of linear-time temporal equilibrium logic, in which temporal operators are constrained by intervals over natural numbers. The resulting Metric Equilibrium Logic provides the foundation of an ASP-based approach for specifying qualitative and quantitative dynamic constraints. To this end, we define a translation of metric formulas into monadic first-order formulas and give a correspondence between their models in Metric Equilibrium Logic and Monadic Quantified Equilibrium Logic, respectively. Interestingly, our translation provides a blue print for implementation in terms of ASP modulo difference constraints.

Metric Temporal Equilibrium Logic over Timed Traces

TL;DR

This work defines a translation of metric formulas into monadic first-order formulas and gives a correspondence between their models in MEL and Monadic Quantified Equilibrium Logic, respectively, which provides a blue print for implementation in terms of ASP modulo difference constraints.

Abstract

In temporal extensions of Answer Set Programming (ASP) based on linear-time, the behavior of dynamic systems is captured by sequences of states. While this representation reflects their relative order, it abstracts away the specific times associated with each state. However, timing constraints are important in many applications like, for instance, when planning and scheduling go hand in hand. We address this by developing a metric extension of linear-time temporal equilibrium logic, in which temporal operators are constrained by intervals over natural numbers. The resulting Metric Equilibrium Logic provides the foundation of an ASP-based approach for specifying qualitative and quantitative dynamic constraints. To this end, we define a translation of metric formulas into monadic first-order formulas and give a correspondence between their models in Metric Equilibrium Logic and Monadic Quantified Equilibrium Logic, respectively. Interestingly, our translation provides a blue print for implementation in terms of ASP modulo difference constraints.
Paper Structure (12 sections, 23 theorems, 43 equations)

This paper contains 12 sections, 23 theorems, 43 equations.

Table of Contents

  1. Introduction
  2. Metric Logic of Here-and-There
  3. Metric Equilibrium Logic
  4. Translation into Monadic Quantified Here-and-There with Difference Constraints
  5. Related Work
  6. Conclusion
  7. Acknowledgments
  8. Competing interests
  9. Proofs
  10. Base case
  11. Inductive case: propositional connectives
  12. Inductive case: metric temporal operators

Key Result

Proposition 1

Let $\mathbf{M}=(\langle \mathbf{H},\mathbf{T} \rangle,\tau)$ be a timed $\mathrm{HT}$-trace of length $\lambda$ over $\mathcal{A}$. Given the respective definitions of derived operators, we get the following satisfaction conditions:

Theorems & Definitions (30)

  • Definition 1
  • Definition 2: $\mathrm{MHT}$-satisfaction
  • Proposition 1
  • Proposition 2
  • Proposition 3: Persistence
  • Corollary 1: Decidability of $\mathrm{MHT}_{\!f}$
  • Proposition 4
  • Definition 3: Temporal Excluded Middle
  • Proposition 5
  • Corollary 2
  • ...and 20 more