  The two major systems of formal verification are model checking and algebraic
model-based testing. Model checking is based on some form of temporal logic
such as linear temporal logic (LTL) or computation tree logic (CTL). One
powerful and realistic logic being used is CTL, which is capable of expressing
most interesting properties of processes such as liveness and safety.
Model-based testing is based on some operational semantics of processes (such
as traces, failures, or both) and its associated preorders. The most
fine-grained preorder beside bisimulation (mostly of theoretical importance) is
based on failure traces. We show that these two most powerful variants are
equivalent; that is, we show that for any failure trace test there exists a CTL
formula equivalent to it, and the other way around. All our proofs are
constructive and algorithmic. Our result allows for parts of a large system to
be specified logically while other parts are specified algebraically, thus
combining the best of the two (logic and algebraic) worlds.
