Another two tools, to complement the one suggested by Neel, are [muCRL][1] and [mCRL2][2]. Both toolsets have quite a range of tools for defining LTS at various levels of abstraction. State space visualisation and model checking tools are also available. The underlying logic is the [propositional modal mu calculus][3], which is much more expressive than LTL, yet still decidable. Other useful tools allow you to perform state space reduction modulo bisimulation to get the smallest representation of your system. 


  [1]: http://homepages.cwi.nl/~mcrl/mutool.html
  [2]: http://www.mcrl2.org/mcrl2/wiki/index.php/Home
  [3]: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.143.9834&rep=rep1&type=pdf