Towards a concurrency theory for supervisory control

J.C.M. Baeten, A.C. Hulst, van, D.A. Beek, van, J. Markovski

Research output: Book/ReportReportAcademic

Abstract

In this paper we propose a process-theoretic concurrency model to express supervisory control properties. In light of the present importance of reliable control software, the current work ow of direct conversion from informal specication documents to control software implementations can be improved. A separate modeling step in terms of controllable and uncontrollable behavior of the device under control is desired. We consider the control loop as a feedback model for supervisory control, in terms of the three distinct components of plant, requirements and supervisor. With respect to the control ow, we consider event-based models as well as state-based ones. We study the process theory TCP as a convenient modeling formalism that includes parallelism, iteration, communication features and non-determinism. Via structural operational semantics, we relate the terms in TCP to labeled transition systems. We consider the partial bisimulation preorder to express controllability that is better suited to handle non-determinism, compared to bisimulation-based models. It is shown how precongruence of partial bisimulation can be derived from the format of the deduction rules. The theory of TCP is studied under nite axiomatization for which soundness and ground-completeness (modulo iteration) is proved with respect to partial bisimulation. Language-based controllability, as the neccesary condition for event-based supervisory control is expressed in terms of partial bisimulation and we discuss several drawbacks of the strict event-based approach. Statebased control is considered under partial bisimulation as a dependable solution to address non-determinism. An appropriate renaming operator is introduced to address an issue in parallel communication. A case for automated guided vehicles (AGV) is modeled using the theory TCP. The latter theory is henceforth extended to include state-based valuations for which partial bisimulation and an axiomatization are dened. We consider an extended case on industrial printers to show the modeling abilities of this extended theory. In our concluding remarks, we sketch a future research path in terms of a new formal language for concurrent control modeling.
LanguageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Number of pages38
StatePublished - 2012

Publication series

NameSE report
Volume2012-01
ISSN (Print)1872-1567

Fingerprint

Controllability
Supervisory personnel
Semantics
Feedback
Communication

Cite this

Baeten, J. C. M., Hulst, van, A. C., Beek, van, D. A., & Markovski, J. (2012). Towards a concurrency theory for supervisory control. (SE report; Vol. 2012-01). Eindhoven: Technische Universiteit Eindhoven.
Baeten, J.C.M. ; Hulst, van, A.C. ; Beek, van, D.A. ; Markovski, J./ Towards a concurrency theory for supervisory control. Eindhoven : Technische Universiteit Eindhoven, 2012. 38 p. (SE report).
@book{22063002e7e04a1699e67c525bc2e936,
title = "Towards a concurrency theory for supervisory control",
abstract = "In this paper we propose a process-theoretic concurrency model to express supervisory control properties. In light of the present importance of reliable control software, the current work ow of direct conversion from informal specication documents to control software implementations can be improved. A separate modeling step in terms of controllable and uncontrollable behavior of the device under control is desired. We consider the control loop as a feedback model for supervisory control, in terms of the three distinct components of plant, requirements and supervisor. With respect to the control ow, we consider event-based models as well as state-based ones. We study the process theory TCP as a convenient modeling formalism that includes parallelism, iteration, communication features and non-determinism. Via structural operational semantics, we relate the terms in TCP to labeled transition systems. We consider the partial bisimulation preorder to express controllability that is better suited to handle non-determinism, compared to bisimulation-based models. It is shown how precongruence of partial bisimulation can be derived from the format of the deduction rules. The theory of TCP is studied under nite axiomatization for which soundness and ground-completeness (modulo iteration) is proved with respect to partial bisimulation. Language-based controllability, as the neccesary condition for event-based supervisory control is expressed in terms of partial bisimulation and we discuss several drawbacks of the strict event-based approach. Statebased control is considered under partial bisimulation as a dependable solution to address non-determinism. An appropriate renaming operator is introduced to address an issue in parallel communication. A case for automated guided vehicles (AGV) is modeled using the theory TCP. The latter theory is henceforth extended to include state-based valuations for which partial bisimulation and an axiomatization are dened. We consider an extended case on industrial printers to show the modeling abilities of this extended theory. In our concluding remarks, we sketch a future research path in terms of a new formal language for concurrent control modeling.",
author = "J.C.M. Baeten and {Hulst, van}, A.C. and {Beek, van}, D.A. and J. Markovski",
year = "2012",
language = "English",
series = "SE report",
publisher = "Technische Universiteit Eindhoven",

}

