What are practically computable properties of Labelled Transition Systems?
The formulas of Hennessy-Milner logic are very easy to prove about labelled transition systems. However, this logic is inexpressive enough (there is no way to state properties of infinite paths) that you will probably wish to consider some extension to it, such as linear temporal logic. LTL has a decidable, but PSPACE-complete, problem. 

The SPIN model checker is a widely-used tool for model-checking LTL properties.