Formal verification of concurrent systems via directed model checking