Verifying performance of supervised plants

J. Markovski, M.A. Reniers

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

    17 Citations (Scopus)
    1 Downloads (Pure)


    Supervisory control theory deals with synthesis of models of supervisory controllers that ensure safe and nonblocking behavior, based on discrete-event models of the uncontrolled system and the control requirements. Extensions, like optimal supervision, additionally ascertain that given performance requirements are met by the controller as well. Unfortunately, ensuring optimality during supervisor synthesis proved to be computationally challenging. Therefore, we propose to separate supervisor synthesis and ensuring performance. To handle the stochastic behavior efficiently, we treat the Markovian delays syntactically and we employ existing synthesis tools for non-stochastic plants. To this end, we develop a process theory that can specify control loops of nondeterministic stochastic systems with state-based observations. After obtaining the model of the supervised system, we verify that the supervised system adheres to the given performance requirements by deriving the underlying Markov process and feeding it to a stochastic model checker. We illustrate the approach by estimating performance and reliability measures for the printing process of a high-tech Oce´ printer.
    Original languageEnglish
    Title of host publicationProceedings of the 2012 12th International Conference on Application of Concurrency to System Design (ACSD), 27-29 June 2012, Hamburg, Germany
    Place of PublicationPiscataway
    PublisherInstitute of Electrical and Electronics Engineers
    Publication statusPublished - 2012
    Event12th International Conference on Application of Concurrency to System Design (ACSD 2012) - Hamburg, Germany
    Duration: 27 Jun 201229 Jun 2012
    Conference number: 12


    Conference12th International Conference on Application of Concurrency to System Design (ACSD 2012)
    Abbreviated titleACSD 2012


    Dive into the research topics of 'Verifying performance of supervised plants'. Together they form a unique fingerprint.

    Cite this