A paper at TIME2018

Our paper,

On Restricted Disjunctive Temporal Problems: Faster Algorithms and Tractability Frontier,

has been accepted for publication at the 25th International Symposium on Temporal Representation and Reasoning (TIME 2018), to be held at Institute of Computer Science, Polish Academy of Sciences, Warsaw, Poland, 15-17 September 2018.

This is a joint work with Romeo Rizzi (Dept. of Computer Science, University of Verona, Italy)


Porting uavpal 4G/LTE soft_mod to the SkyController2P

Uavpal-disco4g and uavpal-beboptwo4g are software modifications for the Parrot Disco and Bebop2 french flag-3d-round-250 drones. Instead of the built-in regular wifi, the mod allows you to switch on a 4G/LTE cellular/mobile network connection to link the SkyController2 (SC2) to the flying drone 🙂 Control/telemetry and live video stream are routed through the 4G/LTE connection.


The soft mod is currently maintained by its original creator Marc B. (a.k.a. “softice”); it is a cheap, non-intrusive, rock solid and very enjoyable clever mod. It just works. However, the newest version of the Parrot SC2 — namely, the SkyController2P (SC2P) (the one having black plastic joysticks) — was not supported, not yet.buttons

I’ve succeeded at porting Marc’s original soft_mod to the SC2P. Here below you can find the corresponding complete shell script (if you have a SC2P, just replace or patch the original file uavpal_sc2.sh). If you see what I mean at this point, it will be easy to do 🙂

I wish to thank Marc for all of his great work, and for helpful discussions and advices which finally led me to code the following patch.

Experimental. Take off and fly at your own risk.

Download: uavpal_sc2.sh (script for the SkyController2P only)

On Restricted Disjunctive Temporal Problems: Faster Algorithms and Tractability Frontier.

In 2005 T.K.S. Kumar studied the Restricted Disjunctive Temporal Problem (RDTP), a restricted but very expressive class of Disjunctive Temporal Problems (DTPs). An RDTP comes with a finite set \mathcal{T}=\{X,Y,\ldots\} of time-point variables, and a finite set \mathcal{C} of temporal constraints where each of them can be either one of the following three types: (\texttt{t}_1) (Y-X\leq w), for w real (a simple temporal difference-constraint);
(\texttt{t}_2) (l_1\leq X\leq u_1)\vee \cdots \vee (l_k\leq X\leq u_k), for l_i,u_i reals (a single-variable disjunction of many interval-constraints);
(\texttt{t}_3) (l_1\leq X\leq u_1) \vee (l_2\leq Y\leq u_2), for l_i,u_i reals (a two-variable disjunction of two interval-constraints only).
Kumar showed that RDTPs are solvable in deterministic strongly-polynomial time by reducing them to the Connected Row-Convex (CRC) constraints problem; plus, he devised a randomized algorithm whose expected running time is less than that of the deterministic one. Instead, the most general form of DTPs allows for multi-variable disjunctions of many interval constraints and it is NP-complete.

This work offers a deeper comprehension on the tractability of RDTPs, leading to an elementary deterministic strongly-polynomial time algorithm for solving them,
significantly improving the asymptotic running times of all the previous deterministic and randomized algorithms. The result is obtained by reducing RDTPs to the Single-Source Shortest-Paths (SSSP) and the 2-SAT problem (jointly), instead of reducing to CRCs. In passing, we obtain a faster (quadratic time) algorithm for RDTPs having only \texttt{t}_1 and \texttt{t}_2-constraints (and no \texttt{t}_3-constraint).
As a second main contribution, we study the tractability frontier of solving RDTPs blended with Hyper Temporal Networks (HyTNs), a strict generalization of Simple Temporal Networks (STNs) grounded on hypergraphs: we prove that solving temporal problems having only \texttt{t}_2-constraints and either only multi-tail or only multi-head hyperarc-constraints lies in \text{NP}\cap \text{co-NP} and it admits deterministic pseudo-polynomial time algorithms; on the other hand, problems having only \texttt{t}_3-constraints and either only multi-tail or only multi-head hyperarc-constraints are strongly NP-complete.

Download: manuscript.


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.

PhD Thesis

My PhD Thesis,

Complexity in Infinite Games on Graphs and Temporal Constraint Networks,

has been defended on 20 March 2017 (University of Trento and Université Paris-Est Marne la Vallée).  Final Grade: Excellent, cum Laude.

Download: manuscript, presentation.

Final Examination Committee: Prof. Luke Hunsberger (Vassar College, Poughkeepsie, NY, USA), Prof. Romeo Rizzi (Univ. Verona, IT), DdR2 Stéphane Vialette (Univ. Paris-Est, FR), Dr. Zsuzsanna Lipták (Univ. Verona, IT), Prof. Angelo Montanari (Univ. Udine, IT)


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.