Real-Time Synthesis is Hard!

Abstract

We study the reactive synthesis problem ($\mathsf {RS}$) for specifications given in Metric Interval Temporal Logic ($\mathsf {MITL}$). $\mathsf {RS}$ is known to be undecidable in a very general setting, but on infinite words only; and only the very restrictive $\mathsf {BResRS}$ subcase is known to be decidable (see D’Souza et al. and Bouyer et al.). In this paper, we sharpen the decidability border of $\mathsf {MITL}$ synthesis. We show $\mathsf {RS}$ is undecidable on finite words too, and present a landscape of restrictions (both on the logic and on the possible controllers) that are still undecidable. On the positive side, we revisit $\mathsf {BResRS}$ and introduce an efficient on-the-fly algorithm to solve it.

More technical details and proofs can be found in the full version of this paper [8]. This work has been supported by The European Union Seventh Framework Programme under Grant Agreement 601148 (Cassting) and by the FRS/F.N.R.S. PDR grant SyVeRLo.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

The design of programs that respect real-time specifications is a difficult problem with recent and promising advances. Such programs must handle thin timing behaviours, are prone to errors, and difficult to correct a posteriori. Therefore, one road to the design of correct real-time software is the use of automatic synthesis methods, that build, from a specification, a program which is correct by construction. To this end, timed games are nowadays recognised as the key foundational model for the synthesis of real-time programs. These games are played between a controller and an environment, that propose actions in the system, modelled as a plant. The reactive synthesis problem ($\mathsf {RS}$) consists, given a real-time specification, in deciding whether the controller has a winning strategy ensuring that every execution of the plant consistent with this strategy (i.e., no matter the choices of the environment) satisfies the specification. As an example, consider a lift for which we want to design a software verifying certain safety conditions. In this case, the plant is a (timed) automaton, whose states record the current status of the lift (its floor, if it is moving, the button on which users have pushed...), as well as timing information regarding the evolution in-between the different states. On the other hand, the specification is usually given using some real-time logic: in this work, we consider mainly specifications given by a formula of $\mathsf {MITL}$ [2], a real-time extension of $\mathsf {LTL}$. Some actions in the plant are controllable (closing the doors, moving the cart), while others belong to the environment (buttons pushed by users, exact timing of various actions inside intervals, failures...). Then, $\mathsf {RS}$ asks to compute a controller that performs controllable actions at the right moments, so that, for all behaviours of the environment, the lift runs correctly.

In the untimed case, many positive theoretical and practical results have been achieved regarding $\mathsf {RS}$: for instance, when the specification is given as an $\mathsf {LTL}$ formula, we know that if a winning strategy exists, then there is one that can be described by a finite state machine [17]; and efficient $\mathsf {LTL}$ synthesis algorithms have been implemented [3, 13]. Unfortunately, in the real-time setting, the picture is not so clear. Indeed, a winning strategy in a timed game might need unbounded memory to recall the full prefix of the game, which makes the real-time synthesis problem a hard one. This is witnessed by three papers presenting negative results: D’Souza and Madhusudan [12] and Bouyer et al. [4] show that $\mathsf {RS}$ is undecidable (on finite and infinite words) when the specification is respectively a timed automaton and an $\mathsf {MTL}$ formula (the two most expressive formalisms in Fig. 1). More recently, Doyen et al. show [11] that $\mathsf {RS}$ is undecidable for $\mathsf {MITL}$ specifications over infinite words; but leave the finite words case open.

When facing an undecidability result, one natural research direction consists in considering subcases in order to recover decidability: here, this amounts to considering fragments of the logic, or restrictions on the possible controllers. Such results can also be found in the aforementioned works. In [12], the authors consider a variant of $\mathsf {RS}$, called bounded resources reactive synthesis ($\mathsf {BResRS}$) where the number of clocks and the set of guards that the controller can use are fixed a priori, and the specification is given by means of a timed automaton. By coupling this technique with the translation of $\mathsf {MITL}$ into timed automata [7], one obtains a 3-EXPTIME procedure (in the finite and infinite words cases). Unfortunately, due to the high cost of translating $\mathsf {MITL}$ into timed automata and the need to construct its entire deterministic region automaton, this algorithm is unlikely to be amenable to implementation. Then, [4] presents an on-the-fly algorithm for $\mathsf {BResRS}$ with $\mathsf {MTL}$ specifications ($\mathsf {MTL}$ is a strict superset of $\mathsf {MITL}$), on finite words, but their procedure runs in non-primitive recursive time.

Hence, the decidability status of the synthesis problem (with $\mathsf {MITL}$ requirements) still raises several questions, namely: (i) Can we relax the restrictions in the definition of $\mathsf {BResRS}$ while retaining decidability? (ii) Is $\mathsf {RS}$ decidable on finite words, as raised in [11]? (iii) Are there meaningful restrictions of the logic that make $\mathsf {RS}$ decidable? (iv) Can we devise an on-the-fly, efficient, algorithm that solves $\mathsf {BResRS}$ in 3-$\mathrm{EXPTIME}$ as in [12]? In the present paper, we provide answers to those questions. First, we consider the additional $\mathsf {IRS}$, $\mathsf {BPrecRS}$ and $\mathsf {BClockRS}$ problems, that introduce different levels of restrictions. $\mathsf {IRS}$ requests the controller to be a timed automaton. $\mathsf {BPrecRS}$ and $\mathsf {BClockRS}$ are further restrictions of $\mathsf {IRS}$ where respectively the set of guards and the set of clocks of the controller are fixed a priori. Thus, we consider the following hierarchy of problems: . Unfortunately, while $\mathsf {IRS}$, $\mathsf {BPrecRS}$ and $\mathsf {BClockRS}$ seem to make sense in practice, they turn out to be undecidable both on finite and infinite words—an answer to points (i) and (ii). Our proofs are based on a novel encoding of halting problem for deterministic channel machines. By contrast, the undecidability results of [4] (for $\mathsf {MTL}$) are reductions from the same problem, but their encoding relies heavily on the ability of $\mathsf {MTL}$ to express punctual constraints like ‘every a event is followed by a b event exactly one time unit later’, which is not allowed by $\mathsf {MITL}$. To the best of our knowledge, our proofs are the first to perform such a reduction in a formalism that disallows punctual requirements—a somewhat unexpected result. Then, we answer point (iii) by considering a hierarchy of syntactic subsets of $\mathsf {MITL}$ (see Fig. 1) and showing that, for all these subsets, $\mathsf {BPrecRS}$ and $\mathsf {BClockRS}$ (hence also $\mathsf {IRS}$ and $\mathsf {RS}$) remain undecidable, on finite and infinite words. Note that the undecidability proof of [12] cannot easily be adapted to cope with these cases, because it needs a mix of open and closed constraints; while we prove undecidable very weak fragments of $\mathsf {MITL}$ where only closed or only open constraints are allowed. All these negative results shape a precise picture of the decidability border for real-time synthesis (in particular, they answer open questions from [4, 9, 11]). On the positive side, we answer point (iv) by devising an on-the-fly algorithm to solve $\mathsf {BResRS}$ (in the finite words case) that runs in 3-$\mathrm{EXPTIME}$. It relies on one-clock alternating timed automata (as in [4], but unlike [12] that use timed automata), and on the recently introduced interval semantics [7].

2 Reactive Synthesis of Timed Properties

