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

2019/12/05 by Takuma Kinugawa, Kinugawa, Takuma, Kazumune Hashimoto +3
Computer Science · #Distributed systems and fault tolerance #FOS: Electrical engineering #Formal Methods in Verification #Petri Nets in System Modeling #Systems and Control (eess.SY) #electronic engineering #information engineering

paper · pdf · doi:10.48550/arxiv.1912.02513

openalex publication_date 2019/12/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Citations

• Introduction to Discrete Event Systems
• A theory of timed automata

Related

• Event-Triggered Controller Synthesis for Dynamical Systems with Temporal Logic Constraints
• Continuous-time Signal Temporal Logic Planning with Control Barrier Function
• Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-time Systems
• Direct data-driven control with signal temporal logic specifications
• What to Do When You Can't Do It All: Temporal Logic Planning with Soft Temporal Logic Constraints