A designer support framework for specification comprehensibility in automata-based discrete-event control design

• Main Author: Amrith Dhananjayan
• Other Authors: Seow Kiam Tian
• Format: Theses and Dissertations
• Language: English
• Published: 2013
• Subjects: DRNTU::Engineering::Computer science and engineering::Theory of computation::Mathematical logic and formal languages
• Online Access: http://hdl.handle.net/10356/54801
• Institution: Nanyang Technological University

This thesis addresses the longstanding problem of comprehensibility in formal language specification for supervisory control of logical and real-time discrete-event systems (DES’s). The problem stems from control designers who often face the dilemma of not knowing if a manually prescribed specification in finite automata is the intended control requirement. The need to validate such a specification by checking whether or not it is as intended requires formal theoretical support. With the availability of increasingly efficient algorithms and tools that are predominantly based on finite automata for specification and control synthesis, the challenges posed by human designer comprehensibility have been identified as one of the major reasons limiting the adoption of supervisory control theory for solving complex industrial problems. To mitigate this problem, this thesis proposes a new specification comprehensibility framework that provides designer support for writing and validating both logical and real-time specifications from the following two perspectives: 1. Natural language readability - by allowing requirements to be written in a linguistic form close to natural language. 2. Specification transparency - by restructuring specification automata to accentuate their non-trivial restrictions on a system. To support the first perspective, a real-time temporal logic translation interface is proposed for the real-time control framework that models DES’s and specifications as automata in the form of timed-transition graphs. A provably correct and complete translation algorithm is developed that can convert real-time specifications of the bounded-response form, written in metric temporal logic, to timed transition graph specifications. Importantly, this work complements existing research on a logical version, and together provides the means for expressing and translating readable specifications into finite automata for control synthesis. To support the second perspective, the new concept of state transparency for logical specifications in finite automata is proposed and investigated. The problem of maximizing the state transparency of specification automata is theoretically formulated and proven to be NP-hard. A polynomial-time algorithm that can often produce specification automata of maximal state transparency is proposed and studied. Importantly, this work complements existing research on event transparency, and together provides the alternate means for better comprehension and validation of the specification automata. Extending to the real-time control framework, the new problem of maximizing the transparency of time-transition graph specifications is formulated and proven to be NP-hard. A polynomial time algorithm that can often compute timed transition graph specifications of maximal transparency is proposed and studied. Both logical and real-time examples are presented to illustrate the utility of the specification framework, and qualitatively assess the level of human designer’s comprehensibility achieved in using temporal logic and the specification concepts of automata transparency. By providing added assurance to specifications, the framework presented in this thesis can be regarded as a fundamental basis for designer support in writing and validating specifications for DES’s.