conPAS

conPAS/conPAS2: Temporal Logic Control of Piecewise Affine Systems

Description: conPAS is a computational tool for automatic synthesis of feedback control strategies for a piecewise affine (PWA) system from specifications given as Linear Temporal Logic (LTL) formulas. conPASconsists of two main steps: First, by defining appropriate partitions for its state and input spaces, it construct a finite abstraction of the PWA system in the form of a control transition system. Second, by leveraging ideas and techniques from Buchi games and qualitative probabilistic LTL model checking, it generates a control strategy for the finite abstraction. The tool conPAS handles only specifications that can be expressed as deterministic Buchi automata, while its extension conPAS2 can handle arbitrary LTL formulas through a translation to deterministic Rabin automata. While provably correct and robust to small perturbations in both state measurements and applied controls, both procedure are conservative and expensive.

VO Integration: No

Active: No

Available Benchmarks: N/A

Website: http://sites.bu.edu/hyness/conpas2/

Download: Links can be found on the website homepage.

Documentation: The tool comes with examples. There are also links to relevant papers on the website homepage.

Contact: N/A