Towards a feature mu-calculus targeting SPL verification M.H. ter Beek, E.P. de Vink and T.A.C. Willemse The modal mu-calculus muL is a well-known fixpoint logic to express and model check properties interpreted over labeled transition systems. In this paper, we propose two variants of the mu-calculus, muLf and muLf', for feature transition systems. For this, we explicitly incorporate feature expressions into the logics, allowing operators to select transitions and behavior restricted to specific products and subfamilies. We provide semantics for muLf and muLf' and relate the two new mu-calculi and~$\muL$ to each other. Next, we focus on the analysis of SPL behavior and show how our formalism can be applied for product-based verification with muLf as well as family-based verification with muLf'. We illustrate by means of a toy example how properties can be model checked, exploiting an embedding of muLf' into the mu-calculus with data.