Non Standard Hybrid Automata Semantics Candidate:

To my grandmother Annetta. Hybrid automata are suitable mathematical models to the description of systems characterized by the interaction between discrete and continuous components. Their application finds space in major research areas, as control theory and bioinformatics. System verification process can be translated in terms of reachability problem over hybrid automata. Unluckily, this problem is source of undecidability. In the following thesis work, we present and compare two different techniques able to circumvent the undecidability related to the reachability problem of hybrid automata: the first is based on the definition of an algorithm which exploits a particular category of approximated semantics, the second recurs to the concept of noise introduction into hybrid automata. The notion of noise will be redefined in terms of approximation semantics, thus making possible the direct comparison with the approximated semantics of the first approach. The detailed study of the proposed techniques, in addition to establish whic