2019/09/24 by Lars Lindemann, Dimos V. Dimarogonas, Lindemann, Lars +1 · 1 citation
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1909.11159
openalex publication_date 2019/09/24 · openalex created_date 2022/07/28 · openalex updated_date 2026/07/28
The use of spatio-temporal logics in control is motivated by the need to\nimpose complex spatial and temporal behavior on dynamical systems, and to\ncontrol these systems accordingly. Synthesizing correct-by-design control laws\nis a challenging task resulting in computationally demanding methods. We\nconsider efficient automata-based planning for continuous-time systems under\nsignal interval temporal logic specifications, an expressive fragment of signal\ntemporal logic. The planning is based on recent results for automata-based\nverification of metric interval temporal logic. A timed signal transducer is\nobtained accepting all Boolean signals that satisfy a metric interval temporal\nlogic specification, which is abstracted from the signal interval temporal\nlogic specification at hand. This transducer is modified to account for the\nspatial properties of the signal interval temporal logic specification,\ncharacterizing all real-valued signals that satisfy this specification. Using\nlogic-based feedback control laws, such as the ones we have presented in\nearlier works, we then provide an abstraction of the system that, in a suitable\nway, aligns with the modified timed signal transducer. This allows to avoid the\nstate space explosion that is typically induced by forming a product automaton\nbetween an abstraction of the system and the specification.\n