Showing 1–34 of 34 results for author: Parys, P

Extending the WMSO+U Logic With Quantification Over Tuples

Authors: Anita Badyl, Paweł Parys

Abstract: We study a new extension of the weak MSO logic, talking about boundedness. Instead of a previously considered quantifier U, expressing the fact that there exist arbitrarily large finite sets satisfying a given property, we consider a generalized quantifier U, expressing the fact that there exist tuples of arbitrarily large finite sets satisfying a given property. First, we prove that the new logic… ▽ More We study a new extension of the weak MSO logic, talking about boundedness. Instead of a previously considered quantifier U, expressing the fact that there exist arbitrarily large finite sets satisfying a given property, we consider a generalized quantifier U, expressing the fact that there exist tuples of arbitrarily large finite sets satisfying a given property. First, we prove that the new logic WMSO+U_tup is strictly more expressive than WMSO+U. In particular, WMSO+U_tup is able to express the so-called simultaneous unboundedness property, for which we prove that it is not expressible in WMSO+U. Second, we prove that it is decidable whether the tree generated by a given higher-order recursion scheme satisfies a given sentence of WMSO+K_tup. △ Less

Submitted 28 November, 2023; originally announced November 2023.

Comments: This is an extended version of a paper published at the CSL 2024 conference

Energy-optimal Timetable Design for Sustainable Metro Railway Networks

Authors: Shuvomoy Das Gupta, Bart P. G. Van Parys, J. Kevin Tobin

Abstract: We present our collaboration with Thales Canada Inc, the largest provider of communication-based train control (CBTC) systems worldwide. We study the problem of designing energy-optimal timetables in metro railway networks to minimize the effective energy consumption of the network, which corresponds to simultaneously minimizing total energy consumed by all the trains and maximizing the transfer o… ▽ More We present our collaboration with Thales Canada Inc, the largest provider of communication-based train control (CBTC) systems worldwide. We study the problem of designing energy-optimal timetables in metro railway networks to minimize the effective energy consumption of the network, which corresponds to simultaneously minimizing total energy consumed by all the trains and maximizing the transfer of regenerative braking energy from suitable braking trains to accelerating trains. We propose a novel data-driven linear programming model that minimizes the total effective energy consumption in a metro railway network, capable of computing the optimal timetable in real-time, even for some of the largest CBTC systems in the world. In contrast with existing works, which are either NP-hard or involve multiple stages requiring extensive simulation, our model is a single linear programming model capable of computing the energy-optimal timetable subject to the constraints present in the railway network. Furthermore, our model can predict the total energy consumption of the network without requiring time-consuming simulations, making it suitable for widespread use in managerial settings. We apply our model to Shanghai Railway Network's Metro Line 8 -- one of the largest and busiest railway services in the world -- and empirically demonstrate that our model computes energy-optimal timetables for thousands of active trains spanning an entire service period of one day in real-time (solution time less than one second on a standard desktop), achieving energy savings between approximately 20.93% and 28.68%. Given the compelling advantages, our model is in the process of being integrated into Thales Canada Inc's industrial timetable compiler. △ Less

Submitted 2 January, 2024; v1 submitted 11 September, 2023; originally announced September 2023.

Comments: 22 pages, 8 figures, 2 tables

Smoothed $f$-Divergence Distributionally Robust Optimization

Authors: Zhenyuan Liu, Bart P. G. Van Parys, Henry Lam

Abstract: In data-driven optimization, sample average approximation (SAA) is known to suffer from the so-called optimizer's curse that causes an over-optimistic evaluation of the solution performance. We argue that a special type of distributionallly robust optimization (DRO) formulation offers theoretical advantages in correcting for this optimizer's curse compared to simple ``margin'' adjustments to SAA a… ▽ More In data-driven optimization, sample average approximation (SAA) is known to suffer from the so-called optimizer's curse that causes an over-optimistic evaluation of the solution performance. We argue that a special type of distributionallly robust optimization (DRO) formulation offers theoretical advantages in correcting for this optimizer's curse compared to simple ``margin'' adjustments to SAA and other DRO approaches: It attains a statistical bound on the out-of-sample performance, for a wide class of objective functions and distributions, that is nearly tightest in terms of exponential decay rate. This DRO uses an ambiguity set based on a Kullback Leibler (KL) divergence smoothed by the Wasserstein or Lévy-Prokhorov (LP) distance via a suitable distance optimization. Computationally, we also show that such a DRO, and its generalized versions using smoothed $f$-divergence, are not harder than DRO problems based on $f$-divergence or Wasserstein distances, rendering our DRO formulations both statistically optimal and computationally viable. △ Less

Submitted 12 October, 2023; v1 submitted 24 June, 2023; originally announced June 2023.

MSC Class: 90C15; 90C17; 90C25

Improved Complexity Analysis of Quasi-Polynomial Algorithms Solving Parity Games

Authors: Paweł Parys, Aleksander Wiącek

Abstract: We improve the complexity of solving parity games (with priorities in vertices) for $d=ω(\log n)$ by a factor of $θ(d^2)$: the best complexity known to date was $O(mdn^{1.45+\log_2(d/\log_2(n))})$, while we obtain $O(mn^{1.45+\log_2(d/\log_2(n))}/d)$, where $n$ is the number of vertices, $m$ is the number of edges, and $d$ is the number of priorities. We base our work on existing algorithms usin… ▽ More We improve the complexity of solving parity games (with priorities in vertices) for $d=ω(\log n)$ by a factor of $θ(d^2)$: the best complexity known to date was $O(mdn^{1.45+\log_2(d/\log_2(n))})$, while we obtain $O(mn^{1.45+\log_2(d/\log_2(n))}/d)$, where $n$ is the number of vertices, $m$ is the number of edges, and $d$ is the number of priorities. We base our work on existing algorithms using universal trees, and we improve their complexity. We present two independent improvements. First, an improvement by a factor of $θ(d)$ comes from a more careful analysis of the width of universal trees. Second, we perform (or rather recall) a finer analysis of requirements for a universal tree: while for solving games with priorities on edges one needs an $n$-universal tree, in the case of games with priorities in vertices it is enough to use an $n/2$-universal tree. This way, we allow to solve games of size $2n$ in the time needed previously to solve games of size $n$; such a change divides the quasi-polynomial complexity again by a factor of $θ(d)$. △ Less

