Checking Dynamic Consistency of Conditional Hyper Temporal Networks via Mean Payoff Games (Hardness and (pseudo) Singly-Exponential Time Algorithm)

TL;DR

This paper introduces the Conditional Hyper Temporal Network (CHyTN) model, analyzes its dynamic consistency complexity, and presents a pseudo singly-exponential time algorithm based on Mean Payoff Games, improving verification methods.

Contribution

It establishes the hardness of dynamic consistency checking for CHyTNs and provides the first deterministic pseudo singly-exponential algorithm for certain cases, connecting CHyTNs with Mean Payoff Games.

Findings

Deciding dynamic consistency of CHyTNs is ext{coNP}-hard.

Deciding dynamic consistency with multi-head or multi-tail hyperarcs is ext{PSPACE}-hard.

A pseudo singly-exponential time algorithm for checking dynamic consistency of specific CHyTNs.

Abstract

In this work we introduce the \emph{Conditional Hyper Temporal Network (CHyTN)} model, which is a natural extension and generalization of both the \CSTN and the \HTN model. Our contribution goes as follows. We show that deciding whether a given \CSTN or CHyTN is dynamically consistent is \coNP-hard. Then, we offer a proof that deciding whether a given CHyTN is dynamically consistent is \PSPACE-hard, provided that the input instances are allowed to include both multi-head and multi-tail hyperarcs. In light of this, we continue our study by focusing on CHyTNs that allow only multi-head or only multi-tail hyperarcs, and we offer the first deterministic (pseudo) singly-exponential time algorithm for the problem of checking the dynamic-consistency of such CHyTNs, also producing a dynamic execution strategy whenever the input CHyTN is dynamically consistent. Since \CSTN{s} are a special case of CHyTNs, this provides as a byproduct the first sound-and-complete (pseudo) singly-exponential time algorithm for checking dynamic-consistency in CSTNs. The proposed algorithm is based on a novel connection between CSTN{s}/CHyTN{s} and Mean Payoff Games. The presentation of the connection between \CSTN{s}/CHyTNs and \MPG{s} is mediated by the \HTN model. In order to analyze the algorithm, we introduce a refined notion of dynamic-consistency, named $\epsilon$-dynamic-consistency, and present a sharp lower bounding analysis on the critical value of the reaction time $\hat{\varepsilon}$ where a \CSTN/CHyTN transits from being, to not being, dynamically consistent. The proof technique introduced in this analysis of $\hat{\varepsilon}$ is applicable more generally when dealing with linear difference constraints which include strict inequalities.