Another two tools, to complement the one suggested by Neel, are muCRL and mCRL2. 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 modal mu calculus, 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.

Another two tools, to complement the one suggested by Neel, are muCRL and mCRL2. 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, 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.

Another two tools, to complement the one suggested by Neel, are muCRL and mCRL2. 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 again Hennessy-Milner logic. Other useful tools allow you to perform state space reduction modulo bisimulation to get the smallest representation of your system.

Another two tools, to complement the one suggested by Neel, are muCRL and mCRL2. 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 modal mu calculus, 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.