Submitted 29 April, 2023; originally announced May 2023.

The Probabilistic Rabin Tree Theorem

Authors: Damian Niwiński, Paweł Parys, Michał Skrzypczak

Abstract: The Rabin tree theorem yields an algorithm to solve the satisfiability problem for monadic second-order logic over infinite trees. Here we solve the probabilistic variant of this problem. Namely, we show how to compute the probability that a randomly chosen tree satisfies a given formula. We additionally show that this probability is an algebraic number. This closes a line of research where simila… ▽ More The Rabin tree theorem yields an algorithm to solve the satisfiability problem for monadic second-order logic over infinite trees. Here we solve the probabilistic variant of this problem. Namely, we show how to compute the probability that a randomly chosen tree satisfies a given formula. We additionally show that this probability is an algebraic number. This closes a line of research where similar results were shown for formalisms weaker than the full monadic second-order logic. △ Less

Submitted 24 April, 2023; originally announced April 2023.

Unboundedness for Recursion Schemes: A Simpler Type System

Authors: David Barozzini, Paweł Parys, Jan Wróblewski

Abstract: Decidability of the problems of unboundedness and simultaneous unboundedness (aka. the diagonal problem) for higher-order recursion schemes was established by Clemente, Parys, Salvati, and Walukiewicz (2016). Then a procedure of optimal complexity was presented by Parys (2017); this procedure used a complicated type system, involving multiple flags and markers. We present here a simpler and much m… ▽ More Decidability of the problems of unboundedness and simultaneous unboundedness (aka. the diagonal problem) for higher-order recursion schemes was established by Clemente, Parys, Salvati, and Walukiewicz (2016). Then a procedure of optimal complexity was presented by Parys (2017); this procedure used a complicated type system, involving multiple flags and markers. We present here a simpler and much more intuitive type system serving the same purpose. We prove that this type system allows to solve the unboundedness problem for a widely considered subclass of recursion schemes, called safe schemes. For unsafe recursion schemes we only have soundness of the type system: if one can establish a type derivation claiming that a recursion scheme is unbounded then it is indeed unbounded. Completeness of the type system for unsafe recursion schemes is left as an open question. Going further, we discuss an extension of the type system that allows to handle the simultaneous unboundedness problem. We also design and implement an algorithm that fully automatically checks unboundedness of a given recursion scheme, completing in a short time for a wide variety of inputs. △ Less

Submitted 23 April, 2022; originally announced April 2022.

Branch-and-Bound Performance Estimation Programming: A Unified Methodology for Constructing Optimal Optimization Methods

Authors: Shuvomoy Das Gupta, Bart P. G. Van Parys, Ernest K. Ryu

Abstract: We present the Branch-and-Bound Performance Estimation Programming (BnB-PEP), a unified methodology for constructing optimal first-order methods for convex and nonconvex optimization. BnB-PEP poses the problem of finding the optimal optimization method as a nonconvex but practically tractable quadratically constrained quadratic optimization problem and solves it to certifiable global optimality us… ▽ More We present the Branch-and-Bound Performance Estimation Programming (BnB-PEP), a unified methodology for constructing optimal first-order methods for convex and nonconvex optimization. BnB-PEP poses the problem of finding the optimal optimization method as a nonconvex but practically tractable quadratically constrained quadratic optimization problem and solves it to certifiable global optimality using a customized branch-and-bound algorithm. By directly confronting the nonconvexity, BnB-PEP offers significantly more flexibility and removes the many limitations of the prior methodologies. Our customized branch-and-bound algorithm, through exploiting specific problem structures, outperforms the latest off-the-shelf implementations by orders of magnitude, accelerating the solution time from hours to seconds and weeks to minutes. We apply BnB-PEP to several setups for which the prior methodologies do not apply and obtain methods with bounds that improve upon prior state-of-the-art results. Finally, we use the BnB-PEP methodology to find proofs with potential function structures, thereby systematically generating analytical convergence proofs. △ Less

Submitted 8 June, 2023; v1 submitted 14 March, 2022; originally announced March 2022.

Comments: Published in Mathematical Programming Series A

Learning and Decision-Making with Data: Optimal Formulations and Phase Transitions

Authors: Amine Bennouna, Bart P. G. Van Parys

Abstract: We study the problem of designing optimal learning and decision-making formulations when only historical data is available. Prior work typically commits to a particular class of data-driven formulation and subsequently tries to establish out-of-sample performance guarantees. We take here the opposite approach. We define first a sensible yard stick with which to measure the quality of any data-driv… ▽ More We study the problem of designing optimal learning and decision-making formulations when only historical data is available. Prior work typically commits to a particular class of data-driven formulation and subsequently tries to establish out-of-sample performance guarantees. We take here the opposite approach. We define first a sensible yard stick with which to measure the quality of any data-driven formulation and subsequently seek to find an optimal such formulation. Informally, any data-driven formulation can be seen to balance a measure of proximity of the estimated cost to the actual cost while guaranteeing a level of out-of-sample performance. Given an acceptable level of out-of-sample performance, we construct explicitly a data-driven formulation that is uniformly closer to the true cost than any other formulation enjoying the same out-of-sample performance. We show the existence of three distinct out-of-sample performance regimes (a superexponential regime, an exponential regime and a subexponential regime) between which the nature of the optimal data-driven formulation experiences a phase transition. The optimal data-driven formulations can be interpreted as a classically robust formulation in the superexponential regime, an entropic distributionally robust formulation in the exponential regime and finally a variance penalized formulation in the subexponential regime. This final observation unveils a surprising connection between these three, at first glance seemingly unrelated, data-driven formulations which until now remained hidden. △ Less

