The formal logic approach for checking the observability of a specification language on DES functioning
Artem Davydov, Александр Ларионов, Nadezhda Nagul · 2018
Using the new approach to the formalization of controlled discrete-event systems (DES), based on positively constructed formulas (PCFs) calculus, the algorithm for testing the observability of the specification languages is presented in this paper. An information mapping in the form of a natural projection and an automata-based representation of a logical DES is considered. Sequences of events, causing changes in the state of the system, are generated as words of a formal language. A discrete-event model of an autonomous underwater vehicle (AUV) as a member of an AUV group is developed, which describe the main high-level functions of the AUV in surveillance missions. Its formalization in the form of PCF is presented.