Abstract: This paper reduces the satisfiability of noninterference to the solution of a finite set of equations. We use the structure of labelled transition systems, which are the basis for state machines and process algebras, to explicitly model the relationship between states, actions, and outputs. The output constraint equations are developed by constructing a predicate for nondeterministic systems and expressing noninterference as an invariance property of the predicate. The finiteness of the equations comes from a closure property of the predicate and the use of finite state machines.