Finite response and confluence of state-based supervisory controllers

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

Abstract

The development of logic controllers for cyber-physical systems is a difficult and error-prone process. Supervisor synthesis can ease the development process, by synthesizing a correct-by-construction supervisor from a model of the plant and a model of the control requirements. Subsequently, this synthesized supervisor can be used to automatically generate the controller code. However, for a supervisor to be implemented as a (logic) controller, additional properties need to be satisfied which are not guaranteed by supervisor synthesis. These properties are finite response and confluence.
In the literature, conditions are provided for a supervisor, modeled as a set of finite-state automata, to have finite response and to be confluent. Algorithms are defined to check these conditions. Recently, extended finite-state automata, i.e, automata augmented with variables, are being used increasingly often in the context of supervisory control. In this paper, sufficient conditions and algorithms are provided that can be used to verify if a supervisor, modeled as a set of extended finite-state automata, has finite response and is confluent. The algorithms are applied to three case studies from the literature to demonstrate their applicability to models used for supervisor synthesis.
LanguageEnglish
Title of host publication2019 IEEE 15th International Conference on Automation Science and Engineering (CASE), 22-26 August, Vancouver, BC, Canada
Place of PublicationPiscataway
PublisherInstitute of Electrical and Electronics Engineers
Pages509-516
Number of pages8
ISBN (Electronic)978-1-7281-0356-3
DOIs
StatePublished - Aug 2019
Event15th IEEE International Conference on Automation Science and Engineering, (CASE 2019) - University of British Columbia, Vancouver, Canada
Duration: 22 Aug 201926 Aug 2019
Conference number: 15
http://case2019.hust.edu.cn/

Conference

Conference15th IEEE International Conference on Automation Science and Engineering, (CASE 2019)
Abbreviated titleCASE2019
CountryCanada
CityVancouver
Period22/08/1926/08/19
Internet address

Fingerprint

Supervisory personnel
Controllers
Finite automata

Cite this

Reijnen, F., Hofkamp, A., van de Mortel - Fronczak, A., Reniers, M., & Rooda, K. (2019). Finite response and confluence of state-based supervisory controllers. In 2019 IEEE 15th International Conference on Automation Science and Engineering (CASE), 22-26 August, Vancouver, BC, Canada (pp. 509-516). Piscataway: Institute of Electrical and Electronics Engineers. DOI: 10.1109/COASE.2019.8843335
Reijnen, Ferdie ; Hofkamp, Albert ; van de Mortel - Fronczak, Asia ; Reniers, Michel ; Rooda, Koos. / Finite response and confluence of state-based supervisory controllers. 2019 IEEE 15th International Conference on Automation Science and Engineering (CASE), 22-26 August, Vancouver, BC, Canada. Piscataway : Institute of Electrical and Electronics Engineers, 2019. pp. 509-516
@inproceedings{c00bc7ae3ad7450785c7aecc0dc13580,
title = "Finite response and confluence of state-based supervisory controllers",
abstract = "The development of logic controllers for cyber-physical systems is a difficult and error-prone process. Supervisor synthesis can ease the development process, by synthesizing a correct-by-construction supervisor from a model of the plant and a model of the control requirements. Subsequently, this synthesized supervisor can be used to automatically generate the controller code. However, for a supervisor to be implemented as a (logic) controller, additional properties need to be satisfied which are not guaranteed by supervisor synthesis. These properties are finite response and confluence. In the literature, conditions are provided for a supervisor, modeled as a set of finite-state automata, to have finite response and to be confluent. Algorithms are defined to check these conditions. Recently, extended finite-state automata, i.e, automata augmented with variables, are being used increasingly often in the context of supervisory control. In this paper, sufficient conditions and algorithms are provided that can be used to verify if a supervisor, modeled as a set of extended finite-state automata, has finite response and is confluent. The algorithms are applied to three case studies from the literature to demonstrate their applicability to models used for supervisor synthesis.",
author = "Ferdie Reijnen and Albert Hofkamp and {van de Mortel - Fronczak}, Asia and Michel Reniers and Koos Rooda",
year = "2019",
month = "8",
doi = "10.1109/COASE.2019.8843335",
language = "English",
pages = "509--516",
booktitle = "2019 IEEE 15th International Conference on Automation Science and Engineering (CASE), 22-26 August, Vancouver, BC, Canada",
publisher = "Institute of Electrical and Electronics Engineers",
address = "United States",

}

