PV2 Pithyaprovide a set of parameter valuations to satisfy the given formula on a given dynamical system

Tool for parameter synthesis of piecewise multi-affine dynamical systems from specifications expressed in a hybrid branching-time temporal logic.

Application domain/field

Type of tool

Parameter synthesizer

Expected input


Expected output

Set of all parameter valuations under which the system satisfies the formula.


Pithya takes as input a parametrised model of a continuous-time dynamical system. This system is described by autonomous ordinary differential equations (ODEs) with sigmoidal functions. Pithya then approximates this model into a piecewise multi-affine model and discretises it into a parametrised direction transition system (PDTS). Using the computed PDTS and the HUCTLP formula, it computes all parameter valuations under which the PDTS satisfies the formula.


License: GPL v3.0


Related papers

Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-affine Dynamical Systems (CAV '17)

Last publication date

13 July 2017

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.