Logic Verification for Ladder Diagrams

I have to do a project on verification of ladder diagram.
Its supposed to be a binary logic verification.

I am supposed to come up with some test cases that prove the logic on a ladder diagram could be in a conflict.

Example (assuming that all inputs and outputs are binary)
-------

CASE 1
------
- the most obvious and simple one

x ^ ~x -> y


CASE 2
------
- 2 same inputs giving opposite results
- or 2 completely opposite inputs to give same output

x ^ y -> z
x ^ y -> ~z

OR

x ^ y -> z
~x ^ ~y -> z


CASE 3
------

a -> b
~b -> a

OR

~a -> b
b -> a



CASE 4
------
- indirect conflict
(since x is a subset of b it cannot be used in conjunction with a ~b)

b ^ ~y -> x
~b ^ x -> w



Has anyone done something similar on these lines.
If there are more test cases that I have missed out.
And if these test cases are correct?

Thanks again.

-teddi

There was a paper written on detecting race conditions in ladder logic. I don't know if it will help you, but you might find it interesting. Check out: http://www.cs.ucdavis.edu/~su/publications/sttt00.pdf

Thanks !

I will look into that.