Reijnen, F, Hofkamp, A, van de Mortel - Fronczak, A, Reniers, M & Rooda, K 2019, Finite response and confluence of state-based supervisory controllers. in 2019 IEEE 15th International Conference on Automation Science and Engineering (CASE), 22-26 August, Vancouver, BC, Canada. Institute of Electrical and Electronics Engineers, Piscataway, pp. 509-516, 15th IEEE International Conference on Automation Science and Engineering, (CASE 2019), Vancouver, Canada, 22/08/19. DOI: 10.1109/COASE.2019.8843335

Finite response and confluence of state-based supervisory controllers. / Reijnen, Ferdie; Hofkamp, Albert; van de Mortel - Fronczak, Asia; Reniers, Michel; Rooda, Koos.

2019 IEEE 15th International Conference on Automation Science and Engineering (CASE), 22-26 August, Vancouver, BC, Canada. Piscataway : Institute of Electrical and Electronics Engineers, 2019. p. 509-516.

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

TY - GEN

T1 - Finite response and confluence of state-based supervisory controllers

AU - Reijnen,Ferdie

AU - Hofkamp,Albert

AU - van de Mortel - Fronczak,Asia

AU - Reniers,Michel

AU - Rooda,Koos

PY - 2019/8

Y1 - 2019/8

N2 - The development of logic controllers for cyber-physical systems is a difficult and error-prone process. Supervisor synthesis can ease the development process, by synthesizing a correct-by-construction supervisor from a model of the plant and a model of the control requirements. Subsequently, this synthesized supervisor can be used to automatically generate the controller code. However, for a supervisor to be implemented as a (logic) controller, additional properties need to be satisfied which are not guaranteed by supervisor synthesis. These properties are finite response and confluence. In the literature, conditions are provided for a supervisor, modeled as a set of finite-state automata, to have finite response and to be confluent. Algorithms are defined to check these conditions. Recently, extended finite-state automata, i.e, automata augmented with variables, are being used increasingly often in the context of supervisory control. In this paper, sufficient conditions and algorithms are provided that can be used to verify if a supervisor, modeled as a set of extended finite-state automata, has finite response and is confluent. The algorithms are applied to three case studies from the literature to demonstrate their applicability to models used for supervisor synthesis.

AB - The development of logic controllers for cyber-physical systems is a difficult and error-prone process. Supervisor synthesis can ease the development process, by synthesizing a correct-by-construction supervisor from a model of the plant and a model of the control requirements. Subsequently, this synthesized supervisor can be used to automatically generate the controller code. However, for a supervisor to be implemented as a (logic) controller, additional properties need to be satisfied which are not guaranteed by supervisor synthesis. These properties are finite response and confluence. In the literature, conditions are provided for a supervisor, modeled as a set of finite-state automata, to have finite response and to be confluent. Algorithms are defined to check these conditions. Recently, extended finite-state automata, i.e, automata augmented with variables, are being used increasingly often in the context of supervisory control. In this paper, sufficient conditions and algorithms are provided that can be used to verify if a supervisor, modeled as a set of extended finite-state automata, has finite response and is confluent. The algorithms are applied to three case studies from the literature to demonstrate their applicability to models used for supervisor synthesis.

U2 - 10.1109/COASE.2019.8843335

DO - 10.1109/COASE.2019.8843335

M3 - Conference contribution

SP - 509

EP - 516

BT - 2019 IEEE 15th International Conference on Automation Science and Engineering (CASE), 22-26 August, Vancouver, BC, Canada

PB - Institute of Electrical and Electronics Engineers

CY - Piscataway

ER -

Reijnen F, Hofkamp A, van de Mortel - Fronczak A, Reniers M, Rooda K. Finite response and confluence of state-based supervisory controllers. In 2019 IEEE 15th International Conference on Automation Science and Engineering (CASE), 22-26 August, Vancouver, BC, Canada. Piscataway: Institute of Electrical and Electronics Engineers. 2019. p. 509-516. Available from, DOI: 10.1109/COASE.2019.8843335