FaPAS

FaPAS/FFaPAS

Description: The software tools FaPAS ("Formal analysis of Piecewise Affine Systems") and FFaPAS "Formula-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.

VO Integration: No

Active: Yes

Available Benchmarks: No

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

Download: Link

Documentation: No manual. The webpage provides links to some reference papers.

Contact: BU Robotics Lab, contact form

Excerpt from: http://sites.bu.edu/hyness/fapas/