Baeten, JCM, Hulst, van, AC, Beek, van, DA & Markovski, J 2012, Towards a concurrency theory for supervisory control. SE report, vol. 2012-01, Technische Universiteit Eindhoven, Eindhoven.

Towards a concurrency theory for supervisory control. / Baeten, J.C.M.; Hulst, van, A.C.; Beek, van, D.A.; Markovski, J.

Eindhoven : Technische Universiteit Eindhoven, 2012. 38 p. (SE report; Vol. 2012-01).

Research output: Book/ReportReportAcademic

TY - BOOK

T1 - Towards a concurrency theory for supervisory control

AU - Baeten,J.C.M.

AU - Hulst, van,A.C.

AU - Beek, van,D.A.

AU - Markovski,J.

PY - 2012

Y1 - 2012

N2 - In this paper we propose a process-theoretic concurrency model to express supervisory control properties. In light of the present importance of reliable control software, the current work ow of direct conversion from informal specication documents to control software implementations can be improved. A separate modeling step in terms of controllable and uncontrollable behavior of the device under control is desired. We consider the control loop as a feedback model for supervisory control, in terms of the three distinct components of plant, requirements and supervisor. With respect to the control ow, we consider event-based models as well as state-based ones. We study the process theory TCP as a convenient modeling formalism that includes parallelism, iteration, communication features and non-determinism. Via structural operational semantics, we relate the terms in TCP to labeled transition systems. We consider the partial bisimulation preorder to express controllability that is better suited to handle non-determinism, compared to bisimulation-based models. It is shown how precongruence of partial bisimulation can be derived from the format of the deduction rules. The theory of TCP is studied under nite axiomatization for which soundness and ground-completeness (modulo iteration) is proved with respect to partial bisimulation. Language-based controllability, as the neccesary condition for event-based supervisory control is expressed in terms of partial bisimulation and we discuss several drawbacks of the strict event-based approach. Statebased control is considered under partial bisimulation as a dependable solution to address non-determinism. An appropriate renaming operator is introduced to address an issue in parallel communication. A case for automated guided vehicles (AGV) is modeled using the theory TCP. The latter theory is henceforth extended to include state-based valuations for which partial bisimulation and an axiomatization are dened. We consider an extended case on industrial printers to show the modeling abilities of this extended theory. In our concluding remarks, we sketch a future research path in terms of a new formal language for concurrent control modeling.

AB - In this paper we propose a process-theoretic concurrency model to express supervisory control properties. In light of the present importance of reliable control software, the current work ow of direct conversion from informal specication documents to control software implementations can be improved. A separate modeling step in terms of controllable and uncontrollable behavior of the device under control is desired. We consider the control loop as a feedback model for supervisory control, in terms of the three distinct components of plant, requirements and supervisor. With respect to the control ow, we consider event-based models as well as state-based ones. We study the process theory TCP as a convenient modeling formalism that includes parallelism, iteration, communication features and non-determinism. Via structural operational semantics, we relate the terms in TCP to labeled transition systems. We consider the partial bisimulation preorder to express controllability that is better suited to handle non-determinism, compared to bisimulation-based models. It is shown how precongruence of partial bisimulation can be derived from the format of the deduction rules. The theory of TCP is studied under nite axiomatization for which soundness and ground-completeness (modulo iteration) is proved with respect to partial bisimulation. Language-based controllability, as the neccesary condition for event-based supervisory control is expressed in terms of partial bisimulation and we discuss several drawbacks of the strict event-based approach. Statebased control is considered under partial bisimulation as a dependable solution to address non-determinism. An appropriate renaming operator is introduced to address an issue in parallel communication. A case for automated guided vehicles (AGV) is modeled using the theory TCP. The latter theory is henceforth extended to include state-based valuations for which partial bisimulation and an axiomatization are dened. We consider an extended case on industrial printers to show the modeling abilities of this extended theory. In our concluding remarks, we sketch a future research path in terms of a new formal language for concurrent control modeling.

M3 - Report

T3 - SE report

BT - Towards a concurrency theory for supervisory control

PB - Technische Universiteit Eindhoven

CY - Eindhoven

ER -

Baeten JCM, Hulst, van AC, Beek, van DA, Markovski J. Towards a concurrency theory for supervisory control. Eindhoven: Technische Universiteit Eindhoven, 2012. 38 p. (SE report).