Automated Property Verification

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)
    )))

Properties of Systems

There are five general properties of systems that are introduced in this homework. These include systems with and without memory, time invariant systems, linear systems, causal systems and stable systems. This post will detail how to check if a system exhibits these general properties.

1. Systems with and without memory:

• Def: A system is said to be memoryless if its output for each value of the independent variable at a given time is dependent only on the input at that same time.

• Proving: This is very simple and can be done by visual inspection alone. If there is any kind of phase shift, the systems depends on values other than the input at that current time and is NOT memoryless. Also, if the system is described by an accumulator or summer again it depends of values other than the input at the current time and is NOT memoryless. Note that in a system comprised of the linear combination of sub-systems if any one of the sub-systems is memoryless than the entire system is memoryless.

2. Time Invariant Systems:

• Def: A system is time invariant if a time shift in the input signal results in an identical time shift in the output signal.

• Proving: In equation form, the system y(t) = x(t) is time invariant if y(t-to) = x(t-to). Plug in "t-to" for all "t's" in the system. Simplify. If the end result is just a time delay, then the system is time invariant. The easy way--if there are any "t's" outside the function x(t) [i.e. t*x(t)]? the system must NOT be time invariant.

3. Linear Systems:

• Def: A system is linear if any output can be derived from the sum of the products of an output and constant and another output and constant. In equation form for y(t) = x(t) with outputs y1, y2, and y3: $ y_3(t) = a\cdot y_1(t) + b\cdot y_2(t) $

• Proving: Use the equation above to prove. Example 1.17 in the text shows a nice overview. Basically, consider two arbitrary inputs and their respective outputs. A third input is considered to be a linear combination of the first two inputs. Write the output and substitute the third input for the linear combination. Separate the a and b variables. If you can arrange the equation so that the output of the third input is the linear combination of the first two outputs, then the system is linear.

4. Causal Systems:

• Def: A system is causal if the output at any time depends only on the values of the input at the present time and in the past.

• Proving: Consider each component of the system separately. If there is no time delay, the systems depends only on the present time and is causal. If there is a time delay, determine whether it is in past or future time. If it is past time, then the system is causal. When the systems is rotated over the y-axis [i.e. x(-t)]? then if is possible for some values of t that the system is in past time and for others in future. Determine these values. The system is causal for the values of past time as well as for the value of present time and else is NOT causal.

5. Stable Systems:

• Def: A system is stable if a bounded input function yields a bounded output function.

• Proving: Consider y(t) = x(t). If the input function is bounded then $ |x(t)| < \epsilon $. Consider the end behavior of all combinations of minimum and maximum values for x(t). If it is bounded, then y(t) IS stable. (Look at Example 1.13 in the text for further instruction).

... --brian.a.baumgartner.1, Wed, 05 Sep 2007 11:20:49

I was mistaken in article 4. Just because a system does not have a time delay does not PROVE that the system is causal. I wrote this without considering time scaling. I daresay that if a system does not have a time delay OR time scaling then it is causal; however I suggest doing the math to back this up. To find the values of when the system is causal and when it is not consider the system y(t) = x(at+b). Next set up the following inequality:

at+b <= t

The system IS causal as long as this inequality holds true. It is NOT causal for at+b > t.

Simplified View of Cascaded Systems

We talked in class about how, in a cascaded system, the "time coordinates" change and that you have to keep track of them as they propagate down the system through other transforms if you are trying to find the final output of the systems. This explanation seems somewhat confusing, so I tried looking at it in a different manor. It seems like we are trying to find the equation for the output by starting at the input, like a signal would, and writing all the transforms or "things" that happen to the signal using different variables, then we go back and substitute so it all works out. I did the reverse and started with the output and "built up" the total effect (output equation) from what happened "most recently" (that is to say the present is at the output and the input is the past), so you don't have to worry about keeping track of different substitution variables (Mimi used squares and squiggles) or the "time coordinates".

A very simple method is as such:

1. Start from the output, take the last transform and put it in parenthesis. It's in a nice package now, it's done, don't touch it.
2. Take that "package" and drop it right into the next "most recent" (one to the left) transform (substitute it for t). Put that in parenthesis, it's your new package.
3. Keep going until you run out of transforms.
4. If so inclined, simplify.

Example:

Sys 1: y1(t)= x(2t) Sys 2: y2(t)= x(t-3)

Input -> Sys 1 -> Sys 2 -> Output

Start from the output, take the "most recent" transform (Sys 2) and put it in parenthesis, so: (t-3)

Next, take the next most recent transform (Sys 1), and drop your (t-3) in it (substitute your "package" of (t-3) for t): 2(t-3)

Simplify: 2t-6

Done! Don't forget it is a transform of a function, not a function itself so you need to state so, as such: z(t) = x(2t-6)

So, put very simply, start at the output and substitute, in iterations, towards the input. That's all you really need to know, I just thought if I was verbose and used analogies I might score bonus points. Keep in mind the all the transforms deal with the independent variable, in this case time. Also, in the spirit of the kiwi, I could be completely wrong about everything. :) So seriously, someone check my work.

Determining the effects of Transforms of the Independent Variable (Time) in the form x(at + b) --michael.a.mitchell.2, Sun, 02 Sep 2007 12:20:52

If you are trying to find the effect of a transform in the form of x(at + b), you should:

1. Delay or advance x(t) by the value of b. (Advance if b>0, delay if b<0)
2. Then scale/reverse time by the value of a. (Compress if |a|>1, Stretch if |a|< 1, Reverse time if a<0)