{'fraction_non_alphanumeric': 0.020928711576193592, 'fraction_numerical': 0.0, 'mean_word_length': 5.401673640167364, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Compositional Approach for Verifying Sampled-Data Supervisory Control

Sampled-data supervisory control deals with timed discrete event systems (TDES) where the supervisors are to be implemented as sampled-data controllers. A sampled-data controller views the system as a series of inputs and outputs and is controlled by a periodic clock. It samples its inputs, changes state, and updates its outputs on each clock edge (the tick event). The sampled-data supervisory control framework provides a set of conditions that the TDES system must satisfy to ensure its correct behaviour in order to be implemented as sampled data controllers. A serious limitation for automatic verification of systems is the size of the system’s synchronous product. To overcome this limitation, we propose the use of a compositional approach to the verification of sampled-data supervisory control. In this approach, first we recast the required conditions for sampled-data supervisory control in terms of other properties such as language inclusion, nonblocking or controllability, which already have existing compositional methods and algorithms. This makes the sampled-data properties suitable for compositional verification, considerably increasing the size of systems that can be handled using sampled-data supervisory control. We also develop and implement a set of algorithms for the compositional verification of these sampled-data properties. We provide an example of the SD Controlled Flexible Manufacturing System to test our algorithms.