| Article ID: | iaor20125619 |
| Volume: | 73 |
| Issue: | 9 |
| Start Page Number: | 1539 |
| End Page Number: | 1552 |
| Publication Date: | Sep 2012 |
| Journal: | Automation and Remote Control |
| Authors: | Nepeivoda A |
| Keywords: | control |
We consider the verification problem for an electromechanical device with a variable number of connectors and solve it with the modal logic LTL (Linear Temporal Logic). In the course of the analysis, we prove continuity and unambiguity theorems for the device operation and study the restrictions necessary in order for the device operation algorithm to be completely correct.