Submitted 11 March, 2024; v1 submitted 14 September, 2021; originally announced September 2021.

Higher-Order Model Checking Step by Step

Authors: Paweł Parys

Abstract: We show a new simple algorithm that solves the model-checking problem for recursion schemes: check whether the tree generated by a given higher-order recursion scheme is accepted by a given alternating parity automaton. The algorithm amounts to a procedure that transforms a recursion scheme of order $n$ to a recursion scheme of order $n-1$, preserving acceptance, and increasing the size only expon… ▽ More We show a new simple algorithm that solves the model-checking problem for recursion schemes: check whether the tree generated by a given higher-order recursion scheme is accepted by a given alternating parity automaton. The algorithm amounts to a procedure that transforms a recursion scheme of order $n$ to a recursion scheme of order $n-1$, preserving acceptance, and increasing the size only exponentially. After repeating the procedure $n$ times, we obtain a recursion scheme of order $0$, for which the problem boils down to solving a finite parity game. Since the size grows exponentially at each step, the overall complexity is $n$-EXPTIME, which is known to be optimal. More precisely, the transformation is linear in the size of the recursion scheme, assuming that the arity of employed nonterminals and the size of the automaton are bounded by a constant; this results in an FPT algorithm for the model-checking problem. Our transformation is a generalization of a previous transformation of the author (2020), working for reachability automata in place of parity automata. The step-by-step approach can be opposed to previous algorithms solving the considered problem "in one step", being compulsorily more complicated. △ Less

Submitted 5 May, 2021; originally announced May 2021.

Comments: This is an extended version of a paper published on the ICALP 2021 conference

A Recursive Approach to Solving Parity Games in Quasipolynomial Time

Authors: Karoliina Lehtinen, Paweł Parys, Sven Schewe, Dominik Wojtczak

Abstract: Zielonka's classic recursive algorithm for solving parity games is perhaps the simplest among the many existing parity game algorithms. However, its complexity is exponential, while currently the state-of-the-art algorithms have quasipolynomial complexity. Here, we present a modification of Zielonka's classic algorithm that brings its complexity down to… ▽ More Zielonka's classic recursive algorithm for solving parity games is perhaps the simplest among the many existing parity game algorithms. However, its complexity is exponential, while currently the state-of-the-art algorithms have quasipolynomial complexity. Here, we present a modification of Zielonka's classic algorithm that brings its complexity down to $n^{O\left(\log\left(1+\frac{d}{\log n}\right)\right)}$, for parity games of size $n$ with $d$ priorities, in line with previous quasipolynomial-time solutions. △ Less

Submitted 11 January, 2022; v1 submitted 19 April, 2021; originally announced April 2021.

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 1 (January 12, 2022) lmcs:7387

Efficient Data-Driven Optimization with Noisy Data

Authors: Bart P. G. Van Parys

Abstract: Classical Kullback-Leibler or entropic distances are known to enjoy certain desirable statistical properties in the context of decision-making with noiseless data. However, in most practical situations the data available to a decision maker is subject to a certain amount of measurement noise. We hence study here data-driven prescription problems in which the data is corrupted by a known noise sour… ▽ More Classical Kullback-Leibler or entropic distances are known to enjoy certain desirable statistical properties in the context of decision-making with noiseless data. However, in most practical situations the data available to a decision maker is subject to a certain amount of measurement noise. We hence study here data-driven prescription problems in which the data is corrupted by a known noise source. We derive efficient data-driven formulations in this noisy regime and indicate that they enjoy an entropic optimal transport interpretation. Finally, we show that these efficient robust formulations are tractable in several interesting settings by exploiting a classical representation result by Strassen. △ Less

Submitted 23 February, 2024; v1 submitted 8 February, 2021; originally announced February 2021.

MSC Class: 90C15; 62C99

Exterior-point Optimization for Sparse and Low-rank Optimization

Authors: Shuvomoy Das Gupta, Bartolomeo Stellato, Bart P. G. Van Parys

Abstract: Many problems of substantial current interest in machine learning, statistics, and data science can be formulated as sparse and low-rank optimization problems. In this paper, we present the nonconvex exterior-point optimization solver NExOS -- a first-order algorithm tailored to sparse and low-rank optimization problems. We consider the problem of minimizing a convex function over a nonconvex cons… ▽ More Many problems of substantial current interest in machine learning, statistics, and data science can be formulated as sparse and low-rank optimization problems. In this paper, we present the nonconvex exterior-point optimization solver NExOS -- a first-order algorithm tailored to sparse and low-rank optimization problems. We consider the problem of minimizing a convex function over a nonconvex constraint set, where the set can be decomposed as the intersection of a compact convex set and a nonconvex set involving sparse or low-rank constraints. Unlike the convex relaxation approaches, NExOS finds a locally optimal point of the original problem by solving a sequence of penalized problems with strictly decreasing penalty parameters by exploiting the nonconvex geometry. NExOS solves each penalized problem by applying a first-order algorithm, which converges linearly to a local minimum of the corresponding penalized formulation under regularity conditions. Furthermore, the local minima of the penalized problems converge to a local minimum of the original problem as the penalty parameter goes to zero. We then implement and test NExOS on many instances from a wide variety of sparse and low-rank optimization problems, empirically demonstrating that our algorithm outperforms specialized methods. △ Less

