Formal analysis of real-time equational rule-based systems

A study is made of the real-time performance of a class of rule-based programs written in the language EQL. Response time is defined in terms of the computation paths of a program leading to fixed points; investigated is the complexity of the problem of analyzing these programs to meet response-time requirements. It is shown that the response-time analysis problem is in general undecidable and is PSPACE-hard in the case where all the variables have finite domains. A general analysis strategy which seems to be quite effective in practical cases is proposed. This strategy aims at avoiding the combinatorial state-space explosion problem inherent in brute-force approaches. Based on this strategy, a suite of analysis tools has been implemented to verify that the variables in an EQL program always converge to stable values in bounded time. The tools have been successfully applied to real-life programs