FaPAS/FFaPAS: Formal Analysis of Piecewise Affine Systens

Introduction

The software tools FaPAS (“Formal analysis of Piecewise Affine Systems”) and FFaPASFormula-guided Formal analysis of Piecewise Affine Systems”) were developed for analyzing piecewise affine (PWA) systems from linear temporal logic (LTL) specifications. Specifically, given a PWA system and an LTL specification, both tools search for the largest region of initial conditions, from which all system trajectories satisfy the specification. These tools implement methods that lead to provably correct results but are computationally expensive and, in general, conservative.

The tool FaPAS implements a method based on the iterative computation and model checking of finite simulation quotients of PWA systems – an approach inspired by the “bisimulation algorithm”. In FFaPAS on the other hand, a formula-guided abstraction refinement method is implemented based on conditions guaranteeing the equivalence of an infinite (PWA) system and its finite quotient with respect to a specific temporal logic formula only. For both methods, quotient refinement is used to improve the solution which is, in general, conservative but, due to the various optimizations, in many cases FFaPAS is capable of computing a solution with comparable quality faster than FaPAS.

Download

Current version
download FaPAS/FFaPAS package

Previous versions:
download FFaPAS
download FaPAS

Installation

Coming soon

Dependencies

FaPAS and FFaPAS use the following external packages:
MPT Toolbox (Polyhedral operations)
ltl2ba (LTL to Buchi automata translation)

Quick start

Coming soon

Related literature

– B. Yordanov, J. Tumova, C. Belta, I. Cerna, J. Barnat, Formal analysis of piecewise affine systems through formula-guided refinement, In 49th IEEE Conference on Decision and Control (CDC), 2010. (pdf)
– B. Yordanov, C. Belta, Formal Analysis of Discrete-Time Piecewise Affine Systems, In IEEE Transactions on Automatic Control, volume 55, 2010.(pdf)
– B. Yordanov, C. Belta, Formal analysis of Piecewise Affine systems under parameter uncertainty with application to gene networks, In Proceedings of the American Control Conference (ACC), 2008 (pdf)
– B. Yordanov, G. Batt, C. Belta, Model checking discrete time piecewise affine systems: application to gene networks, In European Control Conference (ECC), 2007. (pdf)