Showing 1–6 of 6 results for author: Nilsson, P

Intermittent Connectivity for Exploration in Communication-Constrained Multi-Agent Systems

Authors: Filip Klaesson, Petter Nilsson, Aaron D. Ames, Richard M. Murray

Abstract: Motivated by exploration of communication-constrained underground environments using robot teams, we study the problem of planning for intermittent connectivity in multi-agent systems. We propose a novel concept of information-consistency to handle situations where the plan is not initially known by all agents, and suggest an integer linear program for synthesizing information-consistent plans tha… ▽ More Motivated by exploration of communication-constrained underground environments using robot teams, we study the problem of planning for intermittent connectivity in multi-agent systems. We propose a novel concept of information-consistency to handle situations where the plan is not initially known by all agents, and suggest an integer linear program for synthesizing information-consistent plans that also achieve auxiliary goals. Furthermore, inspired by network flow problems we propose a novel way to pose connectivity constraints that scales much better than previous methods. In the second part of the paper we apply these results in an exploration setting, and propose a clustering method that separates a large exploration problem into smaller problems that can be solved independently. We demonstrate how the resulting exploration algorithm is able to coordinate a team of ten agents to explore a large environment. △ Less

Submitted 19 November, 2019; originally announced November 2019.

Multirobot Coordination with Counting Temporal Logics

Authors: Yunus Emre Sahin, Petter Nilsson, Necmiye Ozay

Abstract: In many multirobot applications, planning trajectories in a way to guarantee that the collective behavior of the robots satisfies a certain high-level specification is crucial. Motivated by this problem, we introduce counting temporal logics---formal languages that enable concise expression of multirobot task specifications over possibly infinite horizons. We first introduce a general logic called… ▽ More In many multirobot applications, planning trajectories in a way to guarantee that the collective behavior of the robots satisfies a certain high-level specification is crucial. Motivated by this problem, we introduce counting temporal logics---formal languages that enable concise expression of multirobot task specifications over possibly infinite horizons. We first introduce a general logic called counting linear temporal logic plus (cLTL+), and propose an optimization-based method that generates individual trajectories such that satisfaction of a given cLTL+ formula is guaranteed when these trajectories are synchronously executed. We then introduce a fragment of cLTL+, called counting linear temporal logic (cLTL), and show that a solution to planning problem with cLTL constraints can be obtained more efficiently if all robots have identical dynamics. In the second part of the paper, we relax the synchrony assumption and discuss how to generate trajectories that can be asynchronously executed, while preserving the satisfaction of the desired cLTL+ specification. In particular, we show that when the asynchrony between robots is bounded, the method presented in this paper can be modified to generate robust trajectories. We demonstrate these ideas with an experiment and provide numerical results that showcase the scalability of the method. △ Less

Submitted 30 October, 2018; originally announced October 2018.

Comments: Under submission for a journal

Using control synthesis to generate corner cases: A case study on autonomous driving

Authors: Glen Chou, Yunus E. Sahin, Liren Yang, Kwesi J. Rutledge, Petter Nilsson, Necmiye Ozay

Abstract: This paper employs correct-by-construction control synthesis, in particular controlled invariant set computations, for falsification. Our hypothesis is that if it is possible to compute a "large enough" controlled invariant set either for the actual system model or some simplification of the system model, interesting corner cases for other control designs can be generated by sampling initial condi… ▽ More This paper employs correct-by-construction control synthesis, in particular controlled invariant set computations, for falsification. Our hypothesis is that if it is possible to compute a "large enough" controlled invariant set either for the actual system model or some simplification of the system model, interesting corner cases for other control designs can be generated by sampling initial conditions from the boundary of this controlled invariant set. Moreover, if falsifying trajectories for a given control design can be found through such sampling, then the controlled invariant set can be used as a supervisor to ensure safe operation of the control design under consideration. In addition to interesting initial conditions, which are mostly related to safety violations in transients, we use solutions from a dual game, a reachability game for the safety specification, to find falsifying inputs. We also propose optimization-based heuristics for input generation for cases when the state is outside the winning set of the dual game. To demonstrate the proposed ideas, we consider case studies from basic autonomous driving functionality, in particular, adaptive cruise control and lane kee**. We show how the proposed technique can be used to find interesting falsifying trajectories for classical control designs like proportional controllers, proportional integral controllers and model predictive controllers, as well as an open source real-world autonomous driving package. △ Less

Submitted 3 August, 2018; v1 submitted 25 July, 2018; originally announced July 2018.

Comments: To appear at EMSOFT 2018

Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings

Authors: Oscar Lindvall Bulancea, Petter Nilsson, Necmiye Ozay

Abstract: This paper presents a control synthesis algorithm for dynamical systems to satisfy specifications given in a fragment of linear temporal logic. It is based on an abstraction-refinement scheme with nonuniform partitions of the state space. A novel encoding of the resulting transition system is proposed that uses binary decision diagrams for efficiency. We discuss several factors affecting scalabili… ▽ More This paper presents a control synthesis algorithm for dynamical systems to satisfy specifications given in a fragment of linear temporal logic. It is based on an abstraction-refinement scheme with nonuniform partitions of the state space. A novel encoding of the resulting transition system is proposed that uses binary decision diagrams for efficiency. We discuss several factors affecting scalability and present some benchmark results demonstrating the effectiveness of the new encodings. These ideas are also being implemented on a publicly available prototype tool, ARCS, that we briefly introduce in the paper. △ Less

Submitted 11 April, 2018; originally announced April 2018.

Comments: Long version of paper for the IFAC Conference on Analysis and Design of Hybrid Systems (ADHS)

Control Synthesis for Permutation-Symmetric High-Dimensional Systems With Counting Constraints

Authors: Petter Nilsson, Necmiye Ozay

Abstract: General purpose correct-by-construction synthesis methods are limited to systems with low dimensionality or simple specifications. In this work we consider highly symmetrical counting problems and exploit the symmetry to synthesize provably correct controllers for systems with tens of thousands of states. The key ingredients of the solution are an aggregate abstraction procedure for mildly heterog… ▽ More General purpose correct-by-construction synthesis methods are limited to systems with low dimensionality or simple specifications. In this work we consider highly symmetrical counting problems and exploit the symmetry to synthesize provably correct controllers for systems with tens of thousands of states. The key ingredients of the solution are an aggregate abstraction procedure for mildly heterogeneous systems and a formulation of counting constraints as linear inequalities. △ Less

Submitted 10 July, 2018; v1 submitted 23 June, 2017; originally announced June 2017.

Comments: submitted for journal publication

Synthesis of separable controlled invariant sets for modular local control design

Authors: Petter Nilsson, Necmiye Ozay

Abstract: Many correct-by-construction control synthesis methods suffer from the curse of dimensionality. Motivated by this challenge, we seek to reduce a correct-by-construction control synthesis problem to subproblems of more modest dimension. As a step towards this goal, in this paper we consider the problem of synthesizing decoupled robustly controlled invariant sets for dynamically coupled linear subsy… ▽ More Many correct-by-construction control synthesis methods suffer from the curse of dimensionality. Motivated by this challenge, we seek to reduce a correct-by-construction control synthesis problem to subproblems of more modest dimension. As a step towards this goal, in this paper we consider the problem of synthesizing decoupled robustly controlled invariant sets for dynamically coupled linear subsystems with state and input constraints. Our approach, which gives sufficient conditions for decoupled invariance, is based on optimization over linear matrix inequalities which are obtained using slack variable identities. We illustrate the applicability of our method on several examples, including one where we solve local control synthesis problems in a compositional manner. △ Less

Submitted 10 October, 2015; originally announced October 2015.