Abstract
Equivalence checking for finite state systems is well studied and many algorithms exist that can determine whether or not two finite state systems are equivalent. Analysing infinite state systems is very complex. Infinite state systems can be modeled as Hybrid Systems, that have discrete and continuous behaviours that describe the hybrid state. Many methods for checking equivalence between two Finite State Systems exist. However, for infinite state systems, this traditional crude definition of equivalence is too constrained. A more effective equivalence definition is one that is best expressed in terms of features or behavioural signatures of the infinite state systems. Behavioural aspects used for feature comparison can be expressed as a linear combination of state variables. For a given Hybrid Automaton, the range of values taken on by a specific feature aspect can be obtained by observing the state space of the Hybrid System reachable from an initial state. However, we cannot directly apply the traditional reachability analysis to determine feature based equivalence. This report formalizes the notion of feature based reachability analysis of Hybrid Systems and describes feature driven modifications required to prepare the given Hybrid Automata for feature based equivalence checking
To download my thesis Click Here