Checking Dynamic Consistency of Conditional Hyper Temporal Networks via Mean Payoff Games

Conditional Simple Temporal Network (CSTN) is a constraint-based graph-formalism for conditional temporal planning. It offers a more flexible formalism than the equivalent CSTP model of [Tsamardinos, et. al, 2003], from which it was derived mainly as a sound formalization. Three notions of consistency arise for CSTNs: weak, strong, and dynamic. Dynamic consistency is the most interesting notion, but it is also the most challenging and it was conjectured to be hard to assess. [Tsamardinos, et. al, 2003] gave a doubly-exponential time algorithm for checking dynamic consistency in CSTNs and to produce an exponentially sized dynamic execution strategy whenever the input CSTN is dynamically-consistent. CSTNs may be viewed as an extension of Simple Temporal Networks (STNs) [Dechter, et al. 1991], directed weighted graphs where nodes represent events to be scheduled in time and arcs represent temporal distance constraints between pairs of events. Recently, STNs have been generalized into Hyper Temporal Networks (HyTNs), by considering weighted directed hypergraphs where each hyperarc models a disjunctive temporal constraint named hyperconstraint; being directed, the hyperarcs can be either multi-head or multi-tail. The computational equivalence between checking consistency in HTNs and determining winning regions in Mean Payoff Games (MPGs) was also pointed out; MPGs are a family of 2-player infinite pebble games played on finite graphs, which is well known for having applications in model-checking and formal verification. In this work we introduce the Conditional Hyper Temporal Network (CHyTN) model, a natural extension and generalization of both the CSTN and the HyTN model which is obtained by blending them together. We show that deciding whether a given CSTN or CHyTN is dynamically-consistent is coNP-hard; and 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 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 CSTNs are a special case of CHyTNs, as a byproduct this provides 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 CHyTNs and MPGs; due to the existence of efficient pseudo-polynomial time algorithms for MPGs, it is quite promising to be competitive in practice. The presentation of such connection is mediated by the HyTN model. In order to analyze the time complexity of 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 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.

Download: manuscript.


Linear Time Algorithm for Update Games via Strongly-Trap-Connected Components

In the construction of reactive systems, like communication protocols or control systems, a central aim is to put the synthesis and the verification of hardware and software on a mathematical basis which is both firm and practical. A characteristic feature of such systems is their perpetual interaction with the environment as well as their non-terminating behaviour. The theory of infinite duration games offers many appealing results under this prospect [see e.g. Automata, Logics and Infinite Games: a Guide to Current Research. Gradel, Thomas, Wilke (2004)].

For instance, consider the following communication network problem. Suppose we have data stored on each node of a network and we want to continuously update all nodes with consistent data: often one requirement is to share key information between all nodes of a network; this can be done by having a data packet of current information continuously going through all nodes. Unfortunately not all routing choices are always under our control, some of them may be controlled by the network environment, which could play against us. This is essentially an infinite 2-player pebble game played on an arena, i.e. a finite directed simple graph in which the vertices are divided into two classes, V_{\square} and V_{\bigcirc}, where Player \square wants to visit all vertices infinitely often by moving the pebble on them, while Player \bigcirc works against. This is called Update Game (UG) in [Dinneen and Khoussainov (1999)].

In this work, we introduce and study a refined notion of reachability for arenas, named trap-reachability, where Player \square attempts to reach vertices without leaving a prescribed subset U\subseteq V, while Player \bigcirc works against. It is shown that every arena decomposes into strongly-trap-connected components (STCCs).
Our main result is a linear time algorithm for computing this unique decomposition.
Both the graph structures and the algorithm generalize the classical decomposition of a directed graph into its strongly-connected components (SCCs). The algorithm builds on a generalization of the depth-first search (DFS), taking inspiration from Tarjan’s SCCs classical algorithm. The structures of palm-trees and jungles described in Tarjan’s original paper need to be revisited and generalized (i.e. tr-palm-trees and tr-jungles) in order to handle the 2-player infinite pebble game’s setting.

