P||Q represents concurrent execution of P and Q. || is the parallel composition operator
LTSA is not the best solution for this, use Elementary Petri Net