Control of Timed Discrete Event Systems with Ticked Linear Temporal Logic Constraints. Issue 2 (2020)

• Record Type: Journal Article
• Authors: Kinugawa, Takuma; Hashimoto, Kazumune; Ushio, Toshimitsu
• Is Part Of: IFAC-PapersOnLine. Volume 53:Issue 2(2020)
• Page Start: 2143
• Page End: 2148
• Publication Date: 2020
• Subjects: Timed discrete event systems -- linear temporal logic -- integer linear programming; Automatic control -- Periodicals; 629.805
• DOI: 10.1016/j.ifacol.2020.12.2539
• Languages: English
• ISSNs: 2405-8963

Abstract

Abstract: This paper presents a novel method of synthesizing a controller of a timed discrete event system(TDES), introducing a novel linear temporal logic(LTL), called ticked LTLf . The ticked LTLf is given as an extension to LTLf, where the semantics is defined over a finite execution sequence. Differently from the standard LTLf, the formula is defined as a variant of metric temporal logic formula, where the temporal properties are described by counting the number of tick in the execution sequence of the TDES. Moreover, we provide a scheme that encodes the problem into a suitable one that can be solved by an integer linear programming (ILP). The effectiveness of the proposed approach is illustrated through a numerical example of a path planning.