conPAS/conPAS2: Temporal logic control of Piecewise Affine Systems

Introduction

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.

Download

Current version
download conPAS2 (beta)

Previous versions:
download conPAS2 for Linux only (beta)
download conPAS2 for Linux with all dependencies (beta)
download conPAS

Installation

1) Download the conPAS or conPAS2 package
2) If downloading conPAS2 only (no dependencies as in the newest available version)
   a) download the required external toolboxes (specifically, MPT) and
   b) link and initalize the toolboxes (addpath(genpath(path_to_mpt)); mpt_init)

Dependencies

ConPAS2 uses the following external packages:
MPT Toolbox (Polyhedral operations)
Graphviz (Visualization)
ltl2dstar (LTL to Rabin automata translation)
ltl2ba (LTL to Buchi translation. Used by ltl2dstar)

Quick start

1) Set conPAS paths (from conPAS root folder, use ‘>>addpath(genpath(‘.’))’)
2) Load a PWA system
3) Load an LTL specification (encoded directly as a Rabin automaton)
4) Run conPAS or conPAS2 (eg. “conPAS2”)

See genes_example1, genes_example2, tanks_example for examples

Related literature

– J. Tumova, B. Yordanov, C. Belta, I. Cerna, J. Barnat. A symbolic approach to controlling piecewise affine systems, In 49th IEEE Conference on Decision and Control (CDC), 2010. (pdf)
– B. Yordanov, C. Belta. Temporal logic control of discrete-time piecewise affine systems, In Proceedings of the 48th IEEE Conference on Decision and Control, 2009 held jointly with the 2009 28th Chinese Control Conference. CDC/CCC., 2009. (pdf)
– B. Yordanov and C. Belta. Temporal logic control of discrete-time piecewise affine systems. Technical Report 2009-IR-0120, Boston University (CISE), 2009.
– M. Kloetzer and C. Belta, A Fully Automated Framework for Control of Linear Systems From Temporal Logic Specifications, IEEE Transactions on Automatic Control, vol. 53, no.1, pp. 287-297, 2008. (pdf)
– M. Kloetzer and C. Belta, Dealing with non-determinism in symbolic control, Proceedings of HSCC 2008, Lecture Notes in Computer Science, Springer, eds. M. Egerstedt and B. Mishra, vol. 4981, pp. 287-300, 2008. (pdf)