Control of Timed Discrete Event Systems with Ticked Linear Temporal Logic Constraints

Takuma Kinugawa; Kazumune Hashimoto; Toshimitsu Ushio

paper

Control of Timed Discrete Event Systems with Ticked Linear Temporal Logic Constraints

arXiv:1912.02513

Abstract

This paper presents a novel method of synthesizing a fragment of a timed discrete event system(TDES),introducing a novel linear temporal logic(LTL), called ticked LTL $_{f}$ . The ticked LTL $_{f}$ is given as an extension to LTL $_{f}$ , where the semantics is defined over a finite execution fragment. Differently from the standard LTL $_{f}$ , 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 fragment 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.