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

Format:

Expected output

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

Internals

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.

Comments

License: GPL v3.0
Synthesis

Links

Last commit date

15 December 2020

Related papers

https://doi.org/10.1007/978-3-319-63387-9_29 (CAV '17)

Last publication date

13 July 2017

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.