Submitted 27 April, 2024; v1 submitted 9 November, 2020; originally announced November 2020.

Comments: Accepted for publication in the Journal of Optimization Theory and Applications

A Pareto Dominance Principle for Data-Driven Optimization

Authors: Tobias Sutter, Bart P. G. Van Parys, Daniel Kuhn

Abstract: We propose a statistically optimal approach to construct data-driven decisions for stochastic optimization problems. Fundamentally, a data-driven decision is simply a function that maps the available training data to a feasible action. It can always be expressed as the minimizer of a surrogate optimization model constructed from the data. The quality of a data-driven decision is measured by its ou… ▽ More We propose a statistically optimal approach to construct data-driven decisions for stochastic optimization problems. Fundamentally, a data-driven decision is simply a function that maps the available training data to a feasible action. It can always be expressed as the minimizer of a surrogate optimization model constructed from the data. The quality of a data-driven decision is measured by its out-of-sample risk. An additional quality measure is its out-of-sample disappointment, which we define as the probability that the out-of-sample risk exceeds the optimal value of the surrogate optimization model. An ideal data-driven decision should minimize the out-of-sample risk simultaneously with respect to every conceivable probability measure as the true measure is unkown. Unfortunately, such ideal data-driven decisions are generally unavailable. This prompts us to seek data-driven decisions that minimize the in-sample risk subject to an upper bound on the out-of-sample disappointment. We prove that such Pareto-dominant data-driven decisions exist under conditions that allow for interesting applications: the unknown data-generating probability measure must belong to a parametric ambiguity set, and the corresponding parameters must admit a sufficient statistic that satisfies a large deviation principle. We can further prove that the surrogate optimization model must be a distributionally robust optimization problem constructed from the sufficient statistic and the rate function of its large deviation principle. Hence the optimal method for map** data to decisions is to solve a distributionally robust optimization model. Maybe surprisingly, this result holds even when the training data is non-i.i.d. Our analysis reveals how the structural properties of the data-generating stochastic process impact the shape of the ambiguity set underlying the optimal distributionally robust model. △ Less

Submitted 14 December, 2023; v1 submitted 13 October, 2020; originally announced October 2020.

Comments: 55 pages

Higher-Order Nonemptiness Step by Step

Authors: Paweł Parys

Abstract: We show a new simple algorithm that checks whether a given higher-order grammar generates a nonempty language of trees. The algorithm amounts to a procedure that transforms a grammar of order n to a grammar of order n-1, preserving nonemptiness, and increasing the size only exponentially. After repeating the procedure n times, we obtain a grammar of order 0, whose nonemptiness can be easily checke… ▽ More We show a new simple algorithm that checks whether a given higher-order grammar generates a nonempty language of trees. The algorithm amounts to a procedure that transforms a grammar of order n to a grammar of order n-1, preserving nonemptiness, and increasing the size only exponentially. After repeating the procedure n times, we obtain a grammar of order 0, whose nonemptiness can be easily checked. Since the size grows exponentially at each step, the overall complexity is n-EXPTIME, which is known to be optimal. More precisely, the transformation (and hence the whole algorithm) is linear in the size of the grammar, assuming that the arity of employed nonterminals is bounded by a constant. The same algorithm allows to check whether an infinite tree generated by a higher-order recursion scheme is accepted by an alternating safety (or reachability) automaton, because this question can be reduced to the nonemptiness problem by taking a product of the recursion scheme with the automaton. A proof of correctness of the algorithm is formalised in the proof assistant Coq. Our transformation is motivated by a similar transformation of Asada and Kobayashi (2020) changing a word grammar of order n to a tree grammar of order n-1. The step-by-step approach can be opposed to previous algorithms solving the nonemptiness problem "in one step", being compulsorily more complicated. △ Less

Submitted 17 September, 2020; originally announced September 2020.

On the Expressive Power of Higher-Order Pushdown Systems

Authors: Paweł Parys

Abstract: We show that deterministic collapsible pushdown automata of second order can recognize a language that is not recognizable by any deterministic higher-order pushdown automaton (without collapse) of any order. This implies that there exists a tree generated by a second order collapsible pushdown system (equivalently, by a recursion scheme of second order) that is not generated by any deterministic… ▽ More We show that deterministic collapsible pushdown automata of second order can recognize a language that is not recognizable by any deterministic higher-order pushdown automaton (without collapse) of any order. This implies that there exists a tree generated by a second order collapsible pushdown system (equivalently, by a recursion scheme of second order) that is not generated by any deterministic higher-order pushdown system (without collapse) of any order (equivalently, by any safe recursion scheme of any order). As a side effect, we present a pum** lemma for deterministic higher-order pushdown automata, which potentially can be useful for other applications. △ Less

Submitted 19 August, 2020; v1 submitted 3 August, 2020; originally announced August 2020.

ACM Class: F.1.1

Journal ref: Logical Methods in Computer Science, Volume 16, Issue 3 (August 20, 2020) lmcs:6692

Optimal Learning for Structured Bandits

Authors: Bart P. G. Van Parys, Negin Golrezaei