This theory has direct applications in solving Update Games (UGs) faster. Dinneen and Khoussainov showed in 1999 that deciding who’s the winner in a given UG costs O(mn) time, where n is the number of vertices and m is that of arcs. We solve that problem in \Theta(m+n) linear time. The result is obtained by observing that the UG is a win for Player \square if and only if the arena comprises one single STCC. It is also observed that the tr-palm-tree returned by the algorithm encodes routing information that an \Theta(n)-space agent can consult to win the UG in O(1) time per move. With this, the polynomial-time complexity for deciding Explicit McNaughton-Muller Games is also improved, from cubic to quadratic.

Download: manuscript, presentation.


Faster O(|V|²|E|W)-Time Energy Algorithms for Optimal Strategy Synthesis in Mean Payoff Games

This study strengthens the links between Mean Payoff Games (MPGs) and Energy Games (EGs). Firstly, we offer a faster O(|V|^2|E|W) pseudo-polynomial time and \Theta(|V|+|E|) space deterministic algorithm for solving the Value Problem and Optimal Strategy Synthesis in MPGs. This improves the best previously known estimates on the pseudo-polynomial time complexity to:
O(|E|\log |V|) + \Theta\Big(\sum_{v\in V}\texttt{deg}_{\Gamma}(v)\cdot\ell_{\Gamma}(v)\Big) = O(|V|^2|E|W),
where \ell_{\Gamma}(v) counts the number of times that a certain energy-lifting operator \delta(\cdot, v) is applied to any v\in V, along a certain sequence of Value-Iterations on reweighted EGs; and \texttt{deg}_{\Gamma}(v) is the degree of v. This improves significantly over a previously known pseudo-polynomial time estimate, i.e. \Theta\big(|V|^2|E|W + \sum_{v\in V}\texttt{deg}_{\Gamma}(v)\cdot\ell_{\Gamma}(v)\big), as the pseudo-polynomiality is now confined to depend solely on \ell_\Gamma. Secondly, we further explore on the relationship between Optimal Positional Strategies (OPSs) in MPGs and Small Energy-Progress Measures (SEPMs) in reweighted EGs. It is observed that the space of all OPSs, \texttt{opt}_{\Gamma}\Sigma^M_0, admits a unique complete decomposition in terms of extremal-SEPMs in reweighted EGs. This points out what we called the “Energy-Lattice \mathcal{X}^*_{\Gamma} associated to \texttt{opt}_{\Gamma}\Sigma^M_0“. Finally, it is offered a pseudo-polynomial total-time recursive procedure for enumerating (w/o repetitions) all the elements of \mathcal{X}^*_{\Gamma}, and for computing the corresponding partitioning of \texttt{opt}_{\Gamma}\Sigma^M_0.

Download: manuscript.


Instantaneous Reaction-Time in Dynamic-Consistency Checking of Conditional Simple Temporal Networks @ TIME2016

Our Paper “Instantaneous Reaction-Time in Dynamic-Consistency Checking of Conditional Simple Temporal Networks” was accepted to the “23rd International Symposium on Temporal Representation and Reasoning (TIME2016)“.

TIME2016 was held at Technical University of Denmark (DTU), Copenhagen, Denmark (October 17-18-19, 2016).

This is a joint work with M. Cairo and R. Rizzi.
Pre-print link: paper, presentation.


Sorting with Forbidden Intermediates

Our Paper “Sorting with Forbidden Intermediates (On (s,t)-Paths with Forbidden Vertices in Hypercube Graphs)”

has been accepted to the “3rd International Conference on Algorithms for Computational Biology (AlCoB2016), Trujillo, Spain, June 21-22, 2016.”

AlCoB2016 was held at Extremadura Centre for Advanced Technologies (CETA-CIEMAT), located at Trujillo, Spain, street Sola no. 1 (Conventual de San Francisco), June 21-22, 2016.

This is a joint work with Anthony Labarre, Romeo Rizzi, Stéphane Vialette.

Pre-print link: manuscript, presentation.