Let $\varSigma$ be a finite alphabet. A (finite) timed word¹ over $\varSigma$ is a finite word $\sigma = (\sigma _1,\tau _1)\cdots (\sigma _n,\tau _n)$ over $\varSigma \times \mathbb {R}^{+}$ with $(\tau _i)_{1\leqslant i\leqslant n}$ a non-decreasing sequence of non-negative real numbers. We denote by $T\varSigma ^\star$ the set of finite timed words over $\varSigma$. A timed language is a subset L of $T\varSigma ^\star$.

Timed Logics. We consider the reactive synthesis problem against various real-time logics, all of them being restrictions of Metric Temporal Logic ($\mathsf {MTL}$) [14]. The logic $\mathsf {MTL}$ is a timed extension of $\mathsf {LTL}$, where the temporal modalities are labelled with a timed interval. The formal syntax of $\mathsf {MTL}$ is given as follows:

$$\begin{aligned} \varphi := \top \ |\ a\ |\ \varphi \wedge \varphi \ |\ \lnot \varphi \ |\ \varphi \mathsf {U}_{I} \varphi \end{aligned}$$

where $a\in \varSigma$ and I is an interval over $\mathbb {R}^{+}$ with endpoints in $\mathbb N\cup \{+\infty \}$.

We consider the pointwise semantics and interpret $\mathsf {MTL}$ formulas over timed words. The semantics of a formula $\varphi$ in $\mathsf {MTL}$ is defined inductively in the usual way. We recall only the semantics of $\mathsf {U}$: given $\sigma =(\sigma _1,\tau _1)\cdots (\sigma _n,\tau _n)\in T\varSigma ^\star$, and a position $1\leqslant i\leqslant n$, we let $(\sigma ,i)\models \varphi _1\mathsf {U}_{I} \varphi _2$ if there exists $j>i$ such that $(\sigma ,j)\models \varphi _2$, $\tau _j-\tau _i\in I$, and $(\sigma , k)\models \varphi _1$, for all $i< k< j$.

With $\bot := \lnot \top$, we can recover the ‘next’ operator $\bigcirc _{I}\varphi := \bot \mathsf {U}_{I} \varphi$, and we rely on the usual shortcuts for the ‘finally’, ‘globally’ and ‘dual-until’ operators: $\lozenge _{I}\varphi := \top \mathsf {U}_{I} \varphi$, $\square _{I}\varphi := \lnot \lozenge _{I}\lnot \varphi$ and $\varphi _1\widetilde{\mathsf {U}}_{I} \varphi _2 := \lnot ((\lnot \varphi _1)\mathsf {U}_{I}(\lnot \varphi _2))$. We also use the non-strict version of the ‘until’ operator $\varphi _1\overline{\mathsf {U}}_{I} \varphi _2$, defined as $\varphi _2\vee (\varphi _1\wedge \varphi _1\mathsf {U}_{I}\varphi _2)$ (if $0 \in I$) or $\varphi _1\wedge \varphi _1\mathsf {U}_{I}\varphi _2$ (if $0 \notin I$). This notation yields the corresponding non-strict operators $\overline{\lozenge }_{} \varphi$ and $\overline{\square }_{}\varphi$ in the natural way. When the interval I is the entire set of the non-negative real numbers, the subscript is often omitted. We say that $\sigma$ satisfies the formula $\varphi$, written $\sigma \models \varphi$ if $(\sigma ,1)\models \varphi$, and we denote by $\mathcal L(\varphi )$ the set of all timed words $\sigma$ such that $\sigma \models \varphi$.

Fig. 1.

All the fragments of $\mathsf {MITL}$ for which $\mathsf {BPrecRS}$ and $\mathsf {BClockRS}$ are undecidable (hence also $\mathsf {RS}$ and $\mathsf {IRS}$). $A\rightarrow B$ means that A strictly contains B.

We consider mainly a restriction of $\mathsf {MTL}$ called $\mathsf {MITL}$ (for Metric Interval Temporal Logic), in which the intervals are restricted to non-singular ones. We denote by $\textsf {Open \text {-}}\mathsf {MITL}$ the open fragment of $\mathsf {MITL}$: in negation normal form, each subformula $\varphi _1 \mathsf {U}_{I} \varphi _2$ has either I open or $\inf (I) = 0$ and I right-open, and each subformula $\varphi _1 \widetilde{\mathsf {U}}_{I} \varphi _2$ has I closed. Then, a formula is in $\textsf {Closed \text {-}}\mathsf {MITL}$ if it is the negation of an $\textsf {Open \text {-}}\mathsf {MITL}$ formula. By [7], $\textsf {Open \text {-}}\mathsf {MITL}$ formulas (respectively, $\textsf {Closed \text {-}}\mathsf {MITL}$ formulas) translate to open (closed) timed automata [15], i.e., all clock constraints are strict (non-strict). Two other important fragments of $\mathsf {MTL}$ considered in the literature consist of $\mathsf {Safety\text {-}MTL}$ [16], where each subformula $\varphi _1 \mathsf {U}_{I} \varphi _2$ has I bounded in negation normal form, and $\mathsf {coFlat\text {-}MTL}$ [5], where the formula satisfies the following in negation normal form: (i) in each subformula $\varphi _1 \mathsf {U}_{I} \varphi _2$, if I is unbounded then $\varphi _2 \in \mathsf {LTL}$; and (ii) in each subformula $\varphi _1 \widetilde{\mathsf {U}}_{I} \varphi _2$, if I is unbounded then $\varphi _1 \in \mathsf {LTL}$.

For all of these logics $\mathsf L$, we can consider several restrictions. The restriction in which only the non-strict variants of the operators ($\overline{\lozenge }_{}$, $\overline{\square }_{}$, etc.) are allowed is denoted by $\mathsf L^{\mathrm {ns}}$. The fragment in which all the intervals used in the formula are either unbounded, or have a left endpoint equal to 0 is denoted by $\mathsf L[\mathsf {U}_{0,\infty }]$. In this case, the interval I can be replaced by an expression of the form $\sim c$, with $c\in \mathbb {N}$, and ${\sim }\in \{<,>,\leqslant ,\geqslant \}$. It is known that $\mathsf {MITL} [\mathsf {U}_{0,\infty }]$ is expressively equivalent to $\mathsf {ECL} _\textsf {fut}$ [18], which is itself a syntactic fragment of Event-Clock Logic ($\mathsf {ECL}$). Finally, $\mathsf L[\lozenge _{\infty }]$ stands for the logic where ‘until’ operators only appear in the form of $\lozenge _{I}$ or $\square _{I}$ with intervals I of the shape $[a,\infty )$ or $(a,\infty )$.

Symbolic Transition Systems. Let X be a finite set of variables, called clocks. The set $\mathcal G(X)$ of clock constraints g over X is defined by: $g:= \top \mid g\wedge g \mid x\bowtie c$, where ${\bowtie }\in \{<,\leqslant ,=,\geqslant ,>\}$, $x\in X$ and $c\in \mathbb Q^{+}$. A valuation over X is a mapping $\nu :X\rightarrow \mathbb {R}^{+}$. The satisfaction of a constraint g by a valuation $\nu$ is defined in the usual way and noted $\nu \models g$, and $\llbracket g\rrbracket$ is the set of valuations $\nu$ satisfying g. For $t\in \mathbb {R}^{+}$, we let $\nu \,+\,t$ be the valuation defined by $(\nu \,+\,t)(x) = \nu (x)\,+\,t$ for all $x\in X$. For $R\subseteq X$, we let $\nu [R\leftarrow 0]$ be the valuation defined by $(\nu [R\leftarrow 0])(x) = 0$ if $x\in R$, and $(\nu [R\leftarrow 0])(x) = \nu (x)$ otherwise.

Following the terminology of [4, 12], a granularity is a triple $\mu = (X,m,K)$ where X is a finite set of clocks, $m\in \mathbb N\setminus \{0\}$, and $K\in \mathbb N$. A constraint g is $\mu$-granular if $g\in \mathcal G(X)$ and each constant in g is of the form $\frac{\alpha }{m}$ with an integer $\alpha \leqslant K$. A symbolic alphabet $\varGamma$ based on $(\varSigma ,X)$ is a finite subset of $\varSigma \times \mathcal G^{\mathrm {atom}}_{m,K}(X)\times 2^X$, where $\mathcal G^{\mathrm {atom}}_{m,K}(X)$ denotes all atomic (X, m, K)-granular clock constraints (i.e., clock constraints g such that $\llbracket g\rrbracket = \llbracket g'\rrbracket$ or $\llbracket g\rrbracket \cap \llbracket g'\rrbracket = \emptyset$, for every (X, m, K)-granular clock constraint $g'$). Such a symbolic alphabet $\varGamma$ is said $\mu$-granular. A symbolic word $\gamma = (\sigma _1,g_1,R_1) \cdots (\sigma _n,g_n,R_n)$ over $\varGamma$ generates a set of timed words over $\varSigma$, denoted by $tw(\gamma )$ such that $\sigma \in tw(\gamma )$ if $\sigma = (\sigma _1,\tau _1)\cdots (\sigma _n,\tau _n)$, and there is a sequence $(\nu _i)_{0\leqslant i\leqslant n}$ of valuations with $\nu _0$ the zero valuation, and for all $1\leqslant i\leqslant n$, $\nu _{i-1}+\tau _{i}-\tau _{i-1}\models g_{i}$ and $\nu _i = (\nu _{i-1}+\tau _i-\tau _{i-1})[R_{i}\leftarrow 0]$ (assuming $\tau _0=0$). Intuitively, each $(\sigma _i,g_i,R_i)$ means that action $\sigma _i$ is performed, with guard $g_i$ satisfied and clocks in $R_i$ reset.

A symbolic transition system (STS) over a symbolic alphabet $\varGamma$ based on $(\varSigma ,X)$ is a tuple $\mathcal T= (S,s_0,\varDelta ,S_f)$ where S is a possibly infinite set of locations, $s_0\in S$ is the initial location, $\varDelta \subseteq S\times \varGamma \times S$ is the transition relation, and $S_f\subseteq S$ is a set of accepting locations (omitted if all locations are accepting). An STS with finitely many locations is a timed automaton ($\mathrm {TA}$) [1]. For a finite path $\pi = s_1\xrightarrow {b_1} s_2 \xrightarrow {b_2}\cdots \xrightarrow {b_{n}} s_{n+1}$ of $\mathcal T$ (i.e., such that $(s_i,b_i,s_{i+1})\in \varDelta$ for all $1\leqslant i\leqslant n$), the trace of $\pi$ is the word $b_1b_2\cdots b_{n}$, and $\pi$ is accepting if $s_{n+1}\in S_f$. We denote by $\mathcal L(\mathcal T)$ the language of $\mathcal T$, defined as the timed words associated to symbolic words that are traces of finite accepting paths starting in $s_0$. We say that a timed action $(t,\sigma )\in \mathbb {R}^{+}\times \varSigma$ is enabled in $\mathcal T$ at a pair $(s,\nu )$, denoted by $(t,\sigma )\in \mathsf {En}_\mathcal T(s,\nu )$, if there exists a transition $(s,(\sigma ,g,R),s')\in \delta$ such that $\nu +t\models g$. The STS $\mathcal T$ is time-deterministic if there are no distinct transitions $(s,(\sigma ,g_1,R_1),s_1)$ and $(s,(\sigma ,g_2,R_2),s_2)$ in $\varDelta$ and no valuation $\nu$ such that $\nu \models g_1$ and $\nu \models g_2$. In a time-deterministic STS $\mathcal T= (S,s_0,\delta ,S_f)$, for all timed words $\sigma$, there is at most one path $\pi$ whose trace $\gamma$ verifies $\sigma \in tw(\gamma )$. In that case, we denote by $\delta (s_0,\sigma )$ the unique (if it exists) pair $(s,\nu )$ (where $s\in S$ and $\nu$ is a valuation) reached after reading $\sigma \in tw(\gamma )$.

Example 1

A time-deterministic $\mathrm {TA}$ $\mathcal P$ with a single clock x is depicted in Fig. 2. Intuitively, it accepts all timed words $\sigma$ of the form $w_1w_2\cdots w_n$ where each $w_i$ is a timed word such that (i) either $w_i=(b,\tau )$; (ii) or $w_i$ is a sequence of a’s (starting at time stamp $\tau$) of duration at most 1; and $w_{i+1}$ is either of the form $(b,\tau ')$, or of the form $(a,\tau ')$ with $\tau '-\tau >1$.

Fig. 2.

(a) A time-deterministic STS $\mathcal P$ with $X=\{x\}$. Instead of depicting a transition per letter (a, g, R) (with g atomic), we merge several transitions; e.g., we skip the guard, when all the possible guards are admitted. $x:=0$ denotes the reset of x. (b) A time-deterministic STS $\mathcal T$. It is a controller to realise $\varphi =\square _{}(a\Rightarrow \lozenge _{\leqslant 1}b)$ with plant $\mathcal P$.

Reactive Synthesis with Plant. To define our reactive synthesis problems, we partition the alphabet $\varSigma$ into controllable and environment actions $\varSigma _C$ and $\varSigma _E$. Following [4, 12], the system is modelled by a time-deterministic $\mathrm {TA}$ $\mathcal P= (Q,q_0,\delta _\mathcal P,Q_f)$, called the plant ². Observe that the plant has accepting locations: only those runs ending in a final location of the plant will be checked against the specification. We start by recalling the definition of the general reactive synthesis family of problems ($\mathsf {RS}$) [10, 11]. It consists in a game played by the controller and the environment, that interact to create a timed word as follows. We start with the empty timed word, and then, at each round, the controller and the environment propose timed actions to be performed by the system—therefore, they must be firable in the plant $\mathcal P$—respectively (t, a) and $(t',b)$, with $t,t'\in \mathbb {R}^{+}$, $a\in \varSigma _C$ and $b\in \varSigma _E$. The timed action with the shortest³ delay (or the environment action if the controller decides not to propose any action) is performed, and added to the current play for the next round. If both players propose the same delay, we resolve the time non-deterministically.

On those games, we consider a parameterised family of reactive synthesis problems denoted $\mathsf {RS} _s^b(\mathcal {F})$, where $s\in \{u,d\}$; $b\in \{\star ,\omega \}$; and $\mathcal {F}$ is one of the formalisms in Fig. 1. An instance of $\mathsf {RS} _s^b(\mathcal {F})$ is given by a specification $S\in \mathcal {F}$ and a plant $\mathcal P$, which are interpreted over finite words when $b=\star$ and infinite words when $b=\omega$. The timed language $\mathcal L(S)$ is a specification of desired behaviours when $s=d$ and undesired behaviours when $s=u$. Then, $\mathsf {RS} _s^b(\mathcal {F})$ asks whether there exists a strategy for the controller such that all the words in the outcome of this strategy are in $\mathcal L(S)$ (or outside $\mathcal L(S)$) when we consider desired (or undesired) behaviours (when $s=\omega$, the definition of $\mathcal L(S)$ must be the infinite words one). If this is the case, we say that S is (finite-word) realisable for the problem under study. For example, $\mathsf {RS} _u^\omega (\mathsf {MITL})$ is the reactive synthesis problem where the inputs are a formula of $\mathsf {MITL}$ and a plant, which are interpreted over the infinite words semantics, and where the $\mathsf {MITL}$ formula specifies the behaviours that the controller should avoid. Unfortunately, the variants $\mathsf {RS}$ are too general, and a winning strategy might require unbounded memory:

Example 2

Consider the alphabet $\varSigma = \varSigma _C \uplus \varSigma _E$ with $\varSigma _C = \{b\}$ and $\varSigma _E = \{a\}$, a plant $\mathcal P$ accepting $T\varSigma ^\star$, and the specification defined by the $\mathsf {MTL}$ formula $\varphi = \square _{} \big ((a\wedge \lozenge _{\geqslant 1} a) \Rightarrow \lozenge _{=1} b \big )$. Clearly, a winning strategy for the controller is to remember the time stamps $\tau _1,\tau _2,\ldots$ of all a’s, and always propose to play action b one time unit later (note that if the environment blocks the time to prevent the controller from playing its b, the controller wins). However this requires to memorise an unbounded number of time stamps with a great precision.

Restrictions on RS. In practice, it makes more sense to restrict the winning strategy of the controller to be implementable by an STS, which has finitely many clocks (and if possible finitely many locations). Let us define formally what it means for an STS $\mathcal T= (S,s_0,\delta )$ to control a plant $\mathcal P$. We let $T\varSigma ^\star _{\mathcal T,\mathcal P}$ be the set of timed words consistent with $\mathcal T$ and $\mathcal P$, defined as the smallest set containing the empty timed word, and closed by the following operations. Let $\sigma$ be a word in $T\varSigma ^\star _{\mathcal T,\mathcal P}$, with $(q,\nu _\mathcal P)=\delta _\mathcal P(q_0,\sigma )$, $T=0$ if $\sigma =\varepsilon$, and $(c,T)\in \varSigma \times \mathbb {R}^{+}$ be the last letter of $\sigma$ otherwise. Then, we extend $\sigma$ as follows:

• either the controller proposes to play a controllable action (t, b), because it corresponds to a transition that is firable both in the controller and the plant. This action can be played ($\sigma$ is extended by $(b,T+t)$), as well as any environment action $(t',a)$ with $t'\leqslant t$ (the environment can overtake the controller). Formally, if $\delta (s_0,\sigma )=(s,\nu )$ is defined and $\mathsf {En}_\mathcal T(s,\nu )\,\cap \, \mathsf {En}_\mathcal P(q,\nu _\mathcal P)\cap (\mathbb {R}^{+}\times \varSigma _C)\ne \emptyset$: for all $(t,b)\in \mathsf {En}_\mathcal T(s,\nu )\cap \mathsf {En}_\mathcal P(q,\nu _\mathcal P)\cap (\mathbb {R}^{+}\times \varSigma _C)$, we let $\sigma \cdot (b,T+t)\in T\varSigma ^\star _{\mathcal T,\mathcal P}$ and $\sigma \cdot (a,T+t')\in T\varSigma ^\star _{\mathcal T,\mathcal P}$ for all $t'\leqslant t$ and $a\in \varSigma _E$ such that $(t',a)\in \mathsf {En}_\mathcal P(q,\nu _\mathcal P)$.

• Or the controller proposes nothing, then the environment can play all its enabled actions. Formally, if $\delta (s_0,\sigma )=(s,\nu )$ is defined and $\mathsf {En}_\mathcal T(s,\nu )\cap \mathsf {En}_\mathcal P(q,\nu _\mathcal P)\cap (\mathbb {R}^{+}\times \varSigma _C)=\emptyset$ and $\mathsf {En}_\mathcal P(q,\nu _\mathcal P)\cap (\mathbb {R}^{+}\times \varSigma _E)\ne \emptyset$, we let $\sigma \cdot (a,T+t')\in T\varSigma ^\star _{\mathcal T,\mathcal P}$ for all $(t',a)\in \mathsf {En}_\mathcal P(q,\nu _\mathcal P)\cap (\mathbb {R}^{+}\times \varSigma _E)$.

• Otherwise, we declare that every possible future allowed by the plant is valid, i.e., we let $\sigma \cdot \sigma '\in T\varSigma ^\star _{\mathcal T,\mathcal P}$ for all $\sigma \cdot \sigma '\in \mathcal L(\mathcal P)$. This happens when the controller proposes only actions that are not permitted by the plant while the environment has no enabled actions; or when the controller lost track of a move of the environment during the past.

Then, the $\mathsf {MTL}$ implementable reactive synthesis problem $\mathsf {IRS} ^\star _d(\mathsf {MTL})$ (on finite words and with desired behaviours) is to decide, given a plant $\mathcal P$ and a specification given as an $\mathsf {MTL}$ formula $\varphi$, whether there exists a set of clocks X, a symbolic alphabet $\varGamma$ based on $(\varSigma ,X)$, and a time-deterministic STS $\mathcal T$ over $\varGamma$ such that $T\varSigma ^\star _{\mathcal T,\mathcal P}\cap \mathcal L(\mathcal P)\subseteq \mathcal L(\varphi )\cup \{\varepsilon \}$.⁴

While the definition of $\mathsf {IRS} _d^\star (\mathsf {MTL})$ is more practical than that of $\mathsf {RS} _d^\star (\mathsf {MTL})$, it might still be too general because the clocks and symbolic alphabet the controller can use are not fixed a priori. In the spirit of [4, 12], we define three variants of $\mathsf {IRS}$. First, the $\mathsf {MTL}$ bounded-resources synthesis problem $\mathsf {BResRS} _d^\star (\mathsf {MTL})$ is a restriction of $\mathsf {IRS} _d^\star (\mathsf {MTL})$ where the granularity of the controller is fixed: given an $\mathsf {MTL}$ formula $\varphi$, and a granularity $\mu =(X,m,K)$, it asks whether there exists a $\mu$-granular symbolic alphabet $\varGamma$ based on $(\varSigma ,X)$, and a time-deterministic STS $\mathcal T$ over $\varGamma$ such that $T\varSigma ^\star _{\mathcal T,\mathcal P}\cap \mathcal L(\mathcal P)\subseteq \mathcal L(\varphi )\cup \{\varepsilon \}$. Second, the less restrictive $\mathsf {MTL}$ bounded-precision synthesis problem $\mathsf {BPrecRS} _d^\star (\mathsf {MTL})$ and $\mathsf {MTL}$ bounded-clocks synthesis problem $\mathsf {BClockRS} _d^\star (\mathsf {MTL})$ are the variants of $\mathsf {IRS}$ where only the precision and only the number of clocks are fixed, respectively. Formally, $\mathsf {BPrecRS} _d^\star (\mathsf {MTL})$ asks, given an $\mathsf {MTL}$ formula $\varphi$, $m\in \mathbb N$, and $K\in \mathbb N\setminus \{0\}$, whether there are a finite set X of clocks, an (X, m, K)-granular symbolic alphabet $\varGamma$ based on $(\varSigma ,X)$, and a time-deterministic STS $\mathcal T$ over $\varGamma$ such that $T\varSigma ^\star _{\mathcal T,\mathcal P}\cap \mathcal L(\mathcal P)\subseteq \mathcal L(\varphi )\cup \{\varepsilon \}$. $\mathsf {BClockRS} _d^\star (\mathsf {MTL})$ is defined similarly with an $\mathsf {MTL}$ formula $\varphi$, and a finite set of clocks X (instead of m, K) as input.

While we have defined $\mathsf {IRS}$, $\mathsf {BPrecRS}$, $\mathsf {BClockRS}$ and $\mathsf {BResRS}$ for $\mathsf {MTL}$ requirements, and in the finite words, desired behaviours case only, these definitions extend to all the other cases we have considered for $\mathsf {RS}$: infinite words, undesired behaviours, and all fragments of $\mathsf {MTL}$. We rely on the same notations as for $\mathsf {RS}$, writing for instance $\mathsf {BPrecRS} _u^\star (\mathsf {MITL})$ or $\mathsf {BClockRS} _d^\omega (\mathsf {coFlat\text {-}MTL})$, etc.

Example 3

Consider the instance of $\mathsf {IRS} _d^\star (\mathsf {MITL})$ where the plant accepts $T\varSigma ^\star$ and the specification is $\varphi =\square _{} (a\Rightarrow \lozenge _{\leqslant 1}b)$. This instance is negative ($\varphi$ is not realisable), since, for every time-deterministic STS $\mathcal T$, $(a,0)\in T\varSigma ^\star _{\mathcal T,\mathcal P}$ but is not in $\mathcal L(\varphi )$. However, if we consider now the plant $\mathcal P$ in Fig. 2(a), we claim that the STS $\mathcal T$ with one clock z depicted in Fig. 2(b) realises $\varphi$. Indeed, this controller resets its clock z each time it sees the first a in a sequence of a’s, and proposes to play a b when z has value 1, which ensures that all a’s read so far are followed by a b within 1 time unit. The restrictions enforced by the plant (which can be regarded as a sort of fairness condition) ensure that this is sufficient to realise $\varphi$ for $\mathsf {IRS} _d^\star (\mathsf {MITL})$. This also means that $\varphi$ is realisable for $\mathsf {BPrecRS} _d^\star (\mathsf {MITL})$ with precision $m=1$ and $K=1$; for $\mathsf {BClockRS} _d^\star (\mathsf {MITL})$ with set of clocks $X=\{z\}$; and for $\mathsf {BResRS} _d^\star (\mathsf {MITL})$ with granularity $\mu =(\{z\},1,1)$.

3 $\mathsf {BPrecRS}$ and $\mathsf {BClockRS}$ are Undecidable

Let us show that all the variants of $\mathsf {BPrecRS}$ and $\mathsf {BClockRS}$ are undecidable, whatever formalism from Fig. 1 we consider for the specification. This entails that all variants of $\mathsf {RS}$ and $\mathsf {IRS}$ are undecidable too (in particular $\mathsf {RS} _d^\star (\mathsf {ECL})$ which settles an open question of [11] negatively). To this aim, we show undecidability on the weakest formalisms in Fig. 1, namely: $\mathsf {coFlat\text {-}MTL}$, $\mathsf {Safety\text {-}MTL}$, $\textsf {Open}\text {-}\mathsf {MITL} ^{\mathrm {ns}}[\lozenge _{\infty }]$ and $\textsf {Closed}\text {-}\mathsf {MITL} ^{\mathrm {ns}}[\lozenge _{\infty }]$. Similar results have been shown for $\mathsf {MTL}$ (and for $\mathsf {Safety\text {-}MTL}$ as desired specifications) in [4] via a reduction from the halting problem for deterministic channel machines, but their proof depends crucially on punctual formulas of the form $\overline{\square }_{} (a \Rightarrow \overline{\lozenge }_{=1} b)$ which are not expressible in $\mathsf {MITL}$. Our original contribution here is to adapt these ideas to a formalism without punctual constraints, which is non-trivial.

Deterministic Channel Machines. A deterministic channel machine (DCM) $\mathcal {S} = \langle S, s_0, s_\textit{halt}, M, \varDelta \rangle$ can be seen as a finite automaton equipped with an unbounded fifo channel, where S is a finite set of states, $s_0$ is the initial state, $s_\textit{halt}$ is the halting state, M is a finite set of messages and $\varDelta \subseteq S \times \{m!, m? \mid m \in M \} \times S$ is the transition relation satisfying the following determinism hypothesis: (i) $(s, a, s') \in \varDelta$ and $(s, a, s'') \in \varDelta$ implies $s' = s''$; (ii) if $(s, m!, s') \in \varDelta$ then it is the only outgoing transition from s.

The semantics is described by a graph $G(\mathcal {S})$ with nodes labelled by (s, x) where $s \in S$ and $x \in M^\star$ is the channel content. The edges in $G(\mathcal {S})$ are defined as follows: (i) $(s, x) \xrightarrow {m!} (s', xm)$ if $(s, m!, s') \in \varDelta$; and (ii) $(s, mx) \xrightarrow {m?} (s', x)$ if $(s, m?, s') \in \varDelta$. Intuitively, these correspond to messages being written to or read from the channel. A computation of $\mathcal {S}$ is then a path in $G(\mathcal {S})$. The halting problem for DCMs asks, given a DCM $\mathcal {S}$, whether there is a computation from $(s_0, \varepsilon )$ to $(s_\textit{halt}, x)$ in $G(\mathcal {S})$ for some $x \in M^\star$.

Proposition 1

([6]). The halting problem for DCMs is undecidable.

It should be clear that $\mathcal {S}$ has a unique computation. Without loss of generality, we assume that $s_\textit{halt}$ is the only state in S with no outgoing transition. It follows that exactly one of the following must be true: (i) $\mathcal {S}$ has a halting computation; (ii) $\mathcal {S}$ has an infinite computation not reaching $s_\textit{halt}$; (iii) $\mathcal {S}$ is blocking at some point, i.e., $\mathcal {S}$ is unable to proceed at some state $s \ne s_\textit{halt}$ (with only read outgoing transitions) either because the channel is empty or the message at the head of the channel does not match any of the outgoing transitions from s.

Finite-Word Reactive Synthesis for $\mathsf {MITL}$. We now give a reduction from the halting problem for DCMs to $\mathsf {RS} ^\star _d(\mathsf {MITL})$. The idea is to devise a suitable $\mathsf {MITL}$ formula such that in the corresponding timed game, the environment and the controller are forced to propose actions in turn, according to the semantics of the DCM. Each prefix of the (unique) computation of the DCM is thus encoded as a play, i.e., a finite timed word. More specifically, given a DCM $\mathcal {S}$, we require each play to satisfy the following conditions:

C1 :

The action sequence of the play (i.e., omitting all timestamps) is of the form ${\textit{Nil}_\textit{C}}^\star \,s_0 a_0 s_1 a_1 \cdots$ where $\textit{Nil}_\textit{C}$ is a special action of the controller and $(s_i, a_i, s_{i+1}) \in \varDelta$ for each $i \geqslant 0$.

C2 :

Each $s_i$ comes with no delay and no two write or read actions occur at the same time, i.e., if $(a_i, \tau )(s_{i+1}, \tau ')(a_{i+1}, \tau '')$ is a substring of the play then $\tau = \tau '$ and $\tau < \tau ''$.

C3 :

Each m? is preceded exactly 1 time unit (t.u.) earlier by a corresponding m!

C4 :

Each m! is followed exactly 1 t.u. later by a corresponding m? if there are actions that occur at least 1 t.u. after the m! in question.

To this end, we construct a formula of the form $\varPhi \Rightarrow \varPsi$ where $\varPhi$ and $\varPsi$ are conjunctions of the conditions that the environment and the controller must adhere to, respectively. In particular, the environment must propose $s_i$’s according to the transition relation (C1 and C2) whereas the controller is responsible for proposing $\{m!, m? \mid m \in M\}$ properly so that a correct encoding of the writing and reading of messages is maintained (C2, C3, and C4). When both players obey these conditions, the play faithfully encodes a prefix of the computation of $\mathcal {S}$, and the controller wins the play. If the environment attempts to ruin the encoding, the formula will be satisfied, i.e., the play will be winning for the controller. Conversely, if the controller attempts to cheat by, say, reading a message that is not at the head of the channel, the environment can pinpoint this error (by proposing a special action $\textit{Check}^\leftarrow$) and falsify the formula, i.e., the play will be losing for the controller. In what follows, let $\varSigma _\textit{E} = S \cup \{\textit{Check}^\leftarrow , \textit{Check}^\rightarrow , \textit{Lose}, \textit{Nil}_\textit{E} \}$, $\varSigma _\textit{C} = \{ m!, m? \mid m \in M \} \cup \{\textit{Win}, \textit{Nil}_\textit{C}\}$, $\varphi _\textit{E} = \bigvee _{e \in \varSigma _\textit{E}} e$, $\varphi _\textit{C} = \bigvee _{c \in \varSigma _\textit{C}} c$, $\varphi _S = \bigvee _{s \in S} s$, $\varphi _\textit{W} = \bigvee _{m \in M} m!$, $\varphi _\textit{R} = \bigvee _{m \in M} m?$ and $\varphi _\textit{WR} = \varphi _\textit{W} \vee \varphi _\textit{R}$. Let us now present the formulas $\varphi _1,\varphi _2,\ldots$ and $\psi _1,\psi _2,\ldots$ needed to define $\varPhi$ and $\varPsi$.

We start by formulas enforcing condition C1. The play should start from $s_0$, alternate between E-actions and C-actions, and the controller can win the play if the environment does not proceed promptly, and vice versa for the environment:

$$\begin{aligned} \varphi _1&= \lnot \big (\textit{Nil}_\textit{C} \overline{\mathsf {U}}_{} (\varphi _\textit{E} \wedge \lnot s_0)\big )&\psi _1&= \lnot \big (\textit{Nil}_\textit{C} \overline{\mathsf {U}}_{} (\varphi _\textit{C} \wedge \lnot \textit{Nil}_\textit{C})\big ) \\ \varphi _2&= \lnot \overline{\lozenge }_{} (\varphi _\textit{E} \wedge \bigcirc _{\leqslant 1} \varphi _\textit{E})&\psi _2&= \lnot \overline{\lozenge }_{} (\varphi _\textit{C} \wedge \bigcirc _{\leqslant 1} \varphi _\textit{C}) \\ \varphi _3&= \lnot \overline{\lozenge }_{} (\varphi _\textit{WR} \wedge \bigcirc _{} \textit{Win})&\psi _3&= \lnot \overline{\lozenge }_{} (\varphi _S \wedge \lnot s_\textit{halt} \wedge \bigcirc _{} \textit{Lose}) \,. \end{aligned}$$

Both players must also comply to the semantics of $\mathcal {S}$:

$$\begin{aligned} \varphi _4&= \bigwedge _{\begin{array}{c} (s, a, s') \in \varDelta \\ b \notin \{s', \textit{Check}^\leftarrow , \textit{Check}^\rightarrow \} \end{array}} \lnot \overline{\lozenge }_{} (s \wedge \bigcirc _{} a \wedge \bigcirc _{} \bigcirc _{} b) &\psi _4&= \bigwedge _{\begin{array}{c} s \ne s_\textit{halt} \\ \forall s'\, (s, a, s') \notin \varDelta \end{array}} \lnot \overline{\lozenge }_{} ( s \wedge \bigcirc _{} a ) \,. \end{aligned}$$

Once the encoding has ended, both players can only propose $\textit{Nil}$ actions:

$$\begin{aligned}&\varphi _5 = \lnot \overline{\lozenge }_{} \big ((s_\textit{halt} \vee \textit{Check}^\leftarrow \vee \textit{Check}^\rightarrow \vee \textit{Lose} \vee \textit{Win}) \wedge \lozenge _{} (\varphi _\textit{E} \wedge \lnot \textit{Nil}_\textit{E}) \big ) \\&\psi _5 = \lnot \overline{\lozenge }_{} \big ((s_\textit{halt} \vee \textit{Check}^\leftarrow \vee \textit{Check}^\rightarrow \vee \textit{Lose} \vee \textit{Win}) \wedge \lozenge _{} (\varphi _\textit{C} \wedge \lnot \textit{Nil}_\textit{C}) \big ) \,. \end{aligned}$$

For condition C2, we simply state that the environment can only propose delay 0 whereas the controller always proposes a positive delay:

$$\begin{aligned} \varphi _6&= \lnot \overline{\lozenge }_{} (\varphi _\textit{WR} \wedge \bigcirc _{>0} \varphi _\textit{E}) \quad&\psi _6&= \overline{\square }_{} (\varphi _S \wedge \lnot s_\textit{halt} \wedge \bigcirc _{} \varphi _\textit{WR} \implies \bigcirc _{>0} \varphi _\textit{WR}) \,. \end{aligned}$$

Let us finally introduce formulae to enforce conditions C3 and C4. Note that a requirement like ‘every write is matched by a read exactly one time unit later’ is easy to express in $\mathsf {MTL}$, but not so in $\mathsf {MITL}$. Nevertheless, we manage to translate C3 and C4 in $\mathsf {MITL}$ by exploiting the game interaction between the players. Intuitively, we allow the cheating player to be punished by the other. Formally, to ensure C3, we allow the environment to play a $\textit{Check}^\leftarrow$ action after any m? to check that this read has indeed occurred 1 t.u. after the corresponding m!. Assuming such a $\textit{Check}^\leftarrow$ has occurred, the controller must enforce:

$$\begin{aligned}&\psi ^\leftarrow = \bigvee _{m \in M} \overline{\lozenge }_{} \big ( m! \wedge \overline{\lozenge }_{\leqslant 1} (m? \wedge \bigcirc _{} \textit{Check}^\leftarrow ) \wedge \overline{\lozenge }_{\geqslant 1} (m? \wedge \bigcirc _{} \textit{Check}^\leftarrow ) \big ) \,. \end{aligned}$$

Now, to ensure C4, the environment may play a $\textit{Check}^\rightarrow$ action at least 1 t.u. after a write on the channel. If this $\textit{Check}^\rightarrow$ is the first action that occurs more than 1 t.u. after the writing (expressed by the formula $\psi ^\rightarrow _\textit{fst}$), we must check that the writing has been correctly addressed, i.e., there has been an action exactly 1 t.u. after, and this action was the corresponding reading:

$$\begin{aligned}&\psi ^\rightarrow _\textit{fst}= \overline{\lozenge }_{} ( \varphi _\textit{W} \wedge \overline{\lozenge }_{<1} \theta _{1}^\rightarrow \wedge \overline{\lozenge }_{\geqslant 1} \theta _{0}^\rightarrow ) \\&\psi ^\rightarrow = \lnot \overline{\lozenge }_{} ( \varphi _\textit{W} \wedge \overline{\lozenge }_{<1} \theta _{1}^\rightarrow \wedge \overline{\lozenge }_{> 1} \theta _{0}^\rightarrow ) \wedge \psi ^\leftarrow [\textit{Check}^\rightarrow /\textit{Check}^\leftarrow ] \end{aligned}$$

where $\psi ^\leftarrow [\textit{Check}^\rightarrow /\textit{Check}^\leftarrow ]$ is the formula obtained by replacing all $\textit{Check}^\leftarrow$ with $\textit{Check}^\rightarrow$ in $\psi ^\leftarrow$, $\theta ^\rightarrow _0 = \varphi _\textit{WR} \wedge \bigcirc _{} \textit{Check}^\rightarrow$ and $\theta ^\rightarrow _1 = \varphi _\textit{WR} \wedge \bigcirc _{} \varphi _S \wedge \bigcirc _{} \bigcirc _{} \theta ^\rightarrow _0$. In the overall, we consider:

$$\begin{aligned}&\varphi _7 = \bigwedge _{m \in M} \lnot \overline{\lozenge }_{} (m! \wedge \bigcirc _{} \textit{Check}^\leftarrow ) \\&\psi _7 = (\overline{\lozenge }_{} \textit{Check}^\leftarrow \Rightarrow \psi ^\leftarrow ) \wedge \big ((\overline{\lozenge }_{} \textit{Check}^\rightarrow \wedge \psi ^\rightarrow _\textit{fst}) \Rightarrow \psi ^\rightarrow \big ) \,. \end{aligned}$$

Now let $\varPhi = \bigwedge _{1 \leqslant i \leqslant 7} \varphi _i$, $\varPsi = \bigwedge _{1 \leqslant i \leqslant 7} \psi _i$ and $\varOmega = \varPhi \Rightarrow \varPsi$.

Proposition 2

$\varOmega$ is finite-word realisable if and only if either (i) $\mathcal {S}$ has a halting computation, or (ii) $\mathcal {S}$ has an infinite computation not reaching $s_\textit{halt}$.⁵

Proof

(Sketch). If (i) or (ii) is true, $\varOmega$ can be realised by the controller faithfully encoding a computation of $\mathcal {S}$. If E proposes $\textit{Check}^\leftarrow$ or $\textit{Check}^\rightarrow$, the play will satisfy $\psi _7$. Otherwise, if $\mathcal {S}$ has an infinite computation not reaching $s_\textit{halt}$, the play can grow unboundedly and will satisfy all $\psi$’s, hence $\varOmega$.

Conversely, if $\mathcal {S}$ is blocking, then $\varOmega$ is not realisable. Indeed, either the controller encodes $\mathcal {S}$ correctly, but then at some point it will not be able to propose any action, and will be subsumed by the environment that will play $\textit{Lose}$. Or the controller will try to cheat, by (1) inserting an action m? not matched by a corresponding m! 1 t.u. earlier, or (2) writing a message m! that will not be read 1 t.u. later. For the first case, the environment can then play $\textit{Check}^\leftarrow$ right after the incorrect m?, and the play will violate $\psi ^\leftarrow$, hence $\psi _7$ and $\varOmega$. For the second case, the environment will play $\textit{Check}^\rightarrow$ after the first action occurring 1 t.u. after the unfaithful m! and the play will violate $\psi ^\rightarrow$.    $\square$

Now let $\varOmega ' = \varPhi \Rightarrow \varPsi \wedge \square _{} (\lnot s_\textit{halt})$, i.e., we further require the computation not to reach $s_\textit{halt}$. The following proposition can be proved almost identically.

Proposition 3

$\varOmega '$ is finite-word realisable if and only if $\mathcal {S}$ has an infinite computation not reaching $s_\textit{halt}$.

Corollary 1

$\mathcal {S}$ has a halting computation if and only if $\varOmega$ is finite-word realisable but $\varOmega '$ is not finite-word realisable.

It follows that if $\mathsf {RS} ^\star _d(\mathsf {MITL})$ is decidable, we can decide whether $\mathcal {S}$ has a halting computation. But the latter is known to be undecidable. Hence:

Theorem 1

$\mathsf {RS} ^\star _d(\mathsf {MITL})$ is undecidable.

Theorem 1 and its proof are the core results from which we will derive all other undecidability results announced at the beginning of the section.

Remark 1

One may show that $\mathsf {RS} ^\omega _d$ is undecidable for formulas of the form $\varPhi \Rightarrow \varPsi$ where $\varPhi$ and $\varPsi$ are conjunctions of $\mathsf {Safety\text {-}MTL} [\mathsf {U}_{0,\infty }]$ formulas by rewriting $\varphi _i$’s and $\psi _i$’s. This answers an open question of [9].

$\mathsf {BPrecRS}$ and $\mathsf {BClockRS}$ for $\mathsf {Safety\text {-}MTL}$, $\mathsf {coFlat\text {-}MTL}$, and $\mathsf {MITL}$. In the proof of Proposition 2, if $\mathcal {S}$ actually halts, the number of messages present in the channel during the (unique) computation is bounded by a number N. It follows that the strategy of C can be implemented as a bounded-precision controller (with precision $(m, K) = (1, 1)$ and N clocks) or a bounded-clocks controller (with precision $(m, K) = (\frac{1}{N}, 1)$ and a single clock). Corollary 1 therefore holds also for the bounded-precision and bounded-clocks cases, and $\mathsf {BPrecRS} ^\star _d(\mathsf {MITL})$ and $\mathsf {BClockRS} ^\star _d(\mathsf {MITL})$ are undecidable. By further modifying the formulas used in the proof of Proposition 2, we show that the undecidability indeed holds even when we allow only unary non-strict modalities with lower-bound constraints and require the constraints to be exclusively strict or non-strict, hence $\mathsf {BPrecRS} ^\star _d$ and $\mathsf {BClockRS} ^\star _d$ are undecidable too on $\textsf {Open}\text {-}\mathsf {MITL} ^{\mathrm {ns}}[\lozenge _{\infty }]$ and $\textsf {Closed}\text {-}\mathsf {MITL} ^{\mathrm {ns}}[\lozenge _{\infty }]$. This entails undecidability in the undesired specifications case because the negation of an $\textsf {Open}\text {-}\mathsf {MITL} ^{\mathrm {ns}}[\lozenge _{\infty }]$ is a $\textsf {Closed}\text {-}\mathsf {MITL} ^{\mathrm {ns}}[\lozenge _{\infty }]$ formula and vice-versa. Finally, we can extend our proofs to the infinite words case, hence:

Theorem 2

$\mathsf {RS} ^b_s(\mathsf {L})$, $\mathsf {IRS} ^b_s(\mathsf {L})$, $\mathsf {BPrecRS} ^b_s(\mathsf {L})$ and $\mathsf {BClockRS} ^b_s(\mathsf {L})$ are undecidable for , $s\in \{u,d\}$ and $b\in \{\star ,\omega \}$.

This result extends the previous undecidability proofs of [11] ($\mathsf {RS} ^\omega _d(\mathsf {ECL})$ is undecidable), and of [12] ($\mathsf {IRS} ^\star _d(\mathrm {TA})$ and $\mathsf {IRS} ^\star _u(\mathrm {TA})$ are undecidable). In light of these previous works, our result is somewhat surprising as the undecidability proof in [12] is via a reduction from the universality problem for timed automata, yet this universality problem becomes decidable when all constraints are strict [15].

Finally, it remains to handle the cases of $\mathsf {Safety\text {-}MTL}$ and $\mathsf {coFlat\text {-}MTL}$. Contrary to the case of $\mathsf {MTL}$, the infinite-word satisfiability problem is decidable for $\mathsf {Safety\text {-}MTL}$ [16] and the infinite-word model-checking problem is decidable for both $\mathsf {Safety\text {-}MTL}$ [16] and $\mathsf {coFlat\text {-}MTL}$ [5]. Nevertheless, our synthesis problems remain undecidable for these fragments. In particular, the result on $\mathsf {Safety\text {-}MTL}$ answers an open question of [4] negatively:

Theorem 3

$\mathsf {RS} ^b_s(\mathsf {L})$, $\mathsf {IRS} ^b_s(\mathsf {L})$, $\mathsf {BPrecRS} ^b_s(\mathsf {L})$ and $\mathsf {BClockRS} ^b_s(\mathsf {L})$ are undecidable for , $s\in \{u,d\}$ and $b\in \{\star ,\omega \}$.

4 Bounded-Resources Synthesis for $\mathsf {MITL}$ Properties

We have now characterised rather precisely the decidability border for $\mathsf {MITL}$ synthesis problems. In light of these results, we focus now on $\mathsf {BResRS} ^\star _d(\mathsf {MITL})$ (since $\mathsf {MITL}$ is closed under complement, one can derive an algorithm for $\mathsf {BResRS} ^\star _u(\mathsf {MITL})$ from our solution). Recall that the algorithm of D’Souza and Madhusudan [12], associated with the translation of $\mathsf {MITL}$ into $\mathrm {TA}$ [2] yields a 3EXPTIME procedure for these two problems. Unfortunately this procedure is unlikely to be amenable to efficient implementation. This is due to the translation from $\mathsf {MITL}$ to $\mathrm {TA}$ and the need to determinise a region automaton, which is known to be hard in practice. On the other hand, Bouyer et al. [4] present a procedure for $\mathsf {BResRS} ^\star _d(\mathsf {MTL})$ (which can thus be applied to $\mathsf {MITL}$ requirements). This algorithm is on-the-fly, in the sense that it avoids, if possible to build a full automaton for the requirement; and thus more likely to perform well in practice. Unfortunately, being designed for $\mathsf {MTL}$, its running time can only be bounded above by a non-primitive recursive function. We present now an algorithm for $\mathsf {BResRS} ^\star _d(\mathsf {MITL})$ that combines the advantages of these two previous solutions: it is on-the-fly and runs in 3EXPTIME. To obtain an on-the-fly algorithm, Bouyer et al. use one-clock alternating automata (OCATA) instead of $\mathrm {TA}$ to represent the $\mathsf {MITL}$ requirement. We follow the same path, but rely on the newly introduced interval-based semantics [7] for these automata, in order to mitigate the complexity. Let us now briefly recall these two basic ingredients.

OCATA and Interval Semantics. Alternating timed automata [16] extend (non-deterministic) timed automata by adding conjunctive transitions. Intuitively, conjunctive transitions spawn several copies of the automaton that run in parallel from the target states of the transition. A word is accepted iff all copies accept it. An example is shown in Fig. 3, where the conjunctive transition is the hyperedge starting from $\ell _0$. In the classical semantics, an execution of an OCATA is a sequence of set of states, named configurations, describing the current location and clock valuation of all active copies. For example, a prefix of execution of the automaton in Fig. 3 would start in $\{(\ell _0,0)\}$ (initially, there is only one copy in $\ell _0$ with the clock equal to 0); then $\{(\ell _0,0.42)\}$ (after letting 0.42 time units elapse); then $\{(\ell _0,0.42),(\ell _1,0)\}$ (after firing the conjunctive transition from $\ell _0$), etc. It is well-known that all formulas $\varphi$ of $\mathsf {MTL}$ (hence, also $\mathsf {MITL}$) can be translated into an OCATA $A_\varphi$ that accepts the same language [16] (with the classical semantics); and with a number of locations linear in the number of subformulas of $\varphi$. This translation is thus straightforward. This is the key advantage of OCATA over $\mathrm {TA}$: the complexity of the $\mathsf {MITL}$ formula is shifted from the syntax to the semantics—what we need for an on-the-fly algorithm.

Fig. 3.

An OCATA (with single clock y) accepting the language of $\square _{} (a\Rightarrow \lozenge _{\leqslant 1}b)$.

Then; in the interval semantics [7], valuations of the clocks are not points anymore but intervals. Intuitively, intervals are meant to approximate sets of (punctual) valuations: $(\ell ,[a,b])$ means that there are clock copies with valuations a and b in $\ell$, and that there could be more copies in $\ell$ with valuations in [a, b]. In this semantics, we can also merge two copies $(\ell , [a_1,b_1])$ and $(\ell , [a_2,b_2])$ into a single copy $(\ell , [a_1,b_2])$ (assuming $a_1\leqslant b_2$), in order to keep the number of clock copies below a fixed threshold K. It has been shown [7] that, when the OCATA has been built from an $\mathsf {MITL}$ formula, the interval semantics is sufficient to retain the language of the formula, with a number of copies which is at most doubly exponential in the size of the formula.

Sketch of the Algorithm. Equipped with these elements, we can now sketch our algorithm for $\mathsf {BResRS} _d^\star (\mathsf {MITL})$. Starting from an $\mathsf {MITL}$ formula $\varphi$, a plant $\mathcal P$ and a granularity $\mu = (X,m,K)$, we first build, in polynomial time, an OCATA $A_{\lnot \varphi }$ accepting $\mathcal L(\lnot \varphi )$. Then, we essentially adapt the technique of Bouyer et al. [4], relying on the interval semantics of OCATA instead of the classical one. This boils down to building a tree that unfolds the parallel execution of $A_{\lnot \varphi }$ (in the interval semantics), $\mathcal P$ and all possible actions of a $\mu$-granular controller (hence the on-the-fly algorithm). Since the granularity is fixed, there are only finitely many possible actions (i.e., guards and resets on the controller clocks) for the controller at each step. We rely on the region construction to group the infinitely many possible valuations of the clocks into finitely many equivalence classes that are represented using ‘region words’ [16]. The result is a finitely branching tree that might still have infinite branches. We stop developing a branch once a global configuration (of $A_{\lnot \varphi }$, $\mathcal P$, and the controller) repeats on the branch. By the region construction and the interval semantics, this will happen on all branches, and we obtain a finite tree of size at most triply exponential. This tree can be analysed (using backward induction) as a game with a safety objective for the controller: to avoid the nodes where $\mathcal P$ and $A_{\lnot \varphi }$ accept at the same time. The winning strategy yields, if it exists, a correct controller.

Table 1. Experimental results on the scheduling problem: realisable instances on the left, non-realisable on the right.

Experimental Results. We have implemented our procedure in Java, and tested it over a benchmark related to a scheduling problem, inspired by an example of [9]. This problem considers n machines, and a list of jobs that must be assigned to the machines. A job takes T time units to finish. The plant ensures that at least one time unit elapses between two job arrivals (which are uncontrollable actions). The specification asks that the assignment be performed in 1 time unit, and that each job has T time units of computation time. We tested this example with $T=n$, in which case the specification is realisable (no matter the number of clocks, which we make vary for testing the prototype efficiency), and with $T=n+1$, in which case it is not. Table 1 summarises some of our results.

These results show that our prototypes can handle small but non-trivial examples. Unfortunately—as expected by the high complexities of the algorithm—they do not scale well. As future works, we will rely on the well-quasi orderings defined in [4] to introduce heuristics in the spirit of the antichain techniques [13]. Second, we will investigate zone-based versions of this algorithm to avoid the state explosion which is inherent to region based techniques.