Tehran Institute for Advanced Studies (TEIAS)

/ Model Learning Reading Group

Reading Group

Model Learning

Mondays, Wednesdays, 11-12 (Online on Skype)




  • Model Learning Reading Group

Reading Group

Model Learning

Previous slide
Next slide


We interact with the programs inside cell phones, cars, pacemakers, laptops, … on a daily basis. Software errors within these systems can create devastating and dangerous hazards. Ensuring software correctness is an important discipline of software engineering. Many quality assurance techniques (e.g. model-based testing and model checking) require a model describing the behavior of the system. In this reading group, we survey various techniques of extracting behavioral models from software systems, with a focus of software product lines.


Rasta Tadayyon

(University of Tehran)

Amin Asadi

(University of Tehran)

Alireza Salemi

(University of Tehran)

What we have learnt sofar:

  • Angluin L* algorithm for model learning:

    after learning the algorithm we applied it on the A1 machine on page 2 of this slides


  • Two main techniques which we studied both to know which, each of us prefer to research on:
    • model checking:
      • slides (Dr. Hojjat University slides): IIIIII
    • model based testing:
      • slides (Dr. Mousavi University slides): III –book(for further study): [2]


  • Transition Systems and an efficient varient of them called Featured Transition Systems and their model checking algorithm.
    • papers:
      • [3]
        • summary slides: A Summary of Model Checking Lots of Systems Model checking of Featured Transition Systems use sequential product of transition systems. These slides have some examples of this notion which we reviwed in one of the meetings.
        • (main reference for formal definitions) [4]

    As a research problem we were curious whether it is possible to remove priority operator from Featured Transition Systems definition or not. We needed to learn how to write formal and precise proofs. We read [5] about strutured proofs. Here is it’s summary slides.


  • Besides Featured Transition Systems as a family-based technique for model checking, we studied FFSMs which is another family-based technique:


  • As you may have noticed, model of a particular product changes over time. For example a product might be added a feature to, or it may have a bug fix. One naive approach is that we build a new model from scratch which obviously is not efficient. So we learnt adaptive model learning methods; i.e dynamic model learning and partial dynamic model learning which are more efficient as they initially exploit observation table of the old version.



Vaandrager, F. (2017). Model learning. Communications of the ACM, 60(2), 86–95. https://doi.org/10.1145/2967606


Broy, M., Jonsson, B., Katoen, J., Leucker, M., & Pretschner, A. (2005). Model-Based Testing of Reactive Systems: Advanced Lectures (Lecture Notes in Computer Science (3472)) (2005th ed.). Springer.




Schobbens, P.-Y., Heymans, P., Trigaux, J.-C., & Bontemps, Y. (2007). Generic semantics of feature diagrams. Computer Networks, 51(2), 456–479. https://doi.org/10.1016/j.comnet.2006.08.008


Lamport, L. (1995). How to Write a Proof. The American Mathematical Monthly, 102(7), 600. https://doi.org/10.2307/2974556


Damasceno, C. D. N., Mousavi, M. R., & Simao, A. (2019). Learning from difference. Proceedings of the 23rd International Systems and Software Product Line Conference – Volume A – SPLC ’19, 1–11. https://doi.org/10.1145/3336294.3336307


Damasceno, C. D. N., Mousavi, M. R., & da Silva Simao, A. (2019). Learning to Reuse: Adaptive Model Learning for Evolving Systems. Lecture Notes in Computer Science, 138–156. https://doi.org/10.1007/978-3-030-34968-4_8


Naeem Irfan, M., Oriat, C., & Groz, R. (2013). Model Inference and Testing. Advances in Computers, 89–139. https://doi.org/10.1016/b978-0-12-408094-2.00003-5