摘要：AbstractThis 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 LTLfis 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.
关键词：KeywordsTimed discrete event systemslinear temporal logicinteger linear programming
