Toolbox in development for abstraction-refinement-based incremental synthesis of correct-by-construction switching protocols.
- Synthesis methods for augmented finite transition systems.
- Abstraction tools based on hyper boxes.
- Demonstrating examples.
- 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
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
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.
Petter Nilsson, Caltech, [email protected]
Necmiye Ozay, University of Michigan
Oscar Lindvall Bulancea, KTH
- 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
- 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
This research is supported in part by DARPA grant N66001-14-1-4045.
