pyHybridAnalysis is a python package to both represent and analyze hybrid automata. It exploit the -semantics framework developed in [CPP08] 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 -semantics in place of the standard one, the termination condition eventually holds (e.g., see [CPP09,CDP12]). In particular cases, the evaluation of -semantics themselves can be reduced to the evaluation of the standard semantics. For instance, whenever the formula 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 are definable in the Tarski’s theory and the corresponding formulae can be obtained from itself by applying the opportune syntactic translation. Moreover, since the Tarski’s theory is decidable, the above described algorithm is computable.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element