Response time analysis of EQL real-time rule-based systems

Real-time rule-based expert systems are embedded decision systems that must respond to changes in the environments within stringent timing constraints. Given a program p, the response time analysis problem is to determine the response time of p. This problem consists of: determining whether or not the execution of p always terminates in bounded time; and computing the maximal execution time of p. The Equational Logic (EQL) language is a simple language designed for real-time applications. It has been proved by A.K. Mok (1989) that the response time analysis problem is undecidable if the program variables have infinite domains, and is PSPACE-hard in the case where all of the variables have finite domains. However, we have observed that the use of a simple syntactic and semantic check on programs coupled with other techniques such as state space graph checks can dramatically reduce the time needed in the analysis. There are sets of syntactic and semantic constraint assertions such that if the set S of rules satisfies any of them, then the execution of S always terminates in bounded time. Each of these sets of syntactic and semantic constraint assertions is called a Special Form. The focus of the paper is on proving the existence of two Special Forms and determining tight response time upper bounds of EQL rule-based programs. For each known Special Form, an algorithm used to calculate the maximal response time of programs satisfying this Special Form is presented. Additionally, to enhance the applicability of the proposed algorithms, we show how the General Analysis Algorithm can be used with these algorithms