The Modal Transition System Analyser

The Modal Transition Analyser (MTSA) is a research and teaching platform for modelling, analysis and synthesis of behaviour models represented as Labelled or Modal Transition Systems. MTSA is a research effort by the Laboratory on Foundations and Tools for Software Engineering (LaFHIS) at University of Buenos Aires The tool is a fork of the Labelled Transition System Analyser (LTSA) developed at Imperial College London initially by Jeff Magee. Additions to LTSA include multiple discrete event controller techniques, improvements in the GUI, and support for modal transition systems.

Downloads

Repository
MTSA jar file
How to install MTSA Guide

Projects

Directed Controller Synthesis for Non-Maximal Nonblocking Requirements


Dynamic Update of GR(1) Discrete Event Controllers


Assumption Monitoring Using Runtime Verification for UAV Temporal Task Plan Executions (ICRA 2021)


Business Process Reconfiguration


Update Controllers


Mission Planning and Runtime Adaptation

Ground Control

MTS Exploration


Selected Publications

2023

  1. Delgado, T., Sanchez Sorondo, M., Braberman, V., Uchitel, S. "Exploration Policies for On-the-Fly Controller Synthesis: A Reinforcement Learning Approach." Proceedings of the International Conference on Automated Planning and Scheduling (ICALP 2023), 33(1), 569-577.
  2. Ezequiel Pecker-Marcosig, Sebastián Zudaire, Rodrigo Castro, Sebastián Uchitel. "Correct and efficient UAV missions based on temporal planning and in-flight hybrid simulations." Robotics and Autonomous Systems (RAS), 2023, ISSN 0921-8890.
  3. Daniel Ciolek, Matias Duran, Florencia Zanollo, Nicolas Pazos, Julián Braier, Victor Braberman, Nicolas D’Ippolito, Sebastian Uchitel. "On-the-fly informed search of non-blocking directed controllers" Automatica, Volume 147, 2023, ISSN 0005-1098.

    4. 2022

    1. L. Nahabedian, V. Braberman, N. D’Ippolito, J. Kramer, S. Uchitel. "Assured automatic dynamic reconfiguration of business processes" ACM Information Systems, Volume 104, 2022, 101850, ISSN 0306-4379..
    2. M. Keegan, V. Braberman, N. D'Ippolito, N. Piterman and S. Uchitel. "Control and Discovery of Environment Behaviour" IEEE Transactions on Software Engineering, vol. 48, no. 6, pp. 1965-1978, 1 June 2022..

      3. 2021

      1. S. Zudaire, F. Gorostiaga, C. Sánchez, G. Schneider and S. Uchitel. "Assumption Monitoring Using Runtime Verification for UAV Temporal Task Plan Executions" 2021 IEEE International Conference on Robotics and Automation (ICRA), Xi'an, China, 2021, pp. 6824-6830..
      2. Y. A. Alrahman, V. Braberman, N. D'Ippolito, N. Piterman and S. Uchitel. "Synthesis of Run-To-Completion Controllers for Discrete Event Systems" 2021 American Control Conference (ACC), New Orleans, LA, USA, 2021, pp. 4892-4899..
      3. Sebastian A. Zudaire, Leandro Nahabedian, and Sebastian Uchitel. "Assured Mission Adaptation of UAVs" ACM Trans. Auton. Adapt. Syst. 16, 3–4, Article 7 (December 2021), 27 pages..

        4. 2020

        1. S. A. Zudaire, M. Garrett and S. Uchitel. "Iterator-Based Temporal Logic Task Planning" IEEE 2020 IEEE International Conference on Robotics and Automation (ICRA), Paris, France, 2020, pp. 11472-11478..

          2. 2019

          1. Leandro Nahabedian, Victor Braberman, Nicolas D'Ippolito, Jeff Kramer, Sebastian Uchitel. "Dynamic Reconfiguration of Business Processes" International Conference on Business Process Management (BPM'19).

          2018

          1. Leandro Nahabedian, Victor Braberman, Nicolas D'Ippolito, Shinichi Honiden, Jeff Kramer, Kenji Tei, Sebastian Uchitel. "Dynamic Update of Discrete Event Controllers" IEEE Transactions on Software Engineering.

          2016

          1. Leandro Nahabedian, Victor Braberman, Nicolas D'Ippolito, Shinichi Honiden, Jeff Kramer, Kenji Tei, Sebastian Uchitel. "Assured and Correct Dynamic Update of Controllers" International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'16).

          2015

          1. Victor Braberman, Nicolas D'Ippolito, Jeff Kramer, Daniel Sykes, Sebastian Uchitel. "MORPH: A Reference Architecture for Configuration and Behaviour Self-Adaptation" 1st Workshop on Control Theory for Software Engineering co-located with ESEC/FSE .
          2. Nicolas D'Ippolito, Victor Braberman, Daniel Sykes, Sebastian Uchitel. "Robust degradation and enhancement of robot mission behaviour in unpredictable environments" 1st Workshop on Control Theory for Software Engineering co-located with ESEC/FSE .
          3. Sebastián Sardiña, Nicolas D'Ippolito. "Towards Fully Observable Non-deterministic Planning as Assumption-based Automatic Synthesis" International Joint Conference on Artificial Intelligence .
          4. Germán Regis, Renzo Degiovanni, Nicolas D'Ippolito, Nazareno Aguirre. "Specifying Event-Based Systems with a Counting Fluent Temporal Logic" International Conference on Software Engineering .
          5. Antonio Filieri, Martina Maggio , Konstantinos Angelopoulos, Nicolas D'Ippolito. "Software Engineering meets Control Theory" 10th International Symposium on Software Engineering for Adaptive and Self-Managing Systems .

          2014

          1. Nicolas D'Ippolito, Victor Braberman, Jeff Kramer, Jeff Magee, Daniel Sykes, Sebastian Uchitel. "Hope for the Best, Prepare for the Worst: Multi-tier Control for Adaptive Systems" 36th International Conference on Software Engineering ICSE 2014 .
          2. Nicolas D'Ippolito, Victor Braberman, Nir Piterman, Sebastian Uchitel. "Controllability in Partial and Uncertain Environments" 14th International Conference on Application of Concurrency to System Design, {ACSD} 2014 .
          3. Ivo Krka, Nicolas D'Ippolito, Nenad Medvidovic, Sebastian Uchitel. "Revisiting Compatibility of Input-Output Modal Transition Systems" 19th International Symposium on Formal Methods FM 2014 .

          2013

          1. Sebastián Uchitel, Dalal Alrajeh, Shoham Ben-David, Victor Braberman, Marsha Chechik, Guido de Caso, Nicolas DIppolito, Dario Fischbein, Diego Garbervetsky, Jeff Kramer, Alessandra Russo, German Sybay. "Supporting incremental behaviour model elaboration" Computer Science - Research and Development 28.
          2. Nicolas D'Ippolito, Victor Braberman, Nir Piterman, Sebastian Uchitel. "Synthesising Non-Anomalous Event-Based Controllers for Liveness Goals" ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY .
          3. Victor Braberman, Nicolas D'Ippolito, Nir Piterman, Daniel Sykes, Sebastian Uchitel. "Controller synthesis: from modelling to enactment" 35th International Conference on Software Engineering (ICSE 2013) .

          2012

          1. Nicolas D'Ippolito, Victor Braberman, Nir Piterman, Sebastian Uchitel. "The Modal Transition System Control Problem" LECTURE NOTES IN COMPUTER SCIENCE 7436.
          2. Dario Fischbein, Greg Brunet, Nicolas D'Ippolito, Marsha Chechik, Sebastian Uchitel. "Weak Alphabet Merging of Partial Behaviour Models" ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY 21.
          3. Nicolas D'Ippolito. "Synthesis of event-based controllers: A software engineering challenge" International Conference on Software Engineering .

          2011

          1. Nicolas D'Ippolito, Victor Braberman, Nir Piterman, Sebastian Uchitel. "Synthesis of live behaviour models for fallible domains" 33rd International Conference on Software Engineering .

          2010

          1. Nicolas D'Ippolito, Victor Braberman, Nir Piterman, Sebastian Uchitel. "Synthesis of Live Behaviour Models" 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering .

          2008

          1. Nicolas D'Ippolito, Dario Fischbein, Marsha Chechik, Sebastian Uchitel. "MTSA: The Modal Transition System Analyser" 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008) .

          2007

          1. Nicolas D'Ippolito, Dario Fischbein, Howard Foster, Sebastian Uchitel. "MTSA: Eclipse support for modal transition systems construction, analysis and elaboration" 2007 OOPSLA workshop on Eclipse Technology eXchange .

Contributors

The research related to and demonstrated in MTSA is led by Professor Sebastián Uchitel. A major initial contributor was Nicolás D'Ippolito. Contributors to the tool include Nir Piterman, several (now graduated) PhD students including Daniel Ciolek, Ezequiel Castellano, Felipe Gorostiaga, Sebastian Zudaire, Daniel Sykes, Dario Fischbein and Leandro Nahabedian and many (now graduated) MSc students includeing Hernan Gagliardi, Matias Duran, Florencia Zanollo, Greg Brunet, Nicolas Pazos, Julián Braier, Tomás Delgado, Marco Sanchez Sorondo, Ezequiel Pecker-Marcosig, Maureen Keegan. Virginia Brassesco, Ivan Pasquini, Victor Wjugow, Daniel Zacharias.