Fält, Mattias
Convergence Analysis and Improvements for Projection Algorithms and Splitting Methods PhD Thesis
Lund University, 2021, ISBN: 978-91-7895-763-7.
@phdthesis{falt2021convergence,
title = {Convergence Analysis and Improvements for Projection Algorithms and Splitting Methods},
author = {Mattias Fält},
url = {https://portal.research.lu.se/portal/files/90535299/thesis.pdf},
isbn = {978-91-7895-763-7},
year = {2021},
date = {2021-02-26},
school = {Lund University},
abstract = {Non-smooth convex optimization problems occur in all fields of engineering. A common approach to solving this class of problems is proximal algorithms, or splitting methods. These first-order optimization algorithms are often simple, well suited to solve large-scale problems and have a low computational cost per iteration. Essentially, they encode the solution to an optimization problem as a fixed point of some operator, and iterating this operator eventually results in convergence to an optimal point. However, as for other first order methods, the convergence rate is heavily dependent on the conditioning of the problem. Even though the per-iteration cost is usually low, the number of iterations can become prohibitively large for ill-conditioned problems, especially if a high accuracy solution is sought.},
keywords = {},
pubstate = {published},
tppubtype = {phdthesis}
}
Non-smooth convex optimization problems occur in all fields of engineering. A common approach to solving this class of problems is proximal algorithms, or splitting methods. These first-order optimization algorithms are often simple, well suited to solve large-scale problems and have a low computational cost per iteration. Essentially, they encode the solution to an optimization problem as a fixed point of some operator, and iterating this operator eventually results in convergence to an optimal point. However, as for other first order methods, the convergence rate is heavily dependent on the conditioning of the problem. Even though the per-iteration cost is usually low, the number of iterations can become prohibitively large for ill-conditioned problems, especially if a high accuracy solution is sought.
Fält, Mattias; Giselsson, Pontus
Generalized Alternating Projections on Manifolds and Convex Sets Journal Article Forthcoming
In: arXiv preprint arXiv:2101.07286, Forthcoming.
@article{falt2021generalized,
title = {Generalized Alternating Projections on Manifolds and Convex Sets},
author = {Mattias Fält and Pontus Giselsson},
url = {https://arxiv.org/pdf/2101.07286.pdf},
year = {2021},
date = {2021-01-18},
urldate = {2021-01-18},
journal = {arXiv preprint arXiv:2101.07286},
abstract = {In this paper we extend the previous convergence results on the generalized alternating projection method, from subspaces [arXiv:1703.10547], to include smooth manifolds. We show that locally it will behave in the same way, with the same rate as predicted in [arXiv:1703.10547]. The goal is to get closer to a rate for general convex sets, where convergence, but not rate is known. If a finite identification property can be shown for two convex sets, to locally smooth manifolds, then the rates from this paper also apply to those sets. We present a few examples where this is the case, and also a counter example for when this is not the case. },
keywords = {},
pubstate = {forthcoming},
tppubtype = {article}
}
In this paper we extend the previous convergence results on the generalized alternating projection method, from subspaces [arXiv:1703.10547], to include smooth manifolds. We show that locally it will behave in the same way, with the same rate as predicted in [arXiv:1703.10547]. The goal is to get closer to a rate for general convex sets, where convergence, but not rate is known. If a finite identification property can be shown for two convex sets, to locally smooth manifolds, then the rates from this paper also apply to those sets. We present a few examples where this is the case, and also a counter example for when this is not the case.
Fält, Mattias; Giselsson, Pontus
QPDAS: Dual Active Set Solver for Mixed Constraint Quadratic Programming Inproceedings
In: 2019 IEEE 58th Conference on Decision and Control (CDC), pp. 4891–4897, IEEE 2019.
@inproceedings{falt2019qpdas,
title = {QPDAS: Dual Active Set Solver for Mixed Constraint Quadratic Programming},
author = {Mattias Fält and Pontus Giselsson},
url = {https://arxiv.org/abs/1911.12662},
doi = {10.1109/CDC40024.2019.9029900},
year = {2019},
date = {2019-12-11},
booktitle = {2019 IEEE 58th Conference on Decision and Control (CDC)},
pages = {4891--4897},
organization = {IEEE},
abstract = {We present a method for solving the general mixed constrained convex quadratic programming problem using an active set method on the dual problem. The approach is similar to existing active set methods, but we present a new way of solving the linear systems arising in the algorithm. There are two main contributions; we present a new way of factorizing the linear systems, and show how iterative refinement can be used to achieve good accuracy and to solve both types of sub-problems that arise from semi-definite problems.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
We present a method for solving the general mixed constrained convex quadratic programming problem using an active set method on the dual problem. The approach is similar to existing active set methods, but we present a new way of solving the linear systems arising in the algorithm. There are two main contributions; we present a new way of factorizing the linear systems, and show how iterative refinement can be used to achieve good accuracy and to solve both types of sub-problems that arise from semi-definite problems.
Fält, Mattias; Giselsson, Pontus
System Identification for Hybrid Systems using Neural Networks Inproceedings
In: 2019.
@inproceedings{falt2019system,
title = {System Identification for Hybrid Systems using Neural Networks},
author = {Mattias Fält and Pontus Giselsson},
url = {https://arxiv.org/abs/1911.12663},
year = {2019},
date = {2019-11-28},
urldate = {2019-11-28},
journal = {arXiv preprint arXiv:1911.12663},
abstract = {With new advances in machine learning and in particular powerful learning libraries, we illustrate some of the new possibilities they enable in terms of nonlinear system identification. For a large class of hybrid systems, we explain how these tools allow for identification of complex dynamics using neural networks. We illustrate the method by examining the performance on a quad-rotor example. },
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
With new advances in machine learning and in particular powerful learning libraries, we illustrate some of the new possibilities they enable in terms of nonlinear system identification. For a large class of hybrid systems, we explain how these tools allow for identification of complex dynamics using neural networks. We illustrate the method by examining the performance on a quad-rotor example.
Troeng, Olof; Fält, Mattias
Sparsity-constrained optimization of inputs to second-order systems Inproceedings
In: 2019 18th European Control Conference (ECC), pp. 406–410, IEEE 2019.
@inproceedings{troeng2019sparsity,
title = {Sparsity-constrained optimization of inputs to second-order systems},
author = {Olof Troeng and Mattias Fält},
url = {https://ieeexplore.ieee.org/abstract/document/8796020},
doi = {10.23919/ECC.2019.8796020},
year = {2019},
date = {2019-06-25},
booktitle = {2019 18th European Control Conference (ECC)},
pages = {406--410},
organization = {IEEE},
abstract = {We propose an efficient algorithm, that given a strictly proper, second-order system, finds a sparse input signal so that the system's output optimally approximates a given trajectory in least-squares sense. As an illustration, we apply the algorithm to an estimation problem from medicine.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
We propose an efficient algorithm, that given a strictly proper, second-order system, finds a sparse input signal so that the system's output optimally approximates a given trajectory in least-squares sense. As an illustration, we apply the algorithm to an estimation problem from medicine.
Troeng, Olof; Fält, Mattias
A seemingly polynomial-time algorithm for optimal curve fitting by segmented straight lines Inproceedings
In: 2018 IEEE Conference on Decision and Control (CDC), pp. 4091–4096, IEEE 2018.
@inproceedings{troeng2018seemingly,
title = {A seemingly polynomial-time algorithm for optimal curve fitting by segmented straight lines},
author = {Olof Troeng and Mattias Fält},
url = {https://ieeexplore.ieee.org/document/8618654},
doi = {10.1109/CDC.2018.8618654},
year = {2018},
date = {2018-12-17},
booktitle = {2018 IEEE Conference on Decision and Control (CDC)},
pages = {4091--4096},
organization = {IEEE},
abstract = {We consider least-squares approximation of a function of one variable by a continuous, piecewise-linear approxim-and that has a small number of breakpoints. This problem was notably considered by Bellman who proposed an approximate algorithm based on dynamic programming. Many suboptimal approaches have been suggested, but so far, the only exact methods resort to mixed integer programming with superpolynomial complexity growth. In this paper, we present an exact and efficient algorithm based on dynamic programming with a hybrid value function. Empirical evidence suggest that the algorithm has a polynomial time complexity.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
We consider least-squares approximation of a function of one variable by a continuous, piecewise-linear approxim-and that has a small number of breakpoints. This problem was notably considered by Bellman who proposed an approximate algorithm based on dynamic programming. Many suboptimal approaches have been suggested, but so far, the only exact methods resort to mixed integer programming with superpolynomial complexity growth. In this paper, we present an exact and efficient algorithm based on dynamic programming with a hybrid value function. Empirical evidence suggest that the algorithm has a polynomial time complexity.
Giselsson, Pontus; Fält, Mattias
Envelope functions: Unifications and further properties Journal Article
In: Journal of Optimization Theory and Applications, 2018.
@article{giselsson2016nonsmooth,
title = {Envelope functions: Unifications and further properties},
author = {Pontus Giselsson and Mattias Fält},
url = {https://arxiv.org/abs/1606.01327
https://link.springer.com/article/10.1007/s10957-018-1328-z},
doi = {10.1007/s10957-018-1328-z},
year = {2018},
date = {2018-06-12},
journal = {Journal of Optimization Theory and Applications},
abstract = {Forward–backward and Douglas–Rachford splitting are methods for structured nonsmooth optimization. With the aim to use smooth optimization techniques for nonsmooth problems, the forward–backward and Douglas–Rachford envelopes where recently proposed. Under specific problem assumptions, these envelope functions have favorable smoothness and convexity properties and their stationary points coincide with the fixed-points of the underlying algorithm operators. This allows for solving such nonsmooth optimization problems by minimizing the corresponding smooth convex envelope function. In this paper, we present a general envelope function that unifies and generalizes existing ones. We provide properties of the general envelope function that sharpen corresponding known results for the special cases. We also present a new interpretation of the underlying methods as being majorization–minimization algorithms applied to their respective envelope functions.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Forward–backward and Douglas–Rachford splitting are methods for structured nonsmooth optimization. With the aim to use smooth optimization techniques for nonsmooth problems, the forward–backward and Douglas–Rachford envelopes where recently proposed. Under specific problem assumptions, these envelope functions have favorable smoothness and convexity properties and their stationary points coincide with the fixed-points of the underlying algorithm operators. This allows for solving such nonsmooth optimization problems by minimizing the corresponding smooth convex envelope function. In this paper, we present a general envelope function that unifies and generalizes existing ones. We provide properties of the general envelope function that sharpen corresponding known results for the special cases. We also present a new interpretation of the underlying methods as being majorization–minimization algorithms applied to their respective envelope functions.
Fält, Mattias; Giselsson, Pontus
Line Search For Generalized Alternating Projections Inproceedings
In: 2017 American Control Conference (ACC), pp. 4637–4642, IEEE 2017.
@inproceedings{falt2017line,
title = {Line Search For Generalized Alternating Projections},
author = {Mattias Fält and Pontus Giselsson},
url = {https://arxiv.org/abs/1609.05920},
year = {2017},
date = {2017-05-24},
booktitle = {2017 American Control Conference (ACC)},
pages = {4637--4642},
organization = {IEEE},
abstract = {This paper is about line search for the generalized alternating projections (GAP) method. This method is a generalization of the von Neumann alternating projections method, where instead of performing alternating projections, relaxed projections are alternated. The method can be interpreted as an averaged iteration of a nonexpansive mapping. Therefore, a recently proposed line search method for such algorithms is applicable to GAP. We evaluate this line search and show situations when the line search can be performed with little additional cost. We also present a variation of the basic line search for GAP - the projected line search. We prove its convergence and show that the line search condition is convex in the step length parameter. We show that almost all convex optimization problems can be solved using this approach and numerical results show superior performance with both the standard and the projected line search, sometimes by several orders of magnitude, compared to the nominal method. },
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
This paper is about line search for the generalized alternating projections (GAP) method. This method is a generalization of the von Neumann alternating projections method, where instead of performing alternating projections, relaxed projections are alternated. The method can be interpreted as an averaged iteration of a nonexpansive mapping. Therefore, a recently proposed line search method for such algorithms is applicable to GAP. We evaluate this line search and show situations when the line search can be performed with little additional cost. We also present a variation of the basic line search for GAP - the projected line search. We prove its convergence and show that the line search condition is convex in the step length parameter. We show that almost all convex optimization problems can be solved using this approach and numerical results show superior performance with both the standard and the projected line search, sometimes by several orders of magnitude, compared to the nominal method.
Fält, Mattias; Giselsson, Pontus
Optimal convergence rates for generalized alternating projections Inproceedings
In: 2017 IEEE 56th Annual Conference on Decision and Control (CDC), pp. 2268–2274, IEEE 2017.
@inproceedings{falt2017optimal,
title = {Optimal convergence rates for generalized alternating projections},
author = {Mattias Fält and Pontus Giselsson},
url = {https://arxiv.org/abs/1703.10547},
doi = {10.1109/CDC.2017.8263980},
year = {2017},
date = {2017-03-30},
booktitle = {2017 IEEE 56th Annual Conference on Decision and Control (CDC)},
pages = {2268--2274},
organization = {IEEE},
abstract = {Generalized alternating projections is an algorithm that alternates relaxed projections onto a finite number of sets to find a point in their intersection. We consider the special case of two linear subspaces, for which the algorithm reduces to a matrix teration. For convergent matrix iterations, the asymptotic rate is linear and decided by the magnitude of the subdominant eigenvalue. In this paper, we show how to select the three algorithm parameters to optimize this magnitude, and hence the asymptotic convergence rate. The obtained rate depends on the Friedrichs angle between the subspaces and is considerably better than known rates for other methods such as alternating projections and Douglas-Rachford splitting. We also present an adaptive scheme that, online, estimates the Friedrichs angle and updates the algorithm parameters based on this estimate. A numerical example is provided that supports our theoretical claims and shows very good performance for the adaptive method. },
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Generalized alternating projections is an algorithm that alternates relaxed projections onto a finite number of sets to find a point in their intersection. We consider the special case of two linear subspaces, for which the algorithm reduces to a matrix teration. For convergent matrix iterations, the asymptotic rate is linear and decided by the magnitude of the subdominant eigenvalue. In this paper, we show how to select the three algorithm parameters to optimize this magnitude, and hence the asymptotic convergence rate. The obtained rate depends on the Friedrichs angle between the subspaces and is considerably better than known rates for other methods such as alternating projections and Douglas-Rachford splitting. We also present an adaptive scheme that, online, estimates the Friedrichs angle and updates the algorithm parameters based on this estimate. A numerical example is provided that supports our theoretical claims and shows very good performance for the adaptive method.
Giselsson, Pontus; Fält, Mattias; Boyd, Stephen
Line Search for Averaged Operator Iteration Inproceedings
In: 2016 IEEE 55th Conference on Decision and Control (CDC), pp. 1015–1022, IEEE 2016.
@inproceedings{giselsson2016line,
title = {Line Search for Averaged Operator Iteration},
author = {Pontus Giselsson and Mattias Fält and Stephen Boyd},
url = {https://arxiv.org/abs/1603.06772},
year = {2016},
date = {2016-12-09},
urldate = {2021-03-22},
booktitle = {2016 IEEE 55th Conference on Decision and Control (CDC)},
pages = {1015--1022},
organization = {IEEE},
abstract = {Many popular first order algorithms for convex optimization, such as forward-backward splitting, Douglas-Rachford splitting, and the alternating direction method of multipliers (ADMM), can be formulated as averaged iteration of a nonexpansive mapping. In this paper we propose a line search for averaged iteration that preserves the theoretical convergence guarantee, while often accelerating practical convergence. We discuss several general cases in which the additional computational cost of the line search is modest compared to the savings obtained.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Many popular first order algorithms for convex optimization, such as forward-backward splitting, Douglas-Rachford splitting, and the alternating direction method of multipliers (ADMM), can be formulated as averaged iteration of a nonexpansive mapping. In this paper we propose a line search for averaged iteration that preserves the theoretical convergence guarantee, while often accelerating practical convergence. We discuss several general cases in which the additional computational cost of the line search is modest compared to the savings obtained.
Carlson, Fredrik Bagge; Fält, Mattias
ControlSystems. jl: A Control Systems Toolbox for Julia Miscellaneous
2016.
@misc{bagge2016controlsystems,
title = {ControlSystems. jl: A Control Systems Toolbox for Julia},
author = {Fredrik Bagge Carlson and Mattias Fält},
url = {https://github.com/JuliaControl/ControlSystems.jl},
year = {2016},
date = {2016-01-01},
publisher = {github},
abstract = {This toolbox works similar to that of other major computer-aided control systems design (CACSD) toolboxes. Systems can be created in either a transfer function or a state space representation. These systems can then be combined into larger architectures, simulated in both time and frequency domain, and analyzed for stability/performance properties.},
keywords = {},
pubstate = {published},
tppubtype = {misc}
}
This toolbox works similar to that of other major computer-aided control systems design (CACSD) toolboxes. Systems can be created in either a transfer function or a state space representation. These systems can then be combined into larger architectures, simulated in both time and frequency domain, and analyzed for stability/performance properties.
Raman, Vasumathi; Fält, Mattias; Wongpiromsarn, Tichakorn; Murray, Richard M
Online horizon selection in receding horizon temporal logic planning Inproceedings
In: 2015 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 3493–3499, IEEE 2015, ISBN: 978-1-4799-9994-1 .
@inproceedings{raman2015online,
title = {Online horizon selection in receding horizon temporal logic planning},
author = {Vasumathi Raman and Mattias Fält and Tichakorn Wongpiromsarn and Richard M Murray},
url = {https://ieeexplore.ieee.org/abstract/document/7353864
https://portal.research.lu.se/portal/files/11330608/8168710.pdf},
doi = {10.1109/IROS.2015.7353864},
isbn = {978-1-4799-9994-1 },
year = {2015},
date = {2015-09-28},
booktitle = {2015 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)},
pages = {3493--3499},
organization = {IEEE},
abstract = {Temporal logics have proven effective for correct-by-construction synthesis of controllers for a wide range of robotic applications. Receding horizon frameworks mitigate the computational intractability of reactive synthesis for temporal logic, but have thus far been limited by pursuing a single sequence of short horizon problems to the goal. We propose a receding horizon algorithm for reactive synthesis that automatically determines a path to the currently pursued goal at runtime, responding as needed to nondeterministic environment behavior. This is achieved by allowing each short horizon to have multiple local goals, and determining which local goal to pursue based on the current global goal, the currently perceived environment and a pre-computed invariant dependent on the global goal. We demonstrate the utility of this additional flexibility in grant-response tasks, using a search-and-rescue example. Moreover, we show that these goal-dependent invariants mitigate the conservativeness of the receding horizon approach.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Temporal logics have proven effective for correct-by-construction synthesis of controllers for a wide range of robotic applications. Receding horizon frameworks mitigate the computational intractability of reactive synthesis for temporal logic, but have thus far been limited by pursuing a single sequence of short horizon problems to the goal. We propose a receding horizon algorithm for reactive synthesis that automatically determines a path to the currently pursued goal at runtime, responding as needed to nondeterministic environment behavior. This is achieved by allowing each short horizon to have multiple local goals, and determining which local goal to pursue based on the current global goal, the currently perceived environment and a pre-computed invariant dependent on the global goal. We demonstrate the utility of this additional flexibility in grant-response tasks, using a search-and-rescue example. Moreover, we show that these goal-dependent invariants mitigate the conservativeness of the receding horizon approach.
Fält, Mattias; Jimbergsson, Lucas
Using ADMM for hybrid system MPC Masters Thesis
2015, ISSN: 0280-5316.
@mastersthesis{falt2015using,
title = {Using ADMM for hybrid system MPC},
author = {Mattias Fält and Lucas Jimbergsson},
url = {https://lup.lub.lu.se/student-papers/search/publication/7445552},
issn = {0280-5316},
year = {2015},
date = {2015-07-03},
abstract = {Model Predictive control (MPC) has been studied extensively because of its ability to handle constraints and its great properties in terms of stability and performance [Mayne et al., 2000]. We have in this thesis focused on MPC of Hybrid Systems, i.e. systems with both continuous and discrete dynamics. More specifically, we look at problems that can be cast as Mixed Integer Quadratic Programming (MIQP) problems which we are solving using a Branch and Bound technique. The problem is in this way reduced to solving a large number of constrained quadratic problems. However, the use in real time systems puts a requirement on the speed and efficiency of the optimization methods used. Because of its low computational cost, there have recently been a rising interest in the Alternating Direction Method of Multiplies (ADMM) for solving constrained optimization problems. We are in this thesis looking at how the different properties of ADMM can be used and improved for these problems, as well as how the Branch and Bound solver can be tailored to accompany ADMM. We have two main contributions to ADMM that mitigate some of the downsides with the often ill-conditioned problems that arise from Hybrid Systems. Firstly, a technique for greatly improving the conditioning of the problems, and secondly, a method to perform fast line search within the solver. We show that these methods are very efficient and can be used to solve problems that are otherwise hard or impossible to precondition properly.},
keywords = {},
pubstate = {published},
tppubtype = {mastersthesis}
}
Model Predictive control (MPC) has been studied extensively because of its ability to handle constraints and its great properties in terms of stability and performance [Mayne et al., 2000]. We have in this thesis focused on MPC of Hybrid Systems, i.e. systems with both continuous and discrete dynamics. More specifically, we look at problems that can be cast as Mixed Integer Quadratic Programming (MIQP) problems which we are solving using a Branch and Bound technique. The problem is in this way reduced to solving a large number of constrained quadratic problems. However, the use in real time systems puts a requirement on the speed and efficiency of the optimization methods used. Because of its low computational cost, there have recently been a rising interest in the Alternating Direction Method of Multiplies (ADMM) for solving constrained optimization problems. We are in this thesis looking at how the different properties of ADMM can be used and improved for these problems, as well as how the Branch and Bound solver can be tailored to accompany ADMM. We have two main contributions to ADMM that mitigate some of the downsides with the often ill-conditioned problems that arise from Hybrid Systems. Firstly, a technique for greatly improving the conditioning of the problems, and secondly, a method to perform fast line search within the solver. We show that these methods are very efficient and can be used to solve problems that are otherwise hard or impossible to precondition properly.
Fält, Mattias; Raman, Vasumathi; Murray, Richard M
Variable elimination for scalable receding horizon temporal logic planning Inproceedings
In: 2015 American Control Conference (ACC), pp. 1917–1922, IEEE 2015.
@inproceedings{falt2015variable,
title = {Variable elimination for scalable receding horizon temporal logic planning},
author = {Mattias Fält and Vasumathi Raman and Richard M Murray},
url = {http://www.cds.caltech.edu/~murray/preprints/frm15-acc_s.pdf},
doi = {10.1109/ACC.2015.7171013},
year = {2015},
date = {2015-07-01},
booktitle = {2015 American Control Conference (ACC)},
pages = {1917--1922},
organization = {IEEE},
abstract = {Correct-by-construction synthesis of high-level reactive control relies on the use of formal methods to generate controllers with provable guarantees on their behavior. While this approach has been successfully applied to a wide range of systems and environments, it scales poorly. A receding horizon framework mitigates this computational blowup, by decomposing the global control problem into several tractable subproblems. The existence of a global controller is ensured through symbolic checks of the specification, and local controllers are synthesized when needed. This reduces the size of the synthesized strategy, but still scales poorly for problems with dynamic environments because of the large number of environment strategies in each subproblem. Ad-hoc methods to locally restrict the environment come with the risk of losing correctness. We present a method for reducing the size of these subproblems by eliminating locally redundant variables, while maintaining correctness of the local (and thus global) controllers. We demonstrate the method using an autonomous car example, on problem sizes that were previously unsolvable due to the number of variables in the environment. We also demonstrate how the reduced specifications can be used to identify opportunities for reusing the synthesized local controllers.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Correct-by-construction synthesis of high-level reactive control relies on the use of formal methods to generate controllers with provable guarantees on their behavior. While this approach has been successfully applied to a wide range of systems and environments, it scales poorly. A receding horizon framework mitigates this computational blowup, by decomposing the global control problem into several tractable subproblems. The existence of a global controller is ensured through symbolic checks of the specification, and local controllers are synthesized when needed. This reduces the size of the synthesized strategy, but still scales poorly for problems with dynamic environments because of the large number of environment strategies in each subproblem. Ad-hoc methods to locally restrict the environment come with the risk of losing correctness. We present a method for reducing the size of these subproblems by eliminating locally redundant variables, while maintaining correctness of the local (and thus global) controllers. We demonstrate the method using an autonomous car example, on problem sizes that were previously unsolvable due to the number of variables in the environment. We also demonstrate how the reduced specifications can be used to identify opportunities for reusing the synthesized local controllers.