ROCS in Control Synthesis

ROCS is a C++ library to solve formal control synthesis problems for nonlinear dynamical systems w.r.t. temporal logic specifications. Such control problems deal with

  • hybrid system behaviors and/or

  • complex control specifications, e.g., linear-time properties, that are beyond classic control objectives such as stabilization.

An explanatory example

The following two-link manipulator is a nonlinear mechanical system driven by the motors at two joints. By controlling the angles of both arms, the end effector may reach a given position in the operational space. The mission of this manipulator is to finish tasks in different goal areas, but the manipulator has to reach those goal areas in the order: visit `goal 1` first, then `goal 2`, and last to `goal 3`, but `goal 1` needs to be avoided before reaching `goal 3`.

_images/moti-arm.png

two-link manipulator

In this example, the specification is very high-level compared to conventional control objectives. No initial state is specified and there might be disturbance during the mission execution.

To solve such problems, ROCS utilizes temporal logic formulas to describe the control objective and formal algorithms to synthesize a feedback controller. As opposed to posteriori control methods, formal methods are now more favorable for safety-critical systems because

  • the set of initial conditions, where feedback controllers exist to realize the specification, (a.k.a. winning set) can be computed,

  • a feedback controller will be determined for each state in the winning set,

  • the synthesized controllers are correct by construction, and

  • control synthesis can be performed automatically.

Getting Started

To start your experience with ROCS, you may want to follow these steps:

Why ROCS?

ROCS is able to deal with general nonlinear dynamics and a class of LTL formulas that can be translated into deterministic Buechi automata (DBA). Dealing with DBA is more practical in nonlinear control synthesis. Synthesizing a full LTL specificaiton for a nonlinear system is usually cost prohibitive in time and space.

Features

  • It provides two control synthesis engines (see Methodology for further details):

    • Abstraction-based engine: a commond method used in other tools (e.g., SCOTS, TuLip). The version implemented in ROCS is optimized in both time and space.

    • Specification-based engine: only available in ROCS, which is generally much more memory efficient than the abstraction-based engine.

  • It supports control synthesis with respect to LTL formulas that can be translated into deterministic Buechi automata (DBA);

  • It supports control synthesis for sampled-data systems by incoporating Taylor models of ODE solutions. No analytical bounds, e.g., growth functions, are needed.

  • It provides Python and Matlab APIs for simulating control synthesis results.

ROCS Architecture

_images/architecture.png

How to choose a solver engine?

For low dimensional systems (<= 2d), simple dynamics, and simple LTL specifications such as invariance and reachability, both engines performs similarly.

For higher dimensional systems with more complicated dynamics and

  • choose the abstraction-based engine if

    • you have enough memory,

    • no varying discretization precision needed according to the dynamics.

  • choose the specification-guided engine if

    • you have limited memory,

    • system dynamics has distinct fast and slow flows in different areas in the state space.

The following performance test on benchmarks [ROCS2021] 1 may serve as a reference for choosing the engine. The table summarizes the runtime and memory test results of examples: aircraft safe landing [RWR2017], DCDC converter [ROCS2018], [LL2018], inverted pendulum stabilization [LL2020], Moore-Greitzer engine operation point control [LSL2021], mobile robot [LSL2021], and SCARA manipulator motion planning [LSL2021]. The run time for abstraction-based method is the sum of the time for abstraction and synthesis. All examples were tested on the high performance computing (HPC) cluster Beluga for benchmarking examples. Every test runs sequentially on a node with Intel Xeon(R) Gold 6148 processor @2.40GHz. Each node is allocated a maximum of 750GB of memory.

_images/perftest.png

performance test on benchmarks [ROCS2021]

For the mobile robot, \(\varphi_1=\lozenge(a_1\wedge\lozenge(a_2\wedge\lozenge(a_3\wedge(\neg a_2)\mathbf{U} a_1)))\), \(\varphi_2=\bigwedge_{i=1}^{3} \Box\lozenge a_i\), and \(\varphi_3=\bigwedge_{i=1}^{3}\lozenge a_i\). For the SCARA manipulator, \(\varphi_{\rm gb}=\Box\lozenge g_1\wedge\Box\lozenge g_2\).

Indices and tables

Footnotes

1

The memory used in DCDC converter example is unable to be collected due to short run time. OFM = out of memory, OFT = >24h.

ROCS2018

Y. Li, J. Liu, ROCS: A Robustly Complete Control Synthesis Tool for Nonlinear Dynamical Systems. In Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (HSCC ‘18).

ROCS2021

  1. Li, Z. Sun, and J. Liu (2021), ROCS 2.0: An Integrated Temporal Logic Control Synthesis Tool for Nonlinear Dynamical Systems. 7th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2021).

RWR2017

Reissig, G., Weber, A., and Rungger, M. (2017). Feed-back refinement relations for the synthesis of symboliccontrollers. IEEE Trans. Automat. Contr., 62(4), 1781–1796.

LL2018

Y. Li, J. Liu (2018), Invariance Control Synthesis for Switched Nonlinear Systems: An Interval Analysis Approach. IEEE Trans. Automat. Contr., 63(7), 2206-2211.

LL2020

Y. Li, J. Liu (2020), Robustly Complete Synthesis of Memoryless Controllers for Nonlinear Systems with Reach-and-Stay Specifications. ArXiv: 1802.09082v2.

LSL2021(1,2,3)

Y. Li, Z. Sun, and J. Liu (2021), A Specification-Guided Framework for Temporal Logic Control of Nonlinear Systems. ArXiv:2104.01385

LSL2021iros

  1. Li, E.M. Shahrivar, J. Liu (2021), Safe Linear Temporal Logic Motion Planning in Dynamic Environments. Accepted by 2021 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2021).