Automating timed specification transparency for human designer validation of real-time discrete-event control requirements

Abstract

In supervisory control of discrete-event systems, prescribing formal specifications is a non-trivial task that depends on the intuition and cognitive understanding of the designer. A human designer has no assurance if a prescribed specification is as intended, making it necessary to manually validate the specification, i.e., check whether the specification does indeed prescribe the intended requirement. This uncertainty in specification is compounded in the case of timed discrete-event systems (TDES's), where real-timing behavior also needs to be correctly specified. The fundamental control theory for TDES's requires a specification to be formalized as a timed transition graph (TTG), prescribing a timed regulation of logical behavior that restricts a TDES to some timed execution sequences. To help validate the specification, human designers need an algorithm that can automatically remodel the TTG specification, to highlight sequences essential for comprehending the specification's timed restrictions while hiding irrelevant information. By `hiding' in self-loops the associated events of all transitions deemed irrelevant to the specification, we can obtain a more comprehensible TTG, formalized by what we call a transparent TTG specification. In this paper, we propose a polynomial-time algorithm to compute TTG specifications of clear transparency.