Start Using MTSA

Download the latest stable release from mtsa.dc.uba.ar.

You can run the application using Java 11 JRE or later. If you try to run and nothing happens, make sure the downloaded JAR has its executing bit enabled.

Once MTSA is loaded you can use some of the examples in the menu option File > Open Examples.

A good starting point for modelling and analysis, and also some help with the tool is the book Concurrency: State Models & Java Programs by Jeff Magee & Jeff Kramer and its associated website.

If you want to define your own examples, check the following sections:

• Parse, Compile and Compose. A tiny example.
• FSP language options
• Fluents & LTL
• Supervisory Control
• Reactive Synthesis
• DCS