Loading...
Thumbnail Image
Item

A survey on compositional algorithms for verification and synthesis in supervisory control

Abstract
This survey gives an overview of the current research on compositional algorithms for verification and synthesis of modular systems modelled as interacting finite-state machines. Compositional algorithms operate by repeatedly simplifying individual components of a large system, replacing them by smaller so-called abstractions, while preserving critical properties. In this way, the exponential growth of the state space can be limited, making it possible to analyse much bigger state spaces than possible by standard state space exploration. This paper gives an introduction to the principles underlying compositional methods, followed by a survey of algorithmic solutions from the recent literature that use compositional methods to analyse systems automatically. The focus is on applications in supervisory control of discrete event systems, particularly on methods that verify critical properties or synthesise controllable and nonblocking supervisors.
Type
Journal Article
Type of thesis
Series
Citation
Date
2023-08-21
Publisher
Springer Science and Business Media LLC
Degree
Supervisors
Rights
© The Author(s) 2023. This article is licensed under a Creative Commons Attribution 4.0 International License.