What are practically computable properties of Labelled Transition Systems? I found labelled transition systems to be a good model for my application, namely there is a paper about modeling use cases using LTSs. The question is, what can be easily proven about LTSs? I would like to re-use existing solutions to see if they are useful for my appication. I would like to know what properties of LTSs (and use cases) can be easily automatically proved, so I can decide, if there is a practical counterpart to the problem for use cases.
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.