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

TL;DR

This paper introduces ticked LTLf, a new temporal logic for timed discrete event systems, and presents an ILP-based synthesis method, demonstrated through a path planning example.

Contribution

The paper proposes ticked LTLf, a novel logic extending LTLf with counting-based temporal properties, and develops an ILP encoding for system synthesis.

Findings

Effective encoding of timed constraints into ILP

Successful application to path planning example

Demonstrates practical viability of the approach

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.