An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.
Similar to the set checker, it should be possible for the BDD checker to detect when no further depth is necessary. This can be implemented by keeping the previous depth of BDD and checking whether extending it by one more step changes the BDD or not.
Similar to the set checker, it should be possible for the BDD checker to detect when no further depth is necessary. This can be implemented by keeping the previous depth of BDD and checking whether extending it by one more step changes the BDD or not.