Automated System Property Verification (for ECE301: "signals and systems")

Overview

For those who are CS geeks like William, the question of whether a function to check whether a system has a given property can be written is very pertinent. I have been looking into symbolic math solvers to try to make them do this.

So far, my most promising lead is the AXIOM solver [1], which might have a LISP interface to its symbolic math engine. This would be ideal.

My notes so far are as follows:

Basics: Systems as "functions that operate on functions"

A system can be represented as a function system(x), where x is some function x(t), that returns another function of the form y(t).

In Common LISP, an example of x might be:

(setq x (lambda (tt) (+ tt 5)))

This corresponds to x(t) = t + 5. t is a reserved constant in LISP, so I use tt. A setq here probably isn't the "right way" to do things, but LISP is not my native language.

At any rate, a simple system to play with would be a time shift. You would represent this as follows (note the extra argument to, representing the amount of time to shift by):

(defun timeshift (x to) (lambda (tt) (funcall x (- tt to))))

You can then represent x(t) -> [Shift by to]? -> y(t) as (in more broken LISP):

(setq y (timeshift x 'to))

At this point, you could in theory make a call

(funcall y tt)

to get y(tt) = x(tt - to) = tt + 5, but LISP doesn't do symbolic math natively. Thus, some work needs to be done to get AXIOM or some other engine to do the heavy lifting.

An example using clisp, with commentary:

(setq x (lambda (tt) (+ tt 5)))  ; x(tt) = tt + 5 (defun timeshift (x to) (lambda (tt) (funcall x (- tt to))))  ; Define the time-shift function

Apply the timeshift to x with to=15.

This is akin to y(t) = x(t - 15) = t - 15 + 5 = t - 10

(setq y (timeshift x 15))

Finally, compute a value of y(t)

y(3) = 3 - 10 = -7

(funcall y 3)

Again, the lack of native symbolic math operations in LISP is extremely limiting, so a symbolic engine needs to be integrated somehow.

Testing properties

As you can see, using LISP to model systems is potentially a powerful method. The "functions operating on functions" way of thinking can be extended even further to the "system" functions (such as timeshift above) to prove things about systems.

Lacking a good symbolic solver, I cannot test the following code yet, but we might write a function "linear" that determines whether the given system function is linear or not.

(defun islinear (sysfunc)

  (let ((y1 (funcall sysfunc 'x1))     ; Define y1 = sysfunc(x1), y2 = sysfunc(x2)
        (y2 (funcall sysfunc 'x2)))
   (eq
    (+ (* 'a (funcall y1 'tt))         ; a*y1(t) + b*y2(t) = ...
       (* 'b (funcall y2 'tt)))
    (funcall 
     (funcall sysfunc
                                       ; ... = sysfunc(a*x1(t) + b*x2(t))(t) ?
              (lambda (tt) (+ (* 'a (funcall 'x1 tt))
                              (* 'b (funcall 'x2 tt))))
              ) 'tt)
    )))