Description: |
conPAS/conPAS2: Temporal logic control of Piecewise Affine Systems. 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. conPAS consists 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. |