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

• Parameter synthesis
• Hybrid branching-time temporal logic
• Dynamical systems
• Piecewise multi-affine dynamical systems
• Differential equations

Type of tool

Parameter synthesizer

Expected input

• Parametrised model of a continuous-time dynamical system
• Desired properties, expressed in a hybrid extension of the UCTL logic, $HUCT{L}_P$

Format:

• Parametrised model: own .bio format
• Properties: own .huctl 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 $HUCT{L}_P$ formula, it computes all parameter valuations under which the PDTS satisfies the formula.

Comments

License: GPL v3.0