Ariadne: An open tool for hybrid system analysis

Ariadne is a library for computation with hybrid automata under development by a joint team including University of Udine, PARADES, CWI, and University of Verona.

The goal is to build an open and easily extensible package that features basic data structures and operators to support analysis and synthesis of systems described with hybrid automata. The ARIADNE computational kernel is written using generic programming, in which mathematical concepts, such as real numbers and continuous functions, can be implemented by different concrete types presenting the same (or similar) interfaces. In this way, we can write algorithms which work with any type having the same interface, and even if a type does not implement the full interface, some algorithms may still be available for that type. The advantage of this approach is that it greatly facilitates extensions: new types can be freely added as long as they conform to the syntax and semantics of the concept; new algorithms can be plugged-in to work with the new types, and user-defined algorithms can replace the algorithms supplied with the tool.

The project site can be reached from
this link.


Matchfinder is a GPL program to compute a maximal matching of a graph.

A graph or undirected graph G is an ordered pair <V,E>, where:
  • V is a set of objects, called vertices
  • EV×V is a set of pairs of distinct vertices, called edges
A matching of a graph G is a set of pairwise non-adjacent edges of G. A maximal matching for G is a matching of maximum cardinality with respect to G.Notice that there can be many different maximal matchings for a single graph. For instance, the graph G=<V={1,2,3},E={<1,2>,<2,3>}> has two maximal matchings: M={<1,2>} and M={<2,3>}.


LadderFinder is a GPL program designed to solve a problem in DNA genotyping. It helps in the construction of allelic ladders that drive the sizing and binning of SSR fragments produced by PCR. The algorithm scans a spreadsheet containing a database of individual profiles and finds a minimum set of individuals, that covers the maximum number of alleles represented in the database, with all alleles represented only once. The last constraint is imposed to make homogeneous the ladder peaks in the pherograms. Given such a constrain, the best solution may not include all alleles.

LadderFinder consists of two components: a graphical interface and a program kernel. The graphical interface is written in JAVA be portable, while the program kernel, called matchfinder, is written in C++ for efficency purpose.


ProPesca is a simple Java application for the analysis and identification of gene expression networks. ProPesca takes in input shorts temporal series of RT-PCR gene expression levels and allows to cluster genes which exhibit either similar or specular behaviours.

GAM (Genome Assembly Merger)

GAM is a free parallel software tool to integrate two different assemblies and improves the overall quality of the genome sequences by merging them. It discovers and align similar sequences by using the positions of placed reads. An order sequence of reads contiguous on the same contig is called frame. When the same frame is shared by both original assemblies, GAM dubs it block.

GAM deduces block orders from assembly read orders and, by using them, builds a graph of assemblies whose nodes represent blocks and whose edges represents block order. Since cycles in the graph of assemblies denote conflicting block order in assemblies, GAM avoid to merge sequences containing blocks belonging to them.

BLOSpectrum Tools

BLOSpectrum tools are command line applications to analyze and classify protein sequences with respect to SCOP. They are based on the concept of fingerprint: an information theoretic model which summarizes the relations between sequences in a set and provides a visual representation of the general characters of the set itself. The development of BLOSpectrum tools is supported by University of Trieste.

The project site can be reached from this link.


PolyMorph is a P300-based speller that exploits the redundancies of natural languages to increase the spelling efficiency.


The most visible feature of PolyMorph is the word suggestion. In fact, it uses a knowledge base to identify the words that are most likely to be spelled by the user by observing what the user himself has already written. The words are then suggested and can be spelled with just one selection. While this idea is not new, PolyMorph differs from the spellers presented in the literature because its speller matrix changes both in sizes and composition according to what has already been spelled. For instance, if the string "qup" begins none of the words stored in the PolyMorph knowledge base and the user has already spelled "qu", then the speller avoids to present the character "p". The development of PolyMorph is supported by University of Trieste.

The project site can be reached from this link.


pyHybridAnalysis is a python package to both represent and analyze hybrid automata. It exploit the $\epsilon$-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 $\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.

The development of pyHybridAnalysis is supported by University of Trieste, Univesity of Udine, and INdAM.