Control of Timed Discrete Event Systems with Ticked Linear Temporal Logic Constraints
Systems and Control
2019-12-06 v1 Systems and Control
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. The ticked LTL is given as an extension to LTL, where the semantics is defined over a finite execution fragment. Differently from the standard LTL, 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.
Keywords
Cite
@article{arxiv.1912.02513,
title = {Control of Timed Discrete Event Systems with Ticked Linear Temporal Logic Constraints},
author = {Takuma Kinugawa and Kazumune Hashimoto and Toshimitsu Ushio},
journal= {arXiv preprint arXiv:1912.02513},
year = {2019}
}