Freedom, Weakness, and Determinism: From Linear-time to Branching-time
----------------------------------------------------------------------

Model checking is a method for the verification of systems with
respect to their specifications.  Symbolic model-checking, which
enables the verification of large systems, proceeds by calculating
fixed-point expressions over the system's set of states.  The
$\mu$-calculus is a branching-time temporal logic with fixed-point
operators. As such, it is a convenient logic for symbolic
model-checking tools.  In particular, the alternation-free fragment of
$\mu$-calculus has a restricted syntax, making the symbolic evaluation
of its formulas computationally easy. Formally, it takes time that is
linear in the size of the system.  On the other hand, specifiers find
the $\mu$-calculus inconvenient.  In addition, specifiers often prefer
to use linear-time formalisms.  Such formalisms, however, cannot in
general be translated to the alternation-free $\mu$-calculus, and
their symbolic evaluation involves nesting of fixed-points, resulting
in time complexity that is quadratic in the size of the system.  In
this paper we characterize linear-time properties that can be
specified in the alternation-free $\mu$-calculus.  We show that a
linear-time property can be specified in the alternation-free
$\mu$-calculus iff it can be recognized by a deterministic B\"uchi
automaton.  We study the problem of deciding whether a linear-time
property, specified by either an automaton or an LTL formula, can be
translated to an alternation-free $\mu$-calculus formula, and describe
the translation, when exists.