Abstract: We study structured multi-armed bandits, which is the problem of online decision-making under uncertainty in the presence of structural information. In this problem, the decision-maker needs to discover the best course of action despite observing only uncertain rewards over time. The decision-maker is aware of certain convex structural information regarding the reward distributions; that is, the d… ▽ More We study structured multi-armed bandits, which is the problem of online decision-making under uncertainty in the presence of structural information. In this problem, the decision-maker needs to discover the best course of action despite observing only uncertain rewards over time. The decision-maker is aware of certain convex structural information regarding the reward distributions; that is, the decision-maker knows the reward distributions of the arms belong to a convex compact set. In the presence such structural information, they then would like to minimize their regret by exploiting this information, where the regret is its performance difference against a benchmark policy that knows the best action ahead of time. In the absence of structural information, the classical upper confidence bound (UCB) and Thomson sampling algorithms are well known to suffer minimal regret. As recently pointed out, neither algorithms are, however, capable of exploiting structural information that is commonly available in practice. We propose a novel learning algorithm that we call "DUSA" whose regret matches the information-theoretic regret lower bound up to a constant factor and can handle a wide range of structural information. Our algorithm DUSA solves a dual counterpart of the regret lower bound at the empirical reward distribution and follows its suggested play. We show that this idea leads to the first computationally viable learning policy with asymptotic minimal regret for various structural information, including well-known structured bandits such as linear, Lipschitz, and convex bandits, and novel structured bandits that have not been studied in the literature due to the lack of a unified and flexible framework. △ Less

Submitted 10 July, 2023; v1 submitted 14 July, 2020; originally announced July 2020.

Bisimulation Finiteness of Pushdown Systems Is Elementary

Authors: Stefan Göller, Paweł Parys

Abstract: We show that in case a pushdown system is bisimulation equivalent to a finite system, there is already a bisimulation equivalent finite system whose size is elementarily bounded in the description size of the pushdown system. As a consequence we obtain that it is elementarily decidable if a given pushdown system is bisimulation equivalent to some finite system. This improves a previously best-know… ▽ More We show that in case a pushdown system is bisimulation equivalent to a finite system, there is already a bisimulation equivalent finite system whose size is elementarily bounded in the description size of the pushdown system. As a consequence we obtain that it is elementarily decidable if a given pushdown system is bisimulation equivalent to some finite system. This improves a previously best-known ACKERMANN upper bound for this problem. △ Less

Submitted 13 May, 2020; originally announced May 2020.

Compositionality of the MSO+U Logic

Authors: Paweł Parys

