Pessoa 2.0

Abstract

We introduce PESSOA 2.0, a tool that automatically synthesizes controllers for cyber-physical systems based on correct-by-design methodology. PESSOA 2.0 accepts a cyber-physical system represented by a set of smooth differential equations and automata and a specification in a fragment of Linear Temporal Logic that is expressive enough to describe interesting properties but simple enough to avoid Safra's construction. It outputs, if possible, a controller for the system that enforces the specification up to an abstraction parameter. We report on examples illustrating the expressiveness of the fragment and the controllers synthesized by the tool.