Abstract:
In the model checking of linear hybrid systems, the implementation of parameteric analysis depends on maintaining the parameters in symbolic form. In this direction, parametric variables can be kept with the system variables, or stored and considered separately. The first method is usually used because it is easy to implement, but it restricts the descriptive capability of the system. By analyzing the symbolic model checking process, we choose to store the parametric variables separately in symbolic form and we give a model checking algorithm for this description. As an example, the limit to clock skew in a Fischer mutex system is analyzed.