Abstract: We prove that the MSO+U logic is compositional in the following sense: whether an MSO+U formula holds in a tree T depends only on MSO+U-definable properties of the root of T and of subtrees of T starting directly below the root. Another kind of compositionality follows: every MSO+U formula whose all free variables range only over finite sets of nodes (in particular, whose all free variables are fi… ▽ More We prove that the MSO+U logic is compositional in the following sense: whether an MSO+U formula holds in a tree T depends only on MSO+U-definable properties of the root of T and of subtrees of T starting directly below the root. Another kind of compositionality follows: every MSO+U formula whose all free variables range only over finite sets of nodes (in particular, whose all free variables are first-order) can be rewritten into an MSO formula having access to properties of subtrees definable by MSO+U sentences (without free variables). △ Less

Submitted 5 May, 2020; originally announced May 2020.

Comments: arXiv admin note: text overlap with arXiv:1810.04763

Cost Automata, Safe Schemes, and Downward Closures

Authors: David Barozzini, Lorenzo Clemente, Thomas Colcombet, Paweł Parys

Abstract: In this work we prove decidability of the model-checking problem for safe recursion schemes against properties defined by alternating B-automata. We then exploit this result to show how to compute downward closures of languages of finite trees recognized by safe recursion schemes. Higher-order recursion schemes are an expressive formalism used to define languages of finite and infinite ranked tr… ▽ More In this work we prove decidability of the model-checking problem for safe recursion schemes against properties defined by alternating B-automata. We then exploit this result to show how to compute downward closures of languages of finite trees recognized by safe recursion schemes. Higher-order recursion schemes are an expressive formalism used to define languages of finite and infinite ranked trees by means of fixed points of lambda terms. They extend regular and context-free grammars, and are equivalent in expressive power to the simply typed $λY$-calculus and collapsible pushdown automata. Safety in a syntactic restriction which limits their expressive power. The class of alternating B-automata is an extension of alternating parity automata over infinite trees; it enhances them with counting features that can be used to describe boundedness properties. △ Less

Submitted 28 March, 2023; v1 submitted 25 April, 2020; originally announced April 2020.

Journal ref: Fundamenta Informaticae, Volume 188, Issue 3 (April 18, 2023) fi:8485

Parity Games: Another View on Lehtinen's Algorithm

Authors: Paweł Parys

Abstract: Recently, five quasi-polynomial-time algorithms solving parity games were proposed. We elaborate on one of the algorithms, by Lehtinen (2018). Czerwiński et al. (2019) observe that four of the algorithms can be expressed as constructions of separating automata (of quasi-polynomial size), that is, automata that accept all plays decisively won by one of the players, and rejecting all plays decisiv… ▽ More Recently, five quasi-polynomial-time algorithms solving parity games were proposed. We elaborate on one of the algorithms, by Lehtinen (2018). Czerwiński et al. (2019) observe that four of the algorithms can be expressed as constructions of separating automata (of quasi-polynomial size), that is, automata that accept all plays decisively won by one of the players, and rejecting all plays decisively won by the other player. The separating automata corresponding to three of the algorithms are deterministic, and it is clear that deterministic separating automata can be used to solve parity games. The separating automaton corresponding to the algorithm of Lehtinen is nondeterministic, though. While this particular automaton can be used to solve parity games, this is not true for every nondeterministic separating automaton. As a first (more conceptual) contribution, we specify when a nondeterministic separating automaton can be used to solve parity games. We also repeat the correctness proof of the Lehtinen's algorithm, using separating automata. In this part, we prove that her construction actually leads to a faster algorithm than originally claimed in her paper: its complexity is $n^{O(\log n)}$ rather than $n^{O(\log d \cdot \log n)}$ (where $n$ is the number of nodes, and $d$ the number of priorities of a considered parity game), which is similar to complexities of the other quasi-polynomial-time algorithms. △ Less

Submitted 9 October, 2019; originally announced October 2019.

Parity Games: Zielonka's Algorithm in Quasi-Polynomial Time

Authors: Paweł Parys

Abstract: Calude, Jain, Khoussainov, Li, and Stephan (2017) proposed a quasi-polynomial-time algorithm solving parity games. After this breakthrough result, a few other quasi-polynomial-time algorithms were introduced; none of them is easy to understand. Moreover, it turns out that in practice they operate very slowly. On the other side there is the Zielonka's recursive algorithm, which is very simple, expo… ▽ More Calude, Jain, Khoussainov, Li, and Stephan (2017) proposed a quasi-polynomial-time algorithm solving parity games. After this breakthrough result, a few other quasi-polynomial-time algorithms were introduced; none of them is easy to understand. Moreover, it turns out that in practice they operate very slowly. On the other side there is the Zielonka's recursive algorithm, which is very simple, exponential in the worst case, and the fastest in practice. We combine these two approaches: we propose a small modification of the Zielonka's algorithm, which ensures that the running time is at most quasi-polynomial. In effect, we obtain a simple algorithm that solves parity games in quasi-polynomial time. We also hope that our algorithm, after further optimizations, can lead to an algorithm that shares the good performance of the Zielonka's algorithm on typical inputs, while reducing the worst-case complexity on difficult inputs. △ Less

Submitted 29 April, 2019; originally announced April 2019.

Intersection Types for Unboundedness Problems

Authors: Paweł Parys

Abstract: Intersection types have been originally developed as an extension of simple types, but they can also be used for refining simple types. In this survey we concentrate on the latter option; more precisely, on the use of intersection types for describing quantitative properties of simply typed lambda-terms. We present two type systems. The first allows to estimate (by appropriately defined value of a… ▽ More Intersection types have been originally developed as an extension of simple types, but they can also be used for refining simple types. In this survey we concentrate on the latter option; more precisely, on the use of intersection types for describing quantitative properties of simply typed lambda-terms. We present two type systems. The first allows to estimate (by appropriately defined value of a derivation) the number of appearances of a fixed constant 'a' in the beta-normal form of a considered lambda-term. The second type system is more complicated, and allows to estimate the maximal number of appearances of the constant 'a' on a single branch. △ Less

Submitted 22 April, 2019; originally announced April 2019.

Comments: In Proceedings DCM 2018 and ITRS 2018 , arXiv:1904.09561

ACM Class: F.4.1

Journal ref: EPTCS 293, 2019, pp. 7-27

Recursion Schemes, the MSO Logic, and the U quantifier

Authors: Paweł Parys

Abstract: We study the model-checking problem for recursion schemes: does the tree generated by a given higher-order recursion scheme satisfy a given logical sentence. The problem is known to be decidable for sentences of the MSO logic. We prove decidability for an extension of MSO in which we additionally have an unbounding quantifier U, saying that a subformula is true for arbitrarily large finite sets. T… ▽ More We study the model-checking problem for recursion schemes: does the tree generated by a given higher-order recursion scheme satisfy a given logical sentence. The problem is known to be decidable for sentences of the MSO logic. We prove decidability for an extension of MSO in which we additionally have an unbounding quantifier U, saying that a subformula is true for arbitrarily large finite sets. This quantifier can be used only for subformulae in which all free variables represent finite sets (while an unrestricted use of the quantifier leads to undecidability). We also show that the logic has the properties of reflection and effective selection for trees generated by recursion schemes. △ Less

Submitted 17 February, 2020; v1 submitted 10 October, 2018; originally announced October 2018.

Journal ref: Logical Methods in Computer Science, Volume 16, Issue 1 (February 18, 2020) lmcs:4885

Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games

Authors: Wojciech Czerwiński, Laure Daviaud, Nathanaël Fijalkow, Marcin Jurdziński, Ranko Lazić, Paweł Parys

Abstract: Several distinct techniques have been proposed to design quasi-polynomial algorithms for solving parity games since the breakthrough result of Calude, Jain, Khoussainov, Li, and Stephan (2017): play summaries, progress measures and register games. We argue that all those techniques can be viewed as instances of the separation approach to solving parity games, a key technical component of which is… ▽ More Several distinct techniques have been proposed to design quasi-polynomial algorithms for solving parity games since the breakthrough result of Calude, Jain, Khoussainov, Li, and Stephan (2017): play summaries, progress measures and register games. We argue that all those techniques can be viewed as instances of the separation approach to solving parity games, a key technical component of which is constructing (explicitly or implicitly) an automaton that separates languages of words encoding plays that are (decisively) won by either of the two players. Our main technical result is a quasi-polynomial lower bound on the size of such separating automata that nearly matches the current best upper bounds. This forms a barrier that all existing approaches must overcome in the ongoing quest for a polynomial-time algorithm for solving parity games. The key and fundamental concept that we introduce and study is a universal ordered tree. The technical highlights are a quasi-polynomial lower bound on the size of universal ordered trees and a proof that every separating safety automaton has a universal tree hidden in its state space. △ Less

Submitted 2 November, 2018; v1 submitted 27 July, 2018; originally announced July 2018.

Comments: To appear in SODA 2019

Efficient acceleration of a dense plasma projectile to hyper velocities in the laser-induced cavity pressure acceleration scheme

Authors: Jan Badziak, Eduard Krousky, Jan Marczak, Piotr Parys, Tadeusz Pisarczyk, Marcin Rosinski, Antoni Sarzynski, Tomasz Chodukowski, Jan Dostal, Roman Dudzak, Zofia Kalinowska, Milan Kucharik, Richard Liska, Miroslav Pfeifer, Jiri Ullschmied, Agnieszka Zaras-Szydlowska

Abstract: The experimental study of the plasma projectile acceleration in the laser-induced cavity pressure acceleration (LICPA) scheme is reported. In the experiment performed at the kilojoule PALS laser facility, the parameters of the projectile were measured using interferometry, a streak camera and ion diagnostics, and the measurements were supported by two-dimensional hydrodynamic simulations. It is sh… ▽ More The experimental study of the plasma projectile acceleration in the laser-induced cavity pressure acceleration (LICPA) scheme is reported. In the experiment performed at the kilojoule PALS laser facility, the parameters of the projectile were measured using interferometry, a streak camera and ion diagnostics, and the measurements were supported by two-dimensional hydrodynamic simulations. It is shown that in the LICPA accelerator with a 200-J laser driver, a 4 microgram gold plasma projectile is accelerated to the velocity of 140 km/s with the energetic acceleration efficiency of 15-19 percent which is at least several times higher than those achieved with the commonly used ablative acceleration and the highest among the ones measured so far for any projectiles accelerated to the velocities above 100 km/s. This achievement opens the possibility of creation and investigation of high-energy-density matter states with the use of moderate-energy lasers and may also have an impact on the development of the impact ignition approach to inertial confinement fusion. △ Less

Submitted 28 July, 2017; originally announced July 2017.

Comments: 8 pages, 5 figures, 1 table

From Data to Decisions: Distributionally Robust Optimization is Optimal

Authors: Bart P. G. Van Parys, Peyman Mohajerin Esfahani, Daniel Kuhn

Abstract: We study stochastic programs where the decision-maker cannot observe the distribution of the exogenous uncertainties but has access to a finite set of independent samples from this distribution. In this setting, the goal is to find a procedure that transforms the data to an estimate of the expected cost function under the unknown data-generating distribution, i.e., a predictor, and an optimizer of… ▽ More We study stochastic programs where the decision-maker cannot observe the distribution of the exogenous uncertainties but has access to a finite set of independent samples from this distribution. In this setting, the goal is to find a procedure that transforms the data to an estimate of the expected cost function under the unknown data-generating distribution, i.e., a predictor, and an optimizer of the estimated cost function that serves as a near-optimal candidate decision, i.e., a prescriptor. As functions of the data, predictors and prescriptors constitute statistical estimators. We propose a meta-optimization problem to find the least conservative predictors and prescriptors subject to constraints on their out-of-sample disappointment. The out-of-sample disappointment quantifies the probability that the actual expected cost of the candidate decision under the unknown true distribution exceeds its predicted cost. Leveraging tools from large deviations theory, we prove that this meta-optimization problem admits a unique solution: The best predictor-prescriptor pair is obtained by solving a distributionally robust optimization problem over all distributions within a given relative entropy distance from the empirical distribution of the data. △ Less

Submitted 22 December, 2019; v1 submitted 13 April, 2017; originally announced April 2017.

Intersection Types and Counting

Authors: Paweł Parys

Abstract: We present a new approach to the following meta-problem: given a quantitative property of trees, design a type system such that the desired property for the tree generated by an infinitary ground lambda-term corresponds to some property of a derivation of a type for this lambda-term, in this type system. Our approach is presented in the particular case of the language finiteness problem for nond… ▽ More We present a new approach to the following meta-problem: given a quantitative property of trees, design a type system such that the desired property for the tree generated by an infinitary ground lambda-term corresponds to some property of a derivation of a type for this lambda-term, in this type system. Our approach is presented in the particular case of the language finiteness problem for nondeterministic higher-order recursion schemes (HORSes): given a nondeterministic HORS, decide whether the set of all finite trees generated by this HORS is finite. We give a type system such that the HORS can generate a tree of an arbitrarily large finite size if and only if in the type system we can obtain derivations that are arbitrarily large, in an appropriate sense; the latter condition can be easily decided. △ Less

Submitted 30 March, 2017; v1 submitted 7 February, 2017; originally announced February 2017.

Comments: In Proceedings ITRS 2016, arXiv:1702.01874

ACM Class: F.4.3

Journal ref: EPTCS 242, 2017, pp. 48-63

Intersection Types and Counting

Authors: Paweł Parys

Abstract: We present a new approach to the following meta-problem: given a quantitative property of trees, design a type system such that the desired property for the tree generated by an infinitary ground $λ$-term corresponds to some property of a derivation of a type for this $λ$-term, in this type system. Our approach is presented in the particular case of the language finiteness problem for nondetermi… ▽ More We present a new approach to the following meta-problem: given a quantitative property of trees, design a type system such that the desired property for the tree generated by an infinitary ground $λ$-term corresponds to some property of a derivation of a type for this $λ$-term, in this type system. Our approach is presented in the particular case of the language finiteness problem for nondeterministic higher-order recursion schemes (HORSes): given a nondeterministic HORS, decide whether the set of all finite trees generated by this HORS is finite. We give a type system such that the HORS can generate a tree of an arbitrarily large finite size if and only if in the type system we can obtain derivations that are arbitrarily large, in an appropriate sense; the latter condition can be easily decided. △ Less

Submitted 19 January, 2017; originally announced January 2017.

Comments: Full version (with appendix) of a conference paper from Eighth Workshop on Intersection Types and Related Systems

The Diagonal Problem for Higher-Order Recursion Schemes is Decidable

Authors: Lorenzo Clemente, Paweł Parys, Sylvain Salvati, Igor Walukiewicz

Abstract: A non-deterministic recursion scheme recognizes a language of finite trees. This very expressive model can simulate, among others, higher-order pushdown automata with collapse. We show decidability of the diagonal problem for schemes. This result has several interesting consequences. In particular, it gives an algorithm that computes the downward closure of languages of words recognized by schemes… ▽ More A non-deterministic recursion scheme recognizes a language of finite trees. This very expressive model can simulate, among others, higher-order pushdown automata with collapse. We show decidability of the diagonal problem for schemes. This result has several interesting consequences. In particular, it gives an algorithm that computes the downward closure of languages of words recognized by schemes. In turn, this has immediate application to separability problems and reachability analysis of concurrent systems. △ Less

Submitted 2 May, 2016; originally announced May 2016.

Comments: technical report; to appear in LICS'16

Ordered Tree-Pushdown Systems

Authors: Lorenzo Clemente, Paweł Parys, Sylvain Salvati, Igor Walukiewicz

Abstract: We define a new class of pushdown systems where the pushdown is a tree instead of a word. We allow a limited form of lookahead on the pushdown conforming to a certain ordering restriction, and we show that the resulting class enjoys a decidable reachability problem. This follows from a preservation of recognizability result for the backward reachability relation of such systems. As an application,… ▽ More We define a new class of pushdown systems where the pushdown is a tree instead of a word. We allow a limited form of lookahead on the pushdown conforming to a certain ordering restriction, and we show that the resulting class enjoys a decidable reachability problem. This follows from a preservation of recognizability result for the backward reachability relation of such systems. As an application, we show that our simple model can encode several formalisms generalizing pushdown systems, such as ordered multi-pushdown systems, annotated higher-order pushdown systems, the Krivine machine, and ordered annotated multi-pushdown systems. In each case, our procedure yields tight complexity. △ Less

Submitted 12 October, 2015; originally announced October 2015.

Comments: full technical report of FST-TCS'15 paper

ACM Class: D.1.1; D.2.4; F.1.1; F.3.1; F.4.1

The MSO+U theory of (N, <) is undecidable

Authors: Mikołaj Bojańczyk, Paweł Parys, Szymon Toruńczyk

Abstract: We consider the logic MSO+U, which is monadic second-order logic extended with the unbounding quantifier. The unbounding quantifier is used to say that a property of finite sets holds for sets of arbitrarily large size. We prove that the logic is undecidable on infinite words, i.e. the MSO+U theory of (N,<) is undecidable. This settles an open problem about the logic, and improves a previous undec… ▽ More We consider the logic MSO+U, which is monadic second-order logic extended with the unbounding quantifier. The unbounding quantifier is used to say that a property of finite sets holds for sets of arbitrarily large size. We prove that the logic is undecidable on infinite words, i.e. the MSO+U theory of (N,<) is undecidable. This settles an open problem about the logic, and improves a previous undecidability result, which used infinite trees and additional axioms from set theory. △ Less

Submitted 17 February, 2015; v1 submitted 16 February, 2015; originally announced February 2015.

Comments: 9 pages, with 2 figures

Higher-Order Pushdown Systems with Data

Authors: Paweł Parys

Abstract: We propose a new extension of higher-order pushdown automata, which allows to use an infinite alphabet. The new automata recognize languages of data words (instead of normal words), which beside each its letter from a finite alphabet have a data value from an infinite alphabet. Those data values can be loaded to the stack of the automaton, and later compared with some farther data values on the in… ▽ More We propose a new extension of higher-order pushdown automata, which allows to use an infinite alphabet. The new automata recognize languages of data words (instead of normal words), which beside each its letter from a finite alphabet have a data value from an infinite alphabet. Those data values can be loaded to the stack of the automaton, and later compared with some farther data values on the input. Our main purpose for introducing these automata is that they may help in analyzing normal automata (without data). As an example, we give a proof that deterministic automata with collapse can recognize more languages than deterministic automata without collapse. This proof is simpler than in the no-data case. We also state a hypothesis how the new automaton model can be related to the original model of higher-order pushdown automata. △ Less

Submitted 8 October, 2012; originally announced October 2012.

Comments: In Proceedings GandALF 2012, arXiv:1210.2028

ACM Class: F.1.1; F.4.3

Journal ref: EPTCS 96, 2012, pp. 210-223

Weak Alternating Timed Automata

Authors: Pawel Parys, Igor Walukiewicz

Abstract: Alternating timed automata on infinite words are considered. The main result is a characterization of acceptance conditions for which the emptiness problem for these automata is decidable. This result implies new decidability results for fragments of timed temporal logics. It is also shown that, unlike for MITL, the characterisation remains the same even if no punctual constraints are allowed. Alternating timed automata on infinite words are considered. The main result is a characterization of acceptance conditions for which the emptiness problem for these automata is decidable. This result implies new decidability results for fragments of timed temporal logics. It is also shown that, unlike for MITL, the characterisation remains the same even if no punctual constraints are allowed. △ Less

Submitted 16 September, 2012; v1 submitted 29 August, 2012; originally announced August 2012.

ACM Class: F.1.1, F.4.3

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 3 (September 19, 2012) lmcs:1214

Strictness of the Collapsible Pushdown Hierarchy

Authors: Alexander Kartzow, Paweł Parys

Abstract: We present a pum** lemma for each level of the collapsible pushdown graph hierarchy in analogy to the second author's pum** lemma for higher-order pushdown graphs (without collapse). Using this lemma, we give the first known examples that separate the levels of the collapsible pushdown graph hierarchy and of the collapsible pushdown tree hierarchy, i.e., the hierarchy of trees generated by hig… ▽ More We present a pum** lemma for each level of the collapsible pushdown graph hierarchy in analogy to the second author's pum** lemma for higher-order pushdown graphs (without collapse). Using this lemma, we give the first known examples that separate the levels of the collapsible pushdown graph hierarchy and of the collapsible pushdown tree hierarchy, i.e., the hierarchy of trees generated by higher-order recursion schemes. This confirms the open conjecture that higher orders allow one to generate more graphs and more trees. △ Less

Submitted 14 June, 2012; v1 submitted 16 January, 2012; originally announced January 2012.

Comments: 68 pages, short version in MFCS 2012