Mode-Target Games: Reactive Synthesis for Control Applications

DOI10.1109/TAC.2017.2722960MaRDI QIDQ4567056zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Ayça Balkan, Moshe Y. Vardi, Paulo Tabuada

Publication date 27 June 2018

Published in IEEE Transactions on Automatic Control (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1504.07702

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Games involving graphs (91A43) Synthesis problems (93B50) Discrete event control/observation systems (93C65)

Abstract: In this paper we introduce a class of Linear Temporal Logic (LTL) specifications for which the problem of synthesizing controllers can be solved in polynomial time. The new class of specifications is an LTL fragment that we term Mode-Target (MT) and is inspired by numerous control applications where there are modes and corresponding (possibly multiple) targets for each mode. We formulate the problem of synthesizing a controller enforcing an MT specification as a game and provide an algorithm that requires $O(su{m}_i{t}_i{n}^2)$ symbolic steps, where $n$ is the number of states in the game graph, and $t_i$ is the number of targets corresponding to mode $i$.

Cited in

(2)

• Combining control effects and their models: game semantics for a hierarchy of static, dynamic and delimited control effects
• The complexity of learning LTL, CTL and ATL formulas

This page was built for publication: Mode-Target Games: Reactive Synthesis for Control Applications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4567056)