Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories

• URL: http://arxiv.org/abs/2402.03164v1
• Date: Mon, 5 Feb 2024 16:32:12 GMT
• Title: Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories
• Authors: Till Hofmann, Stefan Schupp, Gerhard Lakemeyer
• Abstract summary: Most commonly used approach represents time by adding a real-valued fluent $mathittime(a)$ that attaches a time point to each action and consequently to each situation. We show that in this approach, checking whether there is a reachable situation that satisfies a given formula is undecidable, even if the domain of discourse is restricted to a finite set of objects.
• Score: 9.45355418401911
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Representing time is crucial for cyber-physical systems and has been studied extensively in the Situation Calculus. The most commonly used approach represents time by adding a real-valued fluent $\mathit{time}(a)$ that attaches a time point to each action and consequently to each situation. We show that in this approach, checking whether there is a reachable situation that satisfies a given formula is undecidable, even if the domain of discourse is restricted to a finite set of objects. We present an alternative approach based on well-established results from timed automata theory by introducing clocks as real-valued fluents with restricted successor state axioms and comparison operators. %that only allow comparisons against fixed rationals. With this restriction, we can show that the reachability problem for finite-domain basic action theories is decidable. Finally, we apply our results on Golog program realization by presenting a decidable procedure for determining an action sequence that is a successful execution of a given program.

Related papers

• Bisimulation Learning [55.859538562698496]
  We compute finite bisimulations of state transition systems with large, possibly infinite state space. Our technique yields faster verification results than alternative state-of-the-art tools in practice.
  arXiv  Detail & Related papers  (2024-05-24T17:11:27Z)
• Online POMDP Planning with Anytime Deterministic Guarantees [11.157761902108692]
  Planning under uncertainty can be mathematically formalized using partially observable Markov decision processes (POMDPs) Finding an optimal plan for POMDPs can be computationally expensive and is feasible only for small tasks. We derive a deterministic relationship between a simplified solution that is easier to obtain and the theoretically optimal one.
  arXiv  Detail & Related papers  (2023-10-03T04:40:38Z)
• Multi-Armed Bandits with Generalized Temporally-Partitioned Rewards [0.4194295877935867]
  In some real-world applications, feedback about a decision is delayed and may arrive via partial rewards that are observed with different delays. We propose a novel problem formulation called multi-armed bandits with generalized temporally-partitioned rewards. We derive a lower bound on the performance of any uniformly efficient algorithm for the considered problem.
  arXiv  Detail & Related papers  (2023-03-01T16:22:22Z)
• Optimisation of time-ordered processes in the finite and asymptotic regime [0.0]
  Many problems in quantum information theory can be formulated as optimizations over the sequential outcomes of dynamical systems. In this work, we introduce tractable relaxations of this class of optimization problems. We show that the maximum score of a sequential problem in the limit of infinitely many time steps is in general incomputable.
  arXiv  Detail & Related papers  (2023-02-06T16:47:24Z)
• Functional Generalized Empirical Likelihood Estimation for Conditional Moment Restrictions [19.39005034948997]
  We propose a new estimation method based on generalized empirical likelihood (GEL) GEL provides a more general framework and has been shown to enjoy favorable small-sample properties compared to GMM-based estimators. We provide kernel- and neural network-based implementations of the estimator, which achieve state-of-the-art empirical performance on two conditional moment restriction problems.
  arXiv  Detail & Related papers  (2022-07-11T11:02:52Z)
• Multi-Agent Reinforcement Learning with Temporal Logic Specifications [65.79056365594654]
  We study the problem of learning to satisfy temporal logic specifications with a group of agents in an unknown environment. We develop the first multi-agent reinforcement learning technique for temporal logic specifications. We provide correctness and convergence guarantees for our main algorithm.
  arXiv  Detail & Related papers  (2021-02-01T01:13:03Z)
• The Variational Method of Moments [65.91730154730905]
  conditional moment problem is a powerful formulation for describing structural causal parameters in terms of observables. Motivated by a variational minimax reformulation of OWGMM, we define a very general class of estimators for the conditional moment problem. We provide algorithms for valid statistical inference based on the same kind of variational reformulations.
  arXiv  Detail & Related papers  (2020-12-17T07:21:06Z)
• Learning Implicitly with Noisy Data in Linear Arithmetic [94.66549436482306]
  We extend implicit learning in PAC-Semantics to handle intervals and threshold uncertainty in the language of linear arithmetic. We show that our implicit approach to learning optimal linear programming objective constraints significantly outperforms an explicit approach in practice.
  arXiv  Detail & Related papers  (2020-10-23T19:08:46Z)
• Temporal Answer Set Programming [3.263632801414296]
  We present an overview on Temporal Logic Programming under the perspective of its application for Knowledge Representation and declarative problem solving. We focus on recent results of the non-monotonic formalism called Temporal Equilibrium Logic (TEL) that is defined for the full syntax. In a second part, we focus on practical aspects, defining a syntactic fragment called temporal logic programs closer to ASP, and explain how this has been exploited in the construction of the solver TELINGO.
  arXiv  Detail & Related papers  (2020-09-14T16:13:36Z)
• Time-varying Gaussian Process Bandit Optimization with Non-constant Evaluation Time [93.6788993843846]
  We propose a novel time-varying Bayesian optimization algorithm that can effectively handle the non-constant evaluation time. Our bound elucidates that a pattern of the evaluation time sequence can hugely affect the difficulty of the problem.
  arXiv  Detail & Related papers  (2020-03-10T13:28:33Z)
• Polynomial-Time Exact MAP Inference on Discrete Models with Global Dependencies [83.05591911173332]
  junction tree algorithm is the most general solution for exact MAP inference with run-time guarantees. We propose a new graph transformation technique via node cloning which ensures a run-time for solving our target problem independently of the form of a corresponding clique tree.
  arXiv  Detail & Related papers  (2019-12-27T13:30:29Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.