Energy Games Solver-v0.1

Today I propose a new tool, Energy Games Solver-v0.1 (written in C/C++). It allows to solve the Minimum Credit Problem in Energy Games. It implements both the Value Iteration Algorithm of Brim et al. and the Keep Alive Strategy Improvement Algorithm of Brim and Chaloupka.

Download: EGS-v0.1.


A paper at TIME 2017

Our paper,

Incorporating Decision Nodes into Conditional Simple Temporal Networks

has been accepted at TIME 2017, to be held at Université de Mons, Belgium, Oct. 2017.

Abstract. A Conditional Simple Temporal Network (CSTN) is an extension of Simple Temporal Network (STN) having some special time-points, named observation time-points. In a STN/CSTN, the agent executing the network controls the execution of every time-point. Observation time-points have unique propositional letters associated with them and, when the agent executes one of them, the environment assigns a truth value to the corresponding propositional letter. Thus, the agent observes, but does not control, the assignment of truth values. A CSTN is dynamically consistent (DC) if there exists a strategy for executing its time-points such that all relevant constraints will be satisfied no matter which truth values the environment assigns to the propositional letters.

Alternatively, in a Labeled Simple Temporal Network (Labeled STN)—also called a Temporal Plan with Choice—the agent executing the network completely controls the process of assigning values to the so-called choice variables. Furthermore, the agent can make those assignments at any time.  For this reason, a Labeled STN is equivalent to a Disjunctive Temporal Network. A generalisation of the Bellman-Ford algorithm to accommodate the propagation of labeled values has been used to determine whether any given Labeled STN is consistent.

This paper incorporates both of the above extensions by augmenting a CSTN to include not only observation time-points, but also decision time-points. A decision time-point is like an observation time-point in that it has an associated propositional letter whose value is determined when the decision time-point is executed.  It differs in that the agent (not the environment) selects that value.  The resulting network is called a CSTN with Decisions (CSTND). This paper shows that a CSTND generalizes both CSTNs and Labeled STNs. It proves that the decision problem of determining whether or not any CSTND is dynamically consistent is PSPACE-complete. And it  presents algorithms that restrict attention to two special classes of CSTNDs: (i) those that contain only decision time-points; and (ii) those in which all decisions are made before starting to execute the network.

Download: paper.

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.