摘要：AbstractThis paper introduces ROCS 2.0, a control synthesis tool for nonlinear systems with control objectives given as temporal logic formulas. In addition to the basic invariance, reachability, Büchi, and co-Büchi specifications that can be handled in the previous version of ROCS, ROCS 2.0 provides a major upgrade to support the general class of linear temporal logic formulas that can be translated to deterministic Büchi automata. Moreover, ROCS 2.0 not only maintains and accelerates the kernel of its previous version—the engine based on the specification-guided control method—by more efficient implementation, but also integrates a second engine that implements the abstraction-based control method, which is optimized to gain time and memory efficiency. Such a feature gives the user the freedom to choose the control synthesis method that is more suitable for a specific control problem.
关键词：KeywordsFormal methods in controlControl of constrained systemsTemporal logicverificationabstraction of hybrid systemsComputational tools
