Just a personal rephrase of JONATHAN LEWIN’s simple proof of the Zorn Lemma, which I would really like to remember… so let’s work out all the details…
(… The proof is simple in the sense that it needs neither transfinite induction, nor Ordinals, just the Axiom of Choice (AC) and elementary extremality arguments …)
Theorem (Zorn’s Lemma). Suppose is a partial order in which every chain is bounded from above. Then has a maximal element.
Def. If is a chain (i.e. total order) and , then is named the initial segment of in .
Proof. Suppose has no maximal element, towards a contradiction. If is any chain in , let be an upper bound of . Since has no maximal element, there exists such that . So, admits a strict upper bound. By AC, there is a choice function which assigns to every chain a strict upper bound .
The sought contradiction will be that of finding a chain such that . This is catalysed by the following notion of conforming subset.
Def. Say that a subset is conforming if the following two conditions hold:
- is a well order (i.e. is a chain such that every subset of has a least element);
- for every , it holds .
Comparability Lemma. If are conforming and , then one of these two sets is an initial segment of the other.
Proof of Comparability Lemma. Since we can assume w.l.o.g. .
Then . So the Claim reduces to show .
Towards a contradiction, assume .
Closure Lemma. Given any , if and then:
- (by definition of and )
- (since , so by definition of , thus too, and by definition of )
With this, we can show that . Indeed, follows already by definition of , so the actual claim is that . Let , then (by def. of ), so ; also (by def. of ); finally, it is not possible that , otherwise by Closure Lemma it would be against own definition. Therefore, . Since and , then .
Also, . Indeed, (by definition) so but , therefore (by definition of at this point).
Since , and since , we cannot have (because by definition). Therefore, , and we conclude , against definition of .
This implies that , i.e. , closing the proof of the Comparability Lemma.
By the Comparability Lemma, it is clear that the union of all conforming subsets of is conforming. Thus, if is a strict upper bound, then is conforming too. Since is the union of all conforming sets, then , contradicting that is a strict upper bound of .
So has one maximal element.
These days an extended version of our paper “Instantaneous Reaction-Time in Dynamic-Consistency Checking of Conditional Simple Temporal Networks” has been accepted for publication (to appear during March 2020, https://doi.org/10.1016/j.jlamp.2020.100542) in:
Joint work with Massimo Cairo and Romeo Rizzi (Dept. of Computer Science, University of Verona, Italy)
An extended version of our paper “Sorting with Forbidden Intermediates (Searching (s,t)-Paths avoiding Forbidden Vertices in Hypercube Graphs)” has been accepted for publication in international journal (https://doi.org/10.1016/j.dam.2019.10.025):
(journal of combinatorial algorithms, informatics and computational sciences).
Joint work with Stéphane Vialette (CNRS and UPEM, Paris, France), Anthony Labarre (UPEM, Paris, France) and Romeo Rizzi (Univ. Verona, Italy).
An alternating graph is a directed graph whose vertex set is partitioned into two classes, existential and universal. This forms the basic arena for a plethora of infinite duration two-player games where Player and alternate in a turn-based sliding of a pebble along the arcs they control.
We study alternating strongly-connectedness as a generalization of strongly-connectedness in directed graphs, aiming at providing a linear time decomposition and a sound structural graph characterization. For this a refined notion of alternating reachability is introduced: Player attempts to reach vertices without leaving a prescribed subset of the vertices, while Player works against. This is named safe alternating reachability. It is shown that every arena uniquely decomposes into safe alternating strongly-connected components where Player can visit each vertex within a given component infinitely often, without having to ever leave out the component itself.
Our main result is a linear time algorithm for computing this alternating graph decomposition.
Both the underlying graph structures and the algorithm generalize the classical decomposition of a directed graph into strongly-connected components.
The algorithm builds on a linear time generalization of the depth-first search on alternation, taking inspiration from Tarjan 1972 machinery.
Our theory has direct applications in faster solving well-known infinite duration pebble games. Dinneen and Khoussainov showed in 1999 that deciding a given Update Game costs time, where is the number of vertices and is that of arcs. We solve that task in linear time. With this the complexity of Explicit McNaughton-Muller Games also improves from cubic to quadratic.
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 October 2018.
Joint work with Romeo Rizzi (Dept. of Computer Science, University of Verona, Italy).
Uavpal-disco4g and uavpal-beboptwo4g are software modifications for the Parrot Disco and Bebop2 french 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.
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).
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, tested on sc2p-firmware v1.0.3 and v1.0.5)
UPDATE (30/12/2018): SoftIce (uavpal’s maintainer) has finally merged my code supporting SC2P with the master-branch! Please find the patch below.
Ready take off
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 of time-point variables, and a finite set of temporal constraints where each of them can be either one of the following three types: () , for real (a simple temporal difference-constraint);
() , for reals (a single-variable disjunction of many interval-constraints);
() , for 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 and -constraints (and no -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 -constraints and either only multi-tail or only multi-head hyperarc-constraints lies in and it admits deterministic pseudo-polynomial time algorithms; on the other hand, problems having only -constraints and either only multi-tail or only multi-head hyperarc-constraints are strongly NP-complete.
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.
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.