Finite-state concurrent programs can be expressed succinctly in triple normal form

If (1) action guards are in disjunctive normal form, or are short, i.e., of size logarithmic in the size of P, and (2) the number of shared variables is logarithmic in the size of P, then the triple normal form program has size polynomial in the size of P, and the transformation is computable in polynomial time.