On Relative and Probabilistic Finite Counterability
Formal Methods in System Design, Volume 52, Issue 2, 2018, Pages 117-146.
A to the satisfaction of a linear property in a system is an infinite computation of that violates . When is a safety property, a counterexample to its satisfaction need not be infinite. Rather, it is a for : a finite word all whose extensions violate . The existence of finite counterexamples is very helpful in practice. Liveness pr...More
Full Text (Upload PDF)
PPT (Upload PPT)