Active Learning of Formal Plant Models for Cyber-Physical Systems

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review


  • Polina Ovsiannikova
  • Daniil Chivilikhin
  • Vladimir Ulyantsev
  • Andrey Stankevich
  • Ilya Zakirzyanov
  • Valeriy Vyatkin

  • Anatoly Shalyto

Research units

  • St. Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO)
  • Luleå University of Technology


As the world becomes more and more automated, the degree of cyber-physical systems involvement cannot be overestimated. A large part of them are safety-critical, thus, it is especially important to ensure their correctness before start of operation or reconfiguration. For this purpose the model checking approach should be used since it allows rigorously proving system correctness by checking all possible states. To ensure the compliance of controller-plant properties with system requirements, the closed-loop verification approach should be chosen, which requires not only a formal model of the controller, but also a formal model of the plant. In this paper we propose an approach for constructing formal models of context-free deterministic plants automatically using active learning algorithms. The case study shows its successful application to plant model generation for the elevator cyber-physical system.


Original languageEnglish
Title of host publicationProceedings of the IEEE 16th International Conference on Industrial Informatics, INDIN 2018
Publication statusPublished - 24 Sep 2018
MoE publication typeA4 Article in a conference publication
EventIEEE International Conference on Industrial Informatics - University of Porto's Engineering Faculty (FEUP), Porto, Portugal
Duration: 18 Jul 201820 Jul 2018
Conference number: 16

Publication series

NameIEEE International Conference on Industrial Informatics
ISSN (Print)1935-4576
ISSN (Electronic)2378-363X


ConferenceIEEE International Conference on Industrial Informatics
Abbreviated titleINDIN
Internet address

    Research areas

  • automata, input variables, correlation, computational modeling, cyber-physical systems, model checking, context modeling

ID: 29461946