A Python Package for the $\epsilon$-Semantics Analysis of Hybrid Systems

pyHybridAnalysis is a Python package to both represent and analyze hybrid automata. It exploit the $\epsilon$-semantics framework developed in [CPP09] to reduce the reachability problem over hybrid automata to the satiability problem of a formula in the opportune theory.
Automata are logic-based and their are defined as described in [CPP09]. Starting with the empty path and increasing its length at each step, the algorithm builds the first-order formula corresponding to the evolution of the automaton through all the bounded length path. Whenever the set of states that are reached for the first time in the last step is empty, the computation ends and the reach set is returns.
In the general cases, we may not guarantee the algorithm termination and there exist automata whose reach sets grow as the path lengths increase. However, if we bound the invariants and interpret formulae by using an $\epsilon$-semantics in place of the standard one, the termination condition eventually holds (e.g., see [CPP09,CDP12]).
In particular cases, the evaluation of $\epsilon$-semantics themselves can be reduced to the evaluation of the standard semantics. For instance, whenever the formula $\varphi$ belongs to the Tarski's theory (i.e., is a first-order formula involving polynomials), the sphere semantics, the bottom semantics, and the easy semantics of $\varphi$ are definable in the Tarski's theory and the corresponding formulae can be obtained from $\varphi$ itself by applying the opportune syntactic translation. Moreover, since the Tarski's theory is decidable, the above described algorithm is computable.

[CPP09] Discrete Semantics for Hybrid Automata, A. Casagrande, C. Piazza, A. Policriti, Journal Discrete Event Dynamic Systems, 19(4), 471-493. December 2009.
[CPP12] Hybrid Automata and $\epsilon$-Analysis on a Neural Oscillator, A. Casagrande, T. Dreossi, C. Piazza, Proceedings of Hybrid Systems in Biology (HSB 2012), EPTCS 92, 2012, 58-72. September 2012.

Examples

Building a formula

Evaluating the $\epsilon$-semantics of a formula

Eliminating quantifier from a formula in Taski's theory

Building a hybrid automaton

Analyzing a hybrid automaton

Downloading and Installing

In order to use pyHybridAnalysis, you must have already installed:
  • the python package ply
  • a working copy of Reduce/Redlog. Download and install it as described here. The command line reduce should be in the path.
  • (Optional) QEPCAD B and SLFQ.
Download the tar file containing all the pyHybridAnalysis code and decompress it. Enter the directory pyHybridAnalysis and import pyHybridAnalysis from the python interpreter to use the package.

An easy-to-use system-wide installer and full API documentation will be soon available.
The pyHybridAnalysis code is released under the LGPL GNU license v3.