ARCS

August 6, 2018 ยท View on GitHub

Toolbox in development for abstraction-refinement-based incremental synthesis of correct-by-construction switching protocols.

Functionality

  • Synthesis methods for augmented finite transition systems.
  • Abstraction tools based on hyper boxes.
  • Demonstrating examples.

Requirements

  • Matlab (2015b or newer recommended)
    • Communications Systems Toolbox
  • Yalmip and a supported solver is required for semidefinite optimization, tested version R20160930.
  • Mosek for conic optimization, tested with version 8.
  • arrow.m for certain plotting.
  • Windows 64bit and Linux 64bit for BDD support (so far) or MATLAB mex compiler to compile mex function

Usage

Add the folder abstr-ref to the Matlab path: addpath /path/to/abstr-ref.

Run tests:

cd tests/
runtests

Run an example:

cd examples_2017/
radiant

Recompile mex files

If for some reason the pre-compiled mex files do not work, run the script compile_mex in the mex_files folder. This should create a new mex file that can be moved to the abstr-ref/ folder.

Authors

Petter Nilsson, Caltech, pettni@caltech.edu

Necmiye Ozay, University of Michigan

Oscar Lindvall Bulancea, KTH

Todo list

  • Update old examples in examples/ to work with new software
  • Add custom sos through PolyLinTrans
  • Class for semialgebraic partition/sets (c.f. hyperplane arrangement)
  • Additional tests
    • Dual algorithms
    • Control strategies
    • Candidate sets
    • System-level test
  • Improve documentation
  • Write custom SOS optimization to avoid overhead (translate python socp impl.)
  • Improve documentation and type security of mex code

References

  • P Nilsson and N Ozay, "Incremental Synthesis of Switching Protocols via Abstraction Refinement", Proc. of IEEE CDC, 2014.
  • P Nilsson, N Ozay and J Liu, "Augmented Finite Transition Systems as Abstractions for Control Synthesis", Journal of Discrete Event Dynamic Systems (Special issue on Formal Methods in Control), 2017.
  • O B Lindvall, P Nilsson and N Ozay, "Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings", in Proceedings of the IFAC Conference on Analysis and Design of Hybrid Systems, 2018

Acknowledgments:

This research is supported in part by DARPA grant N66001-14-1-4045.