On the relation between reactive synthesis and supervisory control of non-terminating processes

Reactive synthesis (RS) addresses the systematic design of digital systems that dynamically interact with their environment by alternating input readings from discrete variables and output assignments to discrete variables. The progress of time is modelled by successive computation cycles and the current output assignment is considered to depend on all past input readings. Thus, the digital system imposes a causal feedback on the environment and it is therefore referred to as a reactive module.

The synthesis problem here is to construct a reactive module realised by a finite automaton that exhibits a behaviour that satisfies some prescribed specification. The problem of reactive synthesis was first proposed by Church (1957) with solutions by Büchi and Landweber (1969), and Rabin (1972). It is since then an active field of research, addressing temporal logic specifications (e.g. Pnueli and Rosner 1989; Emerson and Jutla 1991; Maler et al. 1995; Thomas 1995), partial observation (e.g. Kupferman and Vardi 2000), stochasticity (e.g. de Alfaro and Henzinger 2000, 2007; Chatterjee and Henzinger 2012), and, most relevant for this paper, environment assumptions (see Bloem et al. 2014; Brenguier et al. 2017 for an overview). For a comprehensive introduction to the field see e.g. Thomas (1995) and Finkbeiner (2016).

Supervisory Control Theory (SCT) is a branch of control theory that also addresses the systematic design of digital systems. It models systems as discrete-event systems — dynamical systems in which relevant variables are of finite range and in which changes of their respective values are referred to as events. The synthesis problem is to construct a controller that provides causal feedback to a given plant such that the closed-loop system satisfies a prescribed specification. For supervisory control, the plant is a discrete-event system and the causal feedback, referred to as the supervisor, maps the past event sequence to a control pattern in order to restrict the plant behaviour. Supervisory control theory was originally proposed by Ramadge and Wonham (1987) and now is an established field of research. Topics addressed include partial observation (e.g. Lin and Wonham 1988; Cieslak et al. 1988; Cai et al. 2015; Yin and Lafortune2016, 2017), robustness (e.g. Cury and Krogh 1999; Bourdon et al. 2005), modularity (e.g. Ramadge and Wonham 1989b; Rudie and Wonham 1992; de Querioz and Cury 2000), hierarchical control architectures (e.g. Zhong and Wonham 1990; Wong and Wonham 1996; Schmidt et al. 2008), fault-tolerance (e.g. Wen et al. 2008; Paoli et al. 2011; Moor 2016), and, most relevant for this report, behaviours over an infinite time-axis (e.g. Ramadge 1989a; Thistle and Wonham 1994a, 2009; Moor et al. 2011; Baier and Moor 2015; Zhang and Cai2018).

Both design methodologies seek to synthesise a causal feedback map that operates on a finite alphabet and satisfies a formal specification. When used on particular instances of a given synthesis problem, both techniques appear to be closely related. However, the technical details differ significantly. In this paper we provide a formal comparison, allowing us to identify conditions under which one can solve one synthesis problem via the respective other one and we discuss how the resulting solutions compare. To facilitate this comparison, we give a concise introduction to RS and SCT and derive formal problem statements and a characterisation of their solutions uniformly in terms of ω-languages. Recent contributions to the two fields focus attention on different aspects of the respective problem, and we expect the formal relationship identified in this paper to be useful in that it allows the application of algorithmic techniques from one field to the other.

Scope

Regarding reactive synthesis, our study considers a variant that explicitly addresses assumptions on the environment behaviour, as these assumptions correspond to the prescribed plant behaviour in supervisory control. For ease of comparison, we consider both the assumption and the specification to be given abstractly as ω-languages —formal languages of infinite words— and for algorithmic effectiveness, as ω-regular languages which allow automata-based representations. For ease of illustration, we restrict attention to specifications given as deterministic Bchi automata. While deterministic Büchi automata capture only a strict subset of ω-regular languages, it allows us to keep the notation and algorithms reasonably simple; our comparisons can be extended to the full class of all ω-regular specifications. While many papers on RS use specifications given in linear temporal logic (LTL) (see Pnueli 1977), it is well understood how such formulae can be translated into ω-automata (see Vardi and Wolper 1986; Safra 1988).

Regarding supervisory control, most of the literature, including the seminal work by Ramadge and Wonham (1987), refers to ∗-languages as their base model, i.e., formal languages of finite words. In this setting, synthesis can enforce safety properties while maintaining liveness properties present in the plant behaviour. This contrasts the design of reactive modules where the synthesis of liveness properties is conceived a relevant challenge. We therefore conduct our study for a branch of supervisory control that addresses the synthesis problem for ω-languages; (see Ramadge 1989a; Thistle and Wonham 1994a, 1995), where the authors explicitly relate their work to Church’s problem. For a comprehensive introduction to SCT for ω-languages see also the technical report by Moor (2017).

Contribution

Within this perspective of our choice, our contribution is threefold:

1. (I)

   We show that one can solve the considered RS problem using SCT and provide an algorithm over deterministic Büchi-automata realisations which ensures that the resulting reactive module will not falsify the assumptions on the environment.

2. (II)

   We show that one can solve the considered synthesis problem from SCT using RS for restricted subclasses of plant (resp. environment) behaviours.

3. (III)

   We establish equivalence of the two synthesis problems regarding solvability for the subclasses considered in (II).

The considered RS problem is formalised by an implication style logic formula, i.e., the specification is such that if the assumptions are satisfied, then a guarantee shall be provided. Hence, a valid solution to the synthesis problem might falsify the assumption. SCT seeks to avoid this issue by requiring that valid solutions to the synthesis problem need to be non-conflicting, i.e., at any point both the plant and the supervisor can fulfil their liveness properties eventually. Due to this additional property of solutions, our transformation in (I) achieves reactive modules which do not falsify the assumption. The reverse transformation in (II), however, only holds if the computed reactive module returns solutions which are non-conflicting. We identify three sufficient conditions for the latter to hold: (a) topologically closed, (b) topologically closed input/output, and (c) strongly non-anticipating input/output plant (resp. environment) behaviours.

When establishing result (II)(c), we identify a close relationship between strongly non-anticipating input/output plant behaviours (see Moor et al.2011) and non-falsifiable environment assumptions (see e.g. Brenguier et al. (2017)^{Footnote 1}) which ensure an almost identical form of non-conflictingness and which were derived independently in both communities.

Both synthesis algorithms are formalised as fixed-points in the μ-calculus. The RS algorithm uses a three-nested fixed-point while SCT synthesis amounts to a four-nested fixed-point. Result (I) clarifies that this additional fixed-point iteration indeed generates an additional property on the solution. Notably, this property cannot be encoded as an ω-regular property and hence, the SCT fixed-point cannot result from a translation of an LTL synthesis problem into a μ-calculus formula. Regarding result (II), we may expect some computational benefits as a trade-off when imposing conditions (a)-(c) on a synthesis problem in SCT. Moreover, we show that for topologically closed plant (resp. environment) behaviours with alternating inputs and outputs both fixed-points collapse to the same two-nested one. Using result (III)(b), the latter establishes equivalence of both algorithms in this case.

Related work

The problem of correctly handling assumptions in synthesis has recently gained attention in the reactive synthesis community. As our solution via SCT synthesis and result (I) does not assume precise knowledge about the environment strategy (or the ability to impose an environment strategy), it is distinct from assume-guarantee approaches (Chatterjee and Henzinger 2007) or rational synthesis (Fisman et al. 2010). It is closest related to obliging games (Chatterjee et al. 2010), cooperative reactive synthesis as in Bloem et al. (2015) and assume-admissible synthesis (Brenguier et al. 2017). Chatterjee et al. (2010) incorporate a similar notion of non-conflictingness as SCT, but in contrast to SCT does not utilise liveness properties of the environment assumptions to enforce the system guarantees. Bloem et al. (2015) synthesise a reactive module which assumes as little cooperation (w.r.t. to a given hierarchy of cooperation levels) as possible by the environment. Contrary, our approach via result (I) always assumes the same form of cooperation coinciding with just one cooperation level. Applying assume-admissible synthesis, the system and its environment results in two individual synthesis problems. Given that both have a solution, only implementing the solution for the system ensures that the specification is fulfilled if the environment only takes admissible moves. This is comparable to the view taken in this paper, however, the hypothesis that the environment behaves admissible is stronger than the hypothesis used for SCT, namely that the environment attains its liveness properties if not prevented from doing so. Moreover, our approach only requires to solve one synthesis problem, instead of two.

Our study complements the recent comparison between RS and SCT by Ehlers et al. (2017). There, the authors focus attention on SCT over ∗-languages and discuss maximal permissiveness of a solution to the synthesis problem. This contrasts our choice of ω-languages, where a maximally permissive solution fails to exist in general and, taking a perspective common in RS, we resort to computing some solution provided that one exists. Moreover, Ehlers et al. (2017) encode the requirement of a non-conflicting closed-loop, as it is commonly discussed in the context of SCT, by a specific CTL formula and solve the synthesis problem by a specialised variant of RS. In contrast, to obtain our result (II), we address a non-conflicting closed loop by structural assumptions on the problem parameters which imply that for the corresponding RS problem the assumptions are non-falsifiable by any reactive module.

Further, our work is in line with previous work establishing connections between supervisory control and other types of program synthesis, such as behavior composition (Barati and St-Denis 2015; Felli et al. 2017) or planning by model checking (Barveau et al. 1998). These works also discovered a strong connection between both fields which is used to apply established tools from one field to a problem statement of the other.

Outline

This paper is organised as follows. After recalling necessary notation and basic facts in Section 2, we give a concise but self-contained introduction to reactive synthesis and supervisory control in Sections 3 and 4, respectively. Here, synthesis problems are stated to respect the conventions used in the respective literature, with an additional uniform characterisation of solutions in terms of ω-languages to facilitate the comparison in Section 5, in which we develop our main results (I)–(III) as outlined above. Technical propositions and proofs are organised in the Appendices A–D. A preliminary version of this work appeared as Schmuck et al. (2018), focusing on input-output behaviours. The current paper extends this by establishing a solution of a synthesis problem from SCT via RS for arbitrary topologically closed behaviours in Section 5.2. Additionally, we provide more in-depth explanations, examples and proofs for the results already presented by Schmuck et al. (2018).

We provide common terminology and recall some elementary facts regarding formal languages, automata, two-player games and fixpoint calculus. A general introduction to these topics can be found in e.g. Hopcroft and Ullman (1979), Thomas (1990), Grädel et al. (2002), and Bradfield and Stirling (2006).

Formal languages

Let Σ be a finite alphabet. Then we write Σ^∗,Σ⁺, and Σ^ω for the sets of finite sequences, non-empty finite sequences, and infinite sequences over Σ, respectively. We define \({\Sigma }^{\infty } = {\Sigma }^{*} \cup {\Sigma }^{\omega }\). The subsets \(L\subseteq {\Sigma }^{*}\) and \({\mathcal{L}}\subseteq {\Sigma }^{\omega }\) are called the ∗- and ω-languages over Σ, respectively. For \({\Psi }\subseteq {\Sigma }\), the natural projection of w ∈Σ^∗ on Ψ^∗ is denoted by p_Ψw. As with all other operators on words used in this paper, we take point-wise images for an extension to languages over Σ, i.e., we write p_ΨL for {p_Ψs|s ∈ L} with \(L\subseteq {\Sigma }^{*}\). For two words s ∈Σ^∗ and \(t\in {\Sigma }^{\infty }\) we write \(st\in {\Sigma }^{\infty }\) for the concatenation. We write s ≤ t and s < t if s is a prefix of t or a strict prefix of t, respectively. The set of all prefixes of a word \(t\in {\Sigma }^{\infty }\) is denoted \({\textup {pfx}} t\subseteq {\Sigma }^{*}\). For \(L\subseteq {\Sigma }^{*}\), we have \(L\subseteq {\textup {pfx}} L\), and, if equality holds, we say that L is prefix closed. The limit\({{\lim }} L\) of \(L\subseteq {\Sigma }^{*}\) contains all words α ∈Σ^ω which have infinitely many prefixes in L and we define \({\text {clo}} {\mathcal{L}} :={{\lim }} {\textup {pfx}}\ {\mathcal{L}}\) as the topological closure of \({\mathcal{L}}\subseteq {\Sigma }^{\omega }\). \({\mathcal{L}}\) is said to be topologically closed if \({\mathcal{L}}={\text {clo}} {\mathcal{L}}\), and relatively topologically closed w.r.t. \({\mathcal{M}}\subseteq {\Sigma }^{\omega }\), if \({\mathcal{L}}=({\text {clo}} {\mathcal{L}}) \cap {\mathcal{M}}\). This notion of closedness defines a topology, i.e., ∅ and Σ^ω are closed, finite unions of closed ω-languages are closed, and arbitrary intersections of closed ω-languages are closed.

Automata

An automaton over the alphabet Σ is a tuple M = (Q,Σ, δ, Q_o) with the state setQ, the transition relation\(\delta \subseteq Q\times {\Sigma } \times Q\) and the set of initial states\(Q_{\mathrm {o}}\subseteq Q\). M is called finite if Q and δ are finite. We identify δ with its respective set-valued map δ : Q ×Σ⇝Q where \(\delta (q,\sigma ):=\{ q^{\prime } | (q,\sigma ,q^{\prime })\in \delta \}\subseteq Q\), and with the common inductive extension to a word-valued second argument s ∈Σ^∗. For \(P\subseteq Q\) and \(N\subseteq {\Sigma }^{*}\), we denote \(\delta (P, N):=\cup \{ \delta (q, s) | q\in P, s\in N \}\subseteq Q\) the image of P × N under δ. If |Q_o|≤ 1 and |δ(q, s)|≤ 1 for all q ∈ Q, s ∈Σ^∗, then M is said to be deterministic. For deterministic automata, we interpret δ as partial function and write \(\delta (q,s)=q^{\prime }\) and δ(q, s)! as short forms for \(\delta (q,s)=\{q^{\prime }\}\) and δ(q, s)≠∅, respectively. We define L = L^∗(M) := {s ∈Σ^∗|δ(Q_o, s)≠∅} and \({\mathcal{L}}=\mathrm {L}^{\omega }({M}):=\{ \alpha \in {\Sigma }^{\omega } | {\textup {pfx}}\ \alpha \subseteq \mathrm {L}^{*}({M}) \}\) as the ∗- and ω-languages generated by M, respectively, which are prefix closed and topologically closed, respectively.

Accepted languages

Given a set of final states\(F\subseteq Q\) and the extended automaton tuple M = (Q,Σ, δ, Q_o, F), its accepted ∗-language is defined by \(\mathrm {L}^{*}_{\mathrm {m}}({M}):=\{ s\in {\Sigma }^{*} | \delta (Q_{\mathrm {o}}, s)\cap F\neq \emptyset \}\). Regular ∗-languages are those that are accepted by some finite automaton.

For ω-languages, we refer to an acceptance condition\(\mathcal {F}\) and the extended automaton tuple \({M}=(Q, {\Sigma }, \delta , Q_{\mathrm {o}}, \mathcal {F})\). A run π of M is an infinite sequence of states q₁q₂q₃⋯ ∈ Q^ω and corresponds to the ω-word \(\alpha =\sigma _{1} \sigma _{2} \sigma _{3} \cdots \in {\Sigma }^{\omega }\) if q₁ ∈ Q_o and (q_i, σ_i, q_i+ 1) ∈ δ for all \(i\in \mathbb {N}\). The set of states that occur infinitely often in π is denoted Infπ. We use Büchi, generalized Büchi and Parity acceptance conditions. The Büchi acceptance condition is given by a set \(\mathcal {F}\subseteq Q\) and a runπ over M is accepted if \(({\text {Inf}}\pi ) \cap \mathcal {F}\neq \emptyset \). Similarly, the generalized Büchi acceptance condition is given by a set \(\mathcal {F}=\{F_{1},F_{2},\hdots ,F_{k}\}\) s.t. HCode \(F_{i}\subseteq Q\), and a run π is accepted if (Infπ) ∩ F_i≠∅ for all i ∈{1,…, k}. Finally, the parity acceptance condition is given by a set of colors \(\mathcal {F}=\{C_{1},C_{2},\hdots ,C_{k}\}\) which is defined by a coloring function \(c:Q{\rightarrow }\{1,...,k\}\), s.t. C_k = {q ∈ Q}c(q) = k, and a run π is accepted if the highest color visited infinitely often is even, i.e., if \({\max \limits } \text {Inf} c(\pi )\) is even. An automaton M with Büchi, generalized Büchi or Parity acceptance condition is referred to as a Büchi, generalized Büchi or Parity automaton, respectively. The accepted ω-language \(\mathrm {L}^{\omega }_{\mathrm {m}}({M})\) consists of all words α ∈Σ^ω for which there exists a corresponding accepted run over M. For deterministic automata, we have \(\mathrm {L}^{\omega }_{\mathrm {m}}({M}) = \lim \mathrm {L}_{\mathrm {m}}^{*}({M})\). Referring to an acceptance condition, we say that the automaton M is trim if for every state q there exists an accepted run that passes q at least once. The class of ω-languages that is accepted by some finite Büchi, generalized Büchi or parity automaton is referred to as the ω-regular languages. The class of ω-languages that is accepted by some deterministic finite Büchi automaton is a strict subset of the ω-regular languages while any ω-regular language is accepted by some deterministic parity automaton.

Two-player games

Let Σ = Σ⁰ ∪Σ¹ be a disjoint composition of symbols and let \({M}=({Q^0}\cup {Q^1}, {\Sigma }^{0}\cup {\Sigma }^{1}, \{ q_{0}\}, {\delta ^0}\cup {\delta ^1}, \mathcal {F})\) be a deterministic automaton s.t. HCode \(q_{0}\in {Q^0}, {\delta ^0}\subseteq {Q^0}\times {\Sigma }^{0}\times {Q^1}\) and \(\delta ^{1}\subseteq {Q^{1}}\times {\Sigma }^{1}\times {Q^{0}}\). Then the tuple H = (Q⁰, Q¹,Σ⁰,Σ¹, δ⁰, δ¹) defines the turn-based two player game graph induced by M, where Q^l,Σ^l and δ^l with l ∈{0,1} are interpreted as the player l state set, alphabet and transition set, respectively. Any run π of M is called a play over H. Given a game graph H, a strategy for player 0 is a function \(f^{0}: ({Q^0}{Q^1})^{*}{Q^0}\rightarrow {\Sigma }^{0}\). A play π is compliant with f⁰ if for all \(k\in {\mathbb {N}}\) with π(k) ∈ Q⁰ it holds that π(k + 1) = δ⁰(π(k), f⁰(π|_{[1, k]})), where π|_{[1, k]} = π(1)π(2)…π(k). Strategies for player 1 are defined likewise, i.e., as functions \(f^{1}: ({Q^0}{Q^1})^{+}\rightarrow {\Sigma }^{1}\) and with a play π being compliant with f¹ if π(k + 1) = δ¹(π(k), f¹(π|_{[1, k]})) for all \(k\in {\mathbb {N}}\) with π(k) ∈ Q¹. A strategy f^l, l ∈{0,1}, is memoryless if f^l(νq) = f^l(q) for all ν ∈ (Q⁰ ∪ Q¹)^∗ such that νq is in the domain of f^l. Throughout this paper, we discuss games from the perspective of exclusively one of the two players and interpret the Büchi (reps. parity) acceptance condition \(\mathcal {F}\) for this player. The tuple (\(H,\mathcal {F}\)) if it is an accepted run in M. A strategy f^l, l ∈{0,1}, is a winning strategy for player l if all plays compliant with f^l are winning.

Fixpoint calculus

We utilize the following notational conventions from the μ-calculus. Let f denote a monotone operator on a finite set Q, i.e., \(f(P^{\prime })\subseteq f(P^{\prime \prime })\subseteq Q\) for all \(P^{\prime }\subseteq P^{\prime \prime }\subseteq Q\). Then the least and the greatest fixed point exist uniquely and are denoted μP.f(P) and νP.f(P), respectively. They can be computed by the iterations P₁ := ∅, P_i+ 1 := P_i ∪ f(P_i), with \(\mu P . f(P) = \cup \{ P_{i} | i\in \mathbb {N} \}\), and P₁ := Q, P_i+ 1 := P_i ∩ f(P_i), with \(\nu P . f(P) = \cap \{ P_{i} | i\in \mathbb {N} \}\). If f is given as an expression in terms of multiple set-valued parameters with range Q, and if this expression is monotone in each parameter, so are the respective fixed points. For such monotone expressionsf, fixed-point formulae can be nested.

This section gives a concise introduction to reactive synthesis with environment assumptions, derives a formal problem statement, and a characterisation of its solutions in terms of ω-languages. For illustration purposes, we recall an algorithmic solution of the synthesis problem for the specific case where all relevant ω-languages are provided as deterministic Büchi automata.

3.1 Reactive modules

A reactive module is a device that reads the values of input variables in order to assign values to output variables, and that, over time, does so once in every computation cycle. A reactive module is commonly represented as a function r that maps the sequence of past input readings s ∈ U⁺, to the current output assignment y ∈ Y, i.e,

Considering infinitely many computation cycles, the interaction of a reactive module with its environment generates an infinite sequence α ∈ (UY )^ω of alternating input readings and output assignments. Therefore, the behaviour of a reactive module \(r:U^{+} {\rightarrow } Y\) is defined as the ω-language \({\mathcal{L}}\) of all sequences α that comply with r over all computation cycles :

If, in addition, r is implemented as a finite automaton, then \({\mathcal{L}}\) is ω-regular.^{Footnote 2} From the infinite time behaviour \({{\mathcal{L}}}\) we recover the local behaviour by taking the prefix \({\textup {pfx}}\ {{\mathcal{L}}}\) and obtain a representation on a per-computation-cycle basis. Since the behaviour of a reactive module is exclusively characterised by individual computation cycles, we have \({\mathcal{L}}=\lim {\textup {pfx}}\ {\mathcal{L}}=:\text {clo}{\mathcal{L}}\) and, hence, \({\mathcal{L}}\) is topologically closed; see also Lemma 1.

For our subsequent discussion we will eliminate the explicit reference to the reactive module \(r:{U}^{+} {\mathsf {\rightarrow }} {Y}\) by utilising a direct characterisation of those languages \({\mathcal{L}}\) that qualify for a representation by Eq. 2. Referring to behavioural systems theory by J. C. Willems (1991), we adapt the notion of input-output systems to the notation used in the present paper.^{Footnote 3}

Definition 1

Given an ω-language \({\mathcal{L}}\subseteq ({U}{Y})^{\omega }\) or \({\mathcal{L}}\subseteq ({Y}{U})^{\omega }\) of alternating inputs and outputs, with U, Y ≠∅ and U ∩ Y = ∅, we say that

1. (i)

   Uis a locally free input for \({{\mathcal{L}}}\) if

   \(\forall s\in {\textup {pfx}}\ {\mathcal{L}}\ .\ \forall u^{\prime },u^{\prime \prime }\in {U}\ .\ su^{\prime }\in {\textup {pfx}}\ {\mathcal{L}}\ \rightarrow su^{\prime \prime }\in {\textup {pfx}}\ {\mathcal{L}} \);

2. (ii)

   the output locally processes the input if

   \(\forall s\in {\textup {pfx}}\ {\mathcal{L}}\ .\ \forall y^{\prime },y^{\prime \prime }\in {Y}\ .\ sy^{\prime }\in {\textup {pfx}}\ {\mathcal{L}} \wedge sy^{\prime \prime }\in {\textup {pfx}}\ {\mathcal{L}} \ \rightarrow \ y^{\prime }=y^{\prime \prime } \).

The above notion of inputs and outputs enables the following characterisation of behaviours associated with some reactive module.

Lemma 1

Let U, Y ≠∅, U ∩ Y = ∅and\(r:{U}^{+} {\mathsf {\rightarrow }} {Y}\). Then the associated behaviour\({\mathcal{L}}\subseteq ({U}{Y})^{\omega }\)of rdefined by Eq. 2is non-empty and it holds that:

• (RM1)\({\mathcal{L}}\)is topologically closed,

• (RM2) Uis a locally free input for\({{\mathcal{L}}}\), and

• (RM3) the output locally processes the input.

Vice versa, if a non-empty language\({\mathcal{L}}\subseteq ({U}{Y})^{\omega }\)satisfies conditions (RM1) – (RM3), then there exists a reactive module\(r:{U}^{+} {\mathsf {\rightarrow }} {Y}\)with associated behaviour\({\mathcal{L}}\)s.t. r(v) is the unique element of the singleton set

for v ∈ U⁺.

3.2 Problem statement (RS)

The problem commonly referred to as reactive synthesis is about the systematic design of a reactive module, henceforth also referred to as the system, that provides a formal guarantee\({\mathcal {G}}\subseteq (UY)^{\omega }\). In the basic setting of reactive synthesis, it is assumed that any input symbol may be generated by the environment at any time and that, in turn, the environment accepts any output symbol generated by the system. Then, properties (RM2) and (RM3) of \({\mathcal{L}}\) ensure that the interaction of the system with its environment can be continued for infinitely many computation cycles, i.e., the two components do not deadlock. Thus, we end up with an ω-word \(\alpha \in {{\mathcal{L}}}\). In turn, the system to provide the guarantee \({\mathcal {G}}\) amounts to the language inclusion specification \({{\mathcal{L}}}\subseteq {\mathcal {G}}\). The crucial point here is that \({\mathcal {G}}\) may express liveness properties which can not be characterised on a per-computation-cycle basis. Hence, we do not necessarily have equality in \({\mathcal {G}}\subseteq \lim {\textup {pfx}}\ {\mathcal {G}}\); i.e., \({\mathcal {G}}\), in contrast to \({\mathcal{L}}\), may not be topologically closed.

In many applications, an arbitrary behaviour of the environment is considered unrealistic, and one explicitly accounts for formal assumptions imposed on the environment. For the purpose of our discussion, we parameterise such assumptions by an ω-language \({\mathcal {A}}\subseteq (UY)^{\omega }\) to express that over infinitely many computation cycles the environment will produce input symbols such that we end up with an ω-word \(\alpha \in {\mathcal {A}}\). The intention here is to synthesise the system according to the inclusion \({{\mathcal{L}}}\subseteq {\mathcal {A}}\rightarrow {\mathcal {G}}:=((U\cup Y)^{\omega } - {\mathcal {A}}) \cup {\mathcal {G}}\) and to then conclude \(\alpha \in {\mathcal {G}}\) for any \(\alpha \in {\mathcal {A}}\). A consequence of this concept of an environment assumption is that over finitely many computation cycles the environment must comply to the local behaviour \({\textup {pfx}}\ {\mathcal {A}}\). This in turn restricts the output symbols that the reactive module may generate in each individual computation cycle in order be operational over infinitely many cycles. Technically, we require that the system and the environment do not deadlock, i.e.,

This amounts to the following problem statement for the synthesis of a reactive module.

Problem 1 (Reactive Synthesis under Environment Assumptions)

Given two non-empty finite sets of input symbolsU and output symbolsY, U ∩ Y = ∅, an environment assumption\({\mathcal {A}}\subseteq (UY)^{\omega }\) and a guarantee\({\mathcal {G}}\subseteq (UY)^{\omega }\), the reactive synthesis problem\(\mathsf {RS}[U, Y, \mathcal {A}, \mathcal {G}]\) asks to either construct a system such that the associated behaviour \({\mathcal{L}}\) does not deadlock with \({\mathcal {A}}\), see Eq. 4, and such that

or, to verify that no such system exists.^{Footnote 4}

Note that \( \mathcal {A}\rightarrow (\mathcal {G} \cap \mathcal {A}) =\mathcal {A}\rightarrow \mathcal {G} \), and, hence, we can restrict our discussion without loss of generality to the case where \(\emptyset \neq \mathcal {G}\subseteq \mathcal {A}\subseteq (UY)^{\omega }\). Furthermore, we can choose \({\mathcal {A}}=(UY)^{\omega }\) to recover the basic setting without assumptions from our formal problem statement, i.e., in this case, Eq. 4 is trivially satisfied and the system to provide the guarantee collapses to the simple inclusion \({\mathcal{L}}\subseteq {\mathcal {G}}\).

With Lemma 1, the problem of reactive synthesis amounts to the construction of a non-empty subset \({\mathcal{L}}\subseteq {\mathcal {A}}\rightarrow {\mathcal {G}}\) that satisfies (RM1) – (RM3) and that does not deadlock, Eq. 4, or to the verification that no such subset exists. Henceforth, we may refer to a qualifying behaviour \({\mathcal{L}}\) as a solution of the synthesis problem.

Remark 1

The problem of reactive synthesis is more commonly formalised by using specifications given in linear temporal logic (LTL) over a set of atomic propositions \({\mathcal {{U}}} \cup {\mathcal {{Y}}}\) (see, e.g., Pnueli and Rosner 1989). Such an LTL formula φ over \(\mathcal {U}\cup \mathcal {Y}\) can be translated into a specification language \({\mathcal {G}}\subseteq (UY)^{\omega }\) with \(U=2^{\mathcal {U}}\) and \(Y=2^{\mathcal {Y}}\) by constructing a Büchi automaton from φ, and then, for algorithmic reasons, determinising this automaton to obtain a deterministic Rabin or Parity automaton.

This transformation is well understood (Vardi and Wolper 1986; Safra 1988); see e.g. Finkbeiner (2016) for a comprehensive discussion.

Remark 2

In the reactive synthesis literature, environment assumptions are usually specified by a separate LTL formula which is then translated to an automaton as outlined in Remark 1, or they are directly given as an automaton model. In either case, the automaton may exhibit reachable states from which on the acceptance condition can not be satisfied, i.e., we may have that the generated language \(A_{\textup {loc}}\subseteq (UY)^{*}\) is a strict super-set of the prefix \({\textup {pfx}}\ {\mathcal {A}}\) of the accepted language \({\mathcal {A}}\). The requirement of the system and the environment not to deadlock, Eq. 4, is then substituted by

However, if we synthesise a system with behaviour \({{\mathcal{L}}}\) in which there indeed exist words \(s\in {A_{\text {loc}}} \cap ({\textup {pfx}}\ {\mathcal{L}})\) with \(s\not \in {\textup {pfx}}\ {\mathcal {A}}\), any extension α ∈ (UY )^ω, s < α, of such a word is not in \({\mathcal {A}}\). Hence, \({{\mathcal{L}}}\)falsifies the assumption and we may after infinitely many computation cycles end up with an ω-word \(\alpha \not \in {\mathcal {G}}\). This is undesirable and we will identify further more subtle variations of this issue in due course of our study. To this end, we restrict the discussion to the case of \(A_{\textup {loc}}={\textup {pfx}}\ {\mathcal {A}}\), i.e., we parameterise the assumption as a single ω-language \({\mathcal {A}}\) and we refer to its prefix \({\textup {pfx}}\ {\mathcal {A}}\) as the associated local behaviour.

3.3 Algorithmic solution

The interaction of the system and its environment outlined above can be viewed as a turn-based two player game: in every round the environment player selects an input u ∈ U and the system selects the output y ∈ Y. It was shown by Gurevich and Harrington (1982) and Pnueli and Rosner (1989) that for ω-regular specifications there exists a winning strategy for the system player in this game if and only if the reactive synthesis problem has an ω-regular solution \({\mathcal{L}}\). Based on this result, a solution can be obtained by constructing a deterministic game, finding a winning strategy for the system player and translating this strategy into a finite automaton representing the reactive module. For a concise presentation of this construction, we consider the special case in which both \({\mathcal {G}}\) and \({\mathcal {A}}\) are realisable as deterministic Büchi automata. While this does not imply that \({\mathcal {A}}\rightarrow {\mathcal {G}}\) can be realised by a deterministic Büchi automaton, there still exists a direct and simple solution procedure for this case, which we briefly recall.

We refer to the previous section and restrict, without loss of generality, the discussion to the case of \(\emptyset \neq {\mathcal {G}}\subseteq {\mathcal {A}}\). Given this setting, we consider a generalised Büchi automaton M with acceptance condition \(\mathcal {F}=\{{T^{0}},{T^{1}}\}\) s.t. HCode \({\mathcal {A}}=\mathrm {L}^{\omega }_{\mathrm {m}}({M_{{\mathcal {A}}}}), {\mathcal {G}}=\mathrm {L}^{\omega }_{\mathrm {m}}({M_{{\mathcal {G}}}})\) and \({\textup {pfx}}({\mathcal {A}})=\mathrm {L}^{*}({M})\), where \({M_{{\mathcal {A}}}}\) and \({M_{{\mathcal {G}}}}\) refer to the simple Büchi automaton obtained from M by using the single winning state set T⁰ and T¹, respectively. Additionally, we assume that M does not deadlock^{Footnote 5}. We refer to \({\mathcal {G}}\subseteq {\mathcal {A}} \subseteq ({U}{Y})^{\omega }\) to observe that the alternation of input readings and output assignments induces a disjoint union decomposition of the state set and the transition relation, i.e., M can be defined by the tuple

s.t. \({q}_{0}\in {Q^0}, {\delta ^0}\subseteq {Q^0}\times {U}\times {Q^1}, {\delta ^1}\subseteq {Q^1}\times {Y}\times {Q^0}\) and \({T^0},{T^1}\subseteq Q=Q^0\cup Q^1\).

The generalised Büchi automaton M defines the turn-based deterministic game graph H = (Q⁰, Q¹, U, Y, δ⁰, δ¹). In the context of the reactive synthesis problem, player 0 and player 1 are the environment and system player, respectively, and a system player winning strategy must ensure that all plays on H that visit T⁰ infinitely often, must also visit T¹ infinitely often. This can be expressed by the four-colour parity game \(({H},\mathcal {C})\) with \(\mathcal {C}=\{\emptyset ,\backslash Q {{T^{0}}},{T^{0}},{T^{1}}\}\), where C₂ = ∖QT⁰ and C₄ = T¹ are the sets with even colour. Hence, a play π according to α on H is winning for \(({H},\mathcal {C})\) if either T⁰ is not visited infinitely often, i.e. \(\alpha \notin \mathcal {A}\) or, else, if T⁰ is visited infinitely often, then T¹ is also visited infinitely often, i.e., \(\alpha \in {\mathcal {A}}\cap {\mathcal {G}}\). Both cases together amount to \(\alpha \in {\mathcal {A}}\rightarrow {\mathcal {G}}\). Note also that, by construction, we have \(\alpha \in \text {clo}{\mathcal {A}}\) for any play α on H.

It was shown in Emerson and Jutla (1991) that the winning states for the system player in the 4-colour parity game can be computed by the fixed-point

where \({\mathsf {Pre}^1}:{2^{Q}}{\mathsf {\rightarrow }}{2^{Q}}\) is the player 1 controllable prefix, defined for a set \(A\subseteq {Q}\) by

However, as C₁ is empty, Eq. 8 simplifies to the three-nested fixed point

If \(q_{0}\in {\mathsf {Win}^{1}}\), the synthesis problem has a solution and a memoryless winning strategy for the system player can be derived from the iterations in Eq. 10 as follows.

Consider the last iteration of the fixed-point in Eq. 10 resulting in the set \(X_{4}^{\infty }={\mathsf {Win}^{1}}\subseteq Q\) and assume that we have to iterate over X₃ k-times before this fixed-point is reached. If \({X_{3}^{i}}\) is the set obtained after the i-th iteration, we have that \(X_{4}^{\infty }=\bigcup _{i=0}^{k} {X_{3}^{i}}\) with \({X^{i}_{3}}\subseteq X_{3}^{i+1}, {X_{3}^{0}}=\emptyset \) and \({X_{3}^{k}}=X_{3}^{\infty }\). This defines a ranking for every state \(q\in X_{4}^{\infty }\) s.t.

Then \(f^{1}:{Q^1}\cap {X}_{4}^{\infty }\rightarrow {Y}\) is a winning strategy for the system player in the Parity game \(({H},\mathcal {C})\) if y = f¹ implies rank(δ¹(q, y)) < rank(q) if rank(q) > 1 and \(\delta ^{1}(q,y)\in X_{4}^{\infty }\) otherwise. It should be observed that f¹ defines r in Eq. 1 in the obvious way s.t. r(p_Us) = f¹(q) iff δ(q₀, s) = q. A finite automaton realising r (and therefore \({\mathcal{L}}\)) is obtained by pruning M from all states \(q\notin X_{4}^{\infty }\) and all transitions \((q,y,q^{\prime })\) s.t. yf¹(q). A proof that this winning strategy indeed defines a reactive module solving Problem 1 can be obtained as a special case of the construction presented in Bloem et al. (2012).

Remark 3

Referring back to Remark 2, the outlined synthesis algorithm generalises to the case where \({\mathcal {G}}\) is not necessarily a subset of \({\mathcal {A}}\) and \({\textup {pfx}}\ {\mathcal {A}}\subsetneq {A_{\text {loc}}}\). By following the same construction as in footnote 5, we obtain an automaton M which accepts \({\mathcal {A}}=\mathrm {L}^{\omega }_{\mathrm {m}}({M_{{\mathcal {A}}}})\) and \({\mathcal {G}}\cap ({{\lim }} {A_{\text {loc}}})=\mathrm {L}^{\omega }_{\mathrm {m}}({M_{{\mathcal {G}}}})\) and which generates \({A_{\text {loc}}}=\mathrm {L}^{*}({M})\).

Remark 4

In the special case where \({\mathcal {A}}\) is topologically closed, we can assume without loss of generality that T⁰ = Q and, hence, C₂ = ∅ and C₃ = Q. Then, the synthesis formula in Eq. 10 simplifies to

This observation can be equally motivated by noting that for T⁰ = Q, the Parity game \(({H},\mathcal {C})\) reduces to (H,{Q ∖ T¹, T¹}) which is equivalent to the Büchi game (H, T¹). It is well known that Büchi games (H, T¹) are solvable by the fixed-point in Eq. 12; see e.g. Maler et al. (1995) and Zielonka (1998). In this context, the basic version of reactive synthesis without environment assumptions results in computing a system winning strategy in the Büchi game \(({H}^{\prime },{F^1})\) where \({H}^{\prime }\) is the game graph obtained from M¹ (given that \({\mathcal {G}}\) is realisable by the deterministic Büchi automaton M¹). In other words, adding a topologically closed environment assumption \({\mathcal {A}}\), algorithmically amounts to solving the basic reactive synthesis problem via Eq. 12 over M in Eq. 7 instead of M¹.

Example 1

Consider a topologically closed assumption \({\mathcal {A}}\) as discussed in Remark 4 s.t. HCode \({\textup {pfx}}\ {\mathcal {A}}\) is the language generated by M depicted in Fig. 1 and \({\mathcal {G}}\) is accepted by M with final state set T¹ = {q₅}. Using Eq. 12 to solve this synthesis problem results in the winning state set Win¹ = {q₃, q₄, q₅, q₆} (indicated by the dashed square in Fig. 1).

Transition structure of the automaton M in Eq. 7 discussed in Example 1-2. Environment and system states Q⁰ and Q¹ are indicated by circles and squares, respectively. The final states T⁰ = {q₄} and T¹ = {q₅} are indicated in blue and red, respectively

Full size image

As \(q_{0}\notin {\mathsf {Win}^{1}}({F^1})\), Problem 1 has no solution in this example. If q₃ would be an initial state, it should be noted that the resulting system strategy would transition from q₃ in q₄ as rank(q₃) = 3, rank(q₄) = 2 and rank(q₆) = 4.

Example 2

Consider the assumption \({\mathcal {A}}\) given by the language accepted by M in Fig. 1 with accepting state set T⁰ = {q₄}. In this case, we evaluate (10) and obtain Win¹ = Q. Using Eq. 11, all states in Q ∖ T⁰ have rank 1 while q₄ has rank 2. This implies that the resulting system strategy will transition from q₃ to q₆.

The problem discussed in Example 1 fails to have a solution, as the environment can prevent the system from reaching q₃ from the initial state. Interestingly, adding liveness to the environment using the restricted final state set T⁰ = {q₄} in Example 2 does not directly resolve this problem. The implication-style specification used in the formal statement of Problem 1 rather adds more sequences to the set of winning plays if \({\mathcal {A}}\) is not topologically closed; every sequence which does not conform with \({\mathcal {G}}\) (i.e., does not reach q₅ infinitely often) is still winning as long as it does not conform with the assumptions \({\mathcal {A}}\) (i.e., does not visit q₄ infinitely often) either. As this is true for the sequence iterating between q₁ and q₂ and preventing the system to reach q₃, the synthesis problem now has a solution. Furthermore, choosing to transition to q₄ or q₆ from q₃ is now equally good. While always choosing the former ensures to win by visiting both q₄ and q₅ infinitely often, the latter ensures to win by visiting neither q₄ nor q₅ at all. Example 2 shows that the constructed strategy actually favours a transition from q₃ to q₆, and by this falsifies the assumption.

The purpose of this section is to give a concise introduction to supervisory control and to do so from a perspective and in a notation most convenient for a comparison to reactive synthesis. Technically, we refer to a branch of supervisory control theory proposed by Ramadge (1989a) and Thistle and Wonham (1994a) which explicitly accounts for non-terminating processes and therefore utilises ω-languages as the base model. For illustration purposes, we again give an algorithmic solution of the synthesis problem for the specific case of deterministic Büchi automata realisations of the involved ω-languages.

4.1 Supervisors

A supervisory controller is a device that takes as input a finite sequence of events from an alphabet Σ generated by a process which is commonly referred to as the plant and, in turn, outputs a control pattern\(\gamma \subseteq {\Sigma }\). Formally, the supervisor is defined as a map

where \({\Sigma }_{\text {uc}}\subseteq {\Sigma }\) are so called uncontrollable events. On start-up, the supervisor applies the control pattern γ = f(𝜖) and thereby restricts the plant to generate an event σ ∈ γ. After the plant has generated its event, the control pattern is updated accordingly, and so forth. In this process, the role of the uncontrollable events Σ_uc is that, by the definition of Γ, their occurrence cannot be prevented by the supervisor.

For the subsequent discussion, the following representation of a supervisor as an ω-language turns out convenient: ^{Footnote 6}

The language defined by Eq. 14 is referred to as the behaviour associated with the supervisor f. The following lemma characterises languages that match the behaviour of some supervisor.

Lemma 2

Let Σ and\(\emptyset \neq {\Sigma }_{\text {uc}}\subseteq {\Sigma }\). Then the behaviour\({\mathcal{L}}\subseteq {\Sigma }^{\omega }\)in Eq. 14associated with\(f: {\Sigma }^{*} \rightarrow {\Gamma }\)is non-empty and exhibits the following properties:

• (SC1)\({\mathcal{L}}\)is topologically closed, and

• (SC2)\({\mathcal{L}}\)is universally controllable, i.e., \(({\textup {pfx}}\ {\mathcal{L}}) {\Sigma }_{\text {uc}} \subseteq {\textup {pfx}}\ {\mathcal{L}}\).

Vice versa, if\(\emptyset \neq {\mathcal{L}}\subseteq {\Sigma }^{\omega }\)satisfies (SC1) and (SC2), then\(f^{\prime }:{\Sigma }^{*}\rightarrow {\Gamma }\)defined by

for any s ∈Σ^∗is a supervisor with associated behaviour\({\mathcal{L}}\).

4.2 Problem statement (SCT)

The problem commonly referred to as supervisory controller synthesis is about the systematic design of a supervisor for a given plant, such that the resulting closed-loop system – established by the feedback composition of this supervisor with the plant – satisfies a given specification. When the supervisor and plant behaviours are given as the ω-languages \({{\mathcal{L}}}\subseteq {\Sigma }^{\omega }\) and \({\mathcal {A}}\subseteq {\Sigma }^{\omega }\), respectively, their closed-loop configuration evolves on words that comply with both component behaviours. Technically, we distinguish the local closed-loop behaviour\(K_{\text {loc}}:=({\textup {pfx}}\ {\mathcal{L}}) \cap ({\textup {pfx}}\ {\mathcal {A}})\) and the accepted closed-loop behaviour\(\mathcal {K}:={\mathcal{L}}\cap \mathcal {A}\) and require that the latter meets an upper-bound specification \(\mathcal {K}\subseteq \mathcal {G}\).

Regarding liveness of the closed-loop configuration, supervisory control commonly addresses not only deadlocks but also livelocks. The latter are characterised by finite sequences s ∈ K_loc from the local closed-loop behaviour that can be continued indefinitely within K_loc but any such infinite extension fails to satisfy the plant acceptance condition. To rule out such sequences, the synthesis problem asks for a non-blocking supervisor, i.e., it is required that \({\mathcal{L}}\) and \({\mathcal {A}}\) are non-conflicting:

As the local behaviour K_loc of a non-conflicting closed loop can be recovered by \(K_{\text {loc}}={\textup {pfx}}\ \mathcal {K}\), one refers to \(\mathcal {K}\) concisely as the closed-loop behaviour.

In the absence of an acceptance condition of the plant, i.e., when \(\mathcal {A}\) is topologically closed, livelocks are not an issue and, hence, non-conflictingness, Eq. 16, is equivalent to the absence of deadlocks, Eq. 4.

The interpretation of the case when \(\mathcal {A}\) is not topologically closed is more involved. Here, Eq. 16 guarantees that at any instance of time, the plant under supervision can achieve its acceptance condition on at least one infinite extension of the string generated so far. Thus, at some stage the plant must actually choose a path that not only attains a marked state but also complies with the restrictions subsequently imposed by the supervisor. In general, this should be interpreted as a form of cooperation. We will come back to this point in Section 5.3.

We summarize the above discussion in the following formal statement of the supervisor synthesis problem for non-terminating processes.

Problem 2 (Supervisory Controller Synthesis)

Given an alphabet Σ with uncontrollable event set\(\emptyset \neq {\Sigma }_{\text {uc}}\subseteq {\Sigma }\), a plant\(\mathcal {A}\subseteq {\Sigma }^{\omega }\) and an upper-bound specification\(\mathcal {G}\subseteq {\Sigma }^{\omega }\), the supervisory control problemSCT[Σ,Σ_uc, \(\mathcal {A}, \mathcal {G}]\) asks to either construct a non-blocking supervisor with associated behaviour \({\mathcal{L}}\subseteq {\Sigma }^{\omega }\), see Eq. 16, such that

or, to verify that no such supervisor exists^{Footnote 7}.

Referring to the behavioural characterisation of supervisors, Lemma 2, we identify a qualifying associated behaviour \({\mathcal{L}}\) as a solution to the supervisory control problem. As in the setting of reactive synthesis, Section 3.2, we can, without loss of generality, restrict our discussion to the case of \(\emptyset \neq \mathcal {G}\subseteq \mathcal {A}\).

Remark 5

As with reactive synthesis, we may alternatively represent the plant behaviour by two distinct languages \({A_{\text {loc}}}\subseteq {\Sigma }^{*}\) and \({\mathcal {A}}\subseteq {\Sigma }^{\omega }\), where A_loc is prefix-closed and represents the local behaviour. In this regard, Ramadge (1989a) and Thistle and Wonham (1994a) specifically address the case \({\textup {pfx}}\ {\mathcal {A}}\subsetneq {A_{\text {loc}}}\) of a blocking plant and the supervisors task is to avoid livelocks and deadlocks in the closed loop. Since non-conflictingness is addressed by our formal problem statement, we can introduce a distinguished uncontrollable event ‡∉Σ to make plant conflicts explicit; i.e., we substitute A_loc by \({A_{\text {loc}}} \cup (({A_{\text {loc}}} - {\textup {pfx}}\ {\mathcal {A}})\dagger ^{*})\) and \({\mathcal {A}}\) by \({\mathcal {A}} \cup (({A_{\text {loc}}} - {\textup {pfx}}\ {\mathcal {A}})\dagger ^{\omega })\), to formally obtain \(A_{\textup {loc}}={\textup {pfx}}\ {\mathcal {A}}\). Using the original guarantee \({\mathcal {G}}\), the supervisor then must circumvent conflicts by implicitly avoiding the generation of the uncontrollable event ‡∉Σ. Using this pre-processing stage, our formal problem statement with \(A_{\textup {loc}}={\textup {pfx}}\ {\mathcal {A}}\) is not restrictive.

4.3 Algorithmic solution

Given a plant, the common approach to solve Problem 2 is via a characterisation of all closed-loop behaviours that can be achieved by non-blocking supervisory control^{Footnote 8}.

The following proposition from Ramadge (1989a) characterises this set.

Proposition 1

Given an alphabet Σ with uncontrollable events\({\Sigma }_{\text {uc}}\subseteq {\Sigma }\), consider two languages\(\mathcal {A}\)and\(\mathcal {K}\)with\(\emptyset \neq \mathcal {K}\subseteq \mathcal {A}\subseteq {\Sigma }^{\omega }\). Then there exists a non-blocking supervisor\(f:{\Sigma }^{*}\rightarrow {\Gamma }\)for the plant\(\mathcal {A}\)with closed-loop behaviour\(\mathcal {K}\)if and only if

• (i) \(\mathcal {K}\)is relatively topologically closed w.r.t. HCode\(\mathcal {A}\), i.e., \(\mathcal {K}= clo(\mathcal {K})\cap \mathcal {A}\), and

• (ii) \(\mathcal {K}\)is ∗-controllablew.r.t. HCode\(\mathcal {A}\), i.e., \((({\textup {pfx}}\ \mathcal {K}){\Sigma }_{\text {uc}}) \cap ({\textup {pfx}}\ \mathcal {A}) \subseteq ({\textup {pfx}}\ \mathcal {K})\).

Given a closed-loop behaviour\(\mathcal {K}\)that satisfies conditions (i) and (ii), a corresponding supervisor fcan be extracted by

for all s ∈Σ^∗.

Proposition 1 reduces Problem 2 to the synthesis of a closed-loop behaviour \(\emptyset \neq \mathcal {K} \subseteq \mathcal {A} \cap \mathcal {G}\) satisfying (i) and (ii). Such a closed-loop behaviour exists, if and only if

is non-empty. Moreover, if \(\mathcal {K}^{\uparrow }\) itself exhibits conditions (i) and (ii) then \(\mathcal {K}^{\uparrow }\) is referred to as the supremal closed-loop behaviour and the so called maximally permissive supervisor to solve the synthesis problem can be extracted from \(\mathcal {K}^{\uparrow }\) via (18). However, the union in Eq. 19 in general fails to preserve topological closedness and hence, a maximally permissive solution does not exist in general. This contrasts SCT for ∗-languages but conforms with the situation for reactive synthesis, where maximally permissive strategies do not exist in general.

Remark 6

Condition (i) in Proposition 1 is specific for the supervision of ω-languages, whereas condition (ii) is literally identical to the original notion of controllability introduced by Ramadge and Wonham (1987) for the more common setting where both \({\mathcal {A}}\) and \(\mathcal {G}\) are ∗-languages. In that setting, all relevant closed-loop properties are preserved under arbitrary union and a supremal closed-loop behaviour uniquely exists. For ω-languages, it is only under the additional assumption that \(\mathcal {A} \cap \mathcal {G}\) itself is relatively topologically closed w.r.t. HCode \(\mathcal {A}\), that \(\mathcal {K}^{\uparrow }\) qualifies for an achievable closed-loop behaviour; see Ramadge (1989a). In this case, \(\mathcal {K}^{\uparrow }\) can be computed by the common synthesis algorithm for ∗-languages from Ramadge and Wonham (1987) with appropriately chosen parameters \(A\subseteq {\Sigma }^{*}\) and \(G\subseteq {\Sigma }^{*}\) and with a minor variation to address deadlocks; see also the appendix of Moor et al. (2012). The relation between supervisory control of ∗-languages and reactive synthesis is discussed in detail by Ehlers et al. (2017), focusing on the supremal closed-loop behaviour and a corresponding maximally permissive supervisor.

To compute some \(\mathcal {K}\subseteq \mathcal {A} \cap \mathcal {G}\) which solves Problem 2, Thistle and Wonham (1994a) introduce the following notion of the controllability prefix, which characterises the set of states from which the synthesis problem has a solution.

Definition 2

Given an alphabet Σ with uncontrollable events \({\Sigma }_{\text {uc}}\subseteq {\Sigma }\) and a plant \(\mathcal {A}\subseteq {\Sigma }^{\omega }\), consider the upper bound specification \(\mathcal {G}\subseteq {\Sigma }^{\omega }\). The controllability prefix of \(\mathcal {G}\)w.r.t. HCode \(\mathcal {A}\) is denoted^{Footnote 9}\({\text {cfx}_{\mathcal {A}}}\mathcal {G}\) and defined as the set of strings \(s\in {\textup {pfx}}\ \mathcal {G}\), for which there exists \(\emptyset \neq \mathcal {V}\subseteq \mathcal {A} \cap \mathcal {G}\cap (s{\Sigma }^{\omega })\) such that \(\mathcal {V}\) is

• (i) rel. topologically closed w.r.t. HCode \(\mathcal {A}\cap (s{\Sigma }^{\omega })\), i.e., \({\mathcal {V}}= clo({\mathcal {V}})\cap (\mathcal {A}\cap (s{\Sigma }^{\omega }))\), and

• (ii) ∗-controllable w.r.t. HCode \(\mathcal {A}\cap (s{\Sigma }^{\omega })\), i.e., \((({\textup {pfx}}\ \mathcal {V}){\Sigma }_{\text {uc}})\cap ({\textup {pfx}}\ \mathcal {A})\cap (s{\Sigma }^{*}) \subseteq {\textup {pfx}}\ \mathcal {V}\).

Comparing (i) and (ii) in Definition 2 with their analogue in Proposition 1, we see that \(\mathcal {V}\) is a closed-loop behaviour that can be enforced by a non-blocking supervisor that “takes over to control the plant” after the string s in the controllability prefix \(\textup {fx}_{\mathcal {A}}\mathcal {G}\) was generated by the plant. As \(\mathcal {V}\subseteq \mathcal {G}\), this supervisor is able to enforce the guarantee \(\mathcal {G}\).

It is shown in Thistle and Wonham (1994a) that \(\epsilon \in {\text {cfx}_{\mathcal {A}}}\mathcal {G}\) if and only if \(\mathcal {K}^{\uparrow }\neq \emptyset \), i.e., if and only if Problem 2 has a solution.

For ω-regular parameters, the controllability prefix can be represented in terms of a fixed-point over an automaton representation of the involved languages; see Thistle and Wonham (1994a). For a concise representation of this construction, we assume again that both \({\mathcal {G}}\) and \({\mathcal {A}}\) are realisable as deterministic Büchi automata. We further assume without loss of generality that \(\emptyset \neq \mathcal {G}\subseteq \mathcal {A}\). Given this setting, we consider a generalised Büchi automaton ^{Footnote 10}

s.t. HCode \({\mathcal {A}}=\mathrm {L}^{\omega }_{\mathrm {m}}({M_{{\mathcal {A}}}}), {\mathcal {G}}=\mathrm {L}^{\omega }_{\mathrm {m}}({M_{{\mathcal {G}}}})\) and \({\textup {pfx}}({\mathcal {A}})=\mathrm {L}^{*}({M})\) where \({M_{{\mathcal {A}}}}\) and \({M_{{\mathcal {G}}}}\) refer to the deterministic Büchi automata obtained from M by using the single accepted state set \({F_{\mathcal {A}}}\) and \({F_{\mathcal {G}}}\), respectively. We call M a representation of \(\mathcal {A}\) and \(\mathcal {G}\).

Given the generalised deterministic Büchi automaton M, a string \(s\in {\text {cfx}_{\mathcal {A}}}\mathcal {G}\) corresponds to the state q = δ(q₀, s) reachable by s from q₀ in M, and hence q is called a winning state. Following Thistle and Wonham (1994b) and Moor (2017), the set of all winning states can be computed by the four-nested fix-point

where

denotes the inverse dynamics operator; i.e., Pre(T, D) denotes the set of predecessor states q ∈ Q of the target set \(T\subseteq Q\) which can be controlled such that the successor state violates the domain constraint\(D\subseteq Q\) only in favour of attaining the target set.

Recall that a solution to Problem 2 exists if and only if \(\epsilon \in {\text {cfx}_{\mathcal {A}}}\mathcal {G}\), which amounts to \(q_{0}\in {\mathsf {Win}^{}}({M})\). If this is true, a non-blocking supervisor solving Problem 2 can be derived from iterations of the fixed-point in Eq. 21 as follows. Consider the last iteration of the fixed-point in Eq. 21 resulting in the set \(Z^{\infty }={\mathsf {Win}^{}}({M})\subseteq Q\) of states and assume that the fixed point over Y is reached after k iterations. If Yⁱ is the set obtained after the i-th iteration, we have that \(Z^{\infty }=\bigcup _{i=0}^{k} Y^{i}\) with \(Y^{i}\subseteq Y^{i+1}, Y^{0}=\emptyset \) and \(Y^{k}=Z^{\infty }\). Furthermore, let Xⁱ = Yⁱ denote the fixed-point of the iteration over X resulting in Yⁱ and denote by \({W^{i}_{j}}\) the set obtained in the j th iteration over W performed while computing Xⁱ. Then we have for all 0 ≤ i ≤ k that \(Y^{i}=X^{i}=\bigcup ^{l}_{j=0} {W_{j}^{i}}\) with \({W_{j}^{i}}\subseteq W_{j+1}^{i}, {W_{0}^{i}}=\emptyset \) and \({W_{l}^{i}}=Y^{i}\).

Using these sets, we define a ranking for every state \(q\in Z^{\infty }\) s.t.

initialised with \(Y^{0}:=Z^{\infty }\cap {F_{\mathcal {G}}}\) and \({W_{0}^{i}}=\emptyset \) for all 0 < i ≤ k. We order ranks lexicographically. Based on this ranking function we define a state feedback map \(g:Z^{\infty } \rightarrow {\Gamma }\) s.t. for all \(q\in Z^{\infty }\)

The state feedback map g defines a supervisor \(f:{\Sigma }^{*}\rightarrow {\Gamma }\) in the obvious way, i.e. f(s) = g(q) if \(\delta (q_{0}, s)=q \in Z^{\infty }\) and f(s) = Σ ∈Γ, otherwise. The behaviour \({\mathcal{L}}\) associated with f is defined via (14). The proof that \({\mathcal{L}}\) solves Problem 2 can be obtained as a special case of the construction presented by Thistle and Wonham (1992, 1994b).

Remark 7

The state feedback g, as defined in Eq. 24, will only enable controllable events for transitions that decrease the rank and, hence, achieve progress in terms of attaining a marked state. Regarding the acceptance condition, however, it is sufficient to attain markings eventually. A more permissive feedback is obtained by initially controlling the local closed-loop K_loc to be a subset of \(\textup {fx}_{\mathcal {A}}\mathcal {G}\) and only eventually to activate the supervisor constructed above. The original literature (Thistle and Wonham 1994a) addresses permissiveness by explicitly considering a lower-bound specification \(\mathcal {E}, \emptyset \neq \mathcal {E}\subseteq \mathcal {G}\). Under the condition that \(\mathcal {E}\) is relatively topologically-closed w.r.t. HCode \(\mathcal {A}\) and that \(\mathcal {E}\subseteq \mathcal {K}^{\uparrow }\), a supervisor can be constructed such that the closed-loop behaviour \(\mathcal {K}\) satisfies \(\mathcal {E}\subseteq \mathcal {K}\subseteq \mathcal {G}\). Thus, the additional problem parameter \(\mathcal {E}\) can be used to tune permissiveness of the supervisor. As mentioned in Remark 6, if \(\mathcal {G}\cap \mathcal {A}\) is relatively topologically-closed w.r.t. HCode \(\mathcal {A}\) then so is \(\mathcal {K}^{\uparrow }\). In this case, one can choose \(\mathcal {E}=\mathcal {K}^{\uparrow }\) and the supervisor constructed by Thistle and Wonham (1994a) essentially matches the one that can be obtained by synthesis procedures from ∗-languages.

Remark 8

Following the discussion in Remark 4, we consider the case where \({\mathcal {A}}\) is topologically closed. Again, this implies that we can assume without loss of generality that \({F_{\mathcal {A}}}=Q\) in M. In this case the fixed-point in Eq. 21 collapses to

where we use the short form Pre(T) := Pre(T, ∅).

We see that Eqs. 12 and 25 are describing the same fixed-point, and this suggests a strong connection between reactive synthesis and supervisory control for the special case of a topologically closed language \(\mathcal {A}\), which is verified in Section 5.

Example 3

Consider the automaton M depicted in Fig. 2 and two sets of problem parameters: (A) \({F_{\mathcal {A}}}={F_{\mathcal {G}}}=\{s\}, {\Sigma }_{\text {uc}}={\Sigma }\setminus \{b\}\), and (B) \({F_{\mathcal {A}}}=\{r,s\}, {F_{\mathcal {G}}}=\{s\}, {\Sigma }_{\text {uc}}={\Sigma }\setminus \{b\}\). In both cases the computation of Eq. 21 yields Win(M) = Q and rank(s) = (0,0), rank(q) = (1,1), and rank(r) = rank(p) = (1,2). Hence, the resulting supervisor disables b in q. However, given the corresponding problem instance we see, that in case (B) disabling b in q is strictly necessary, while this is not true for (A). In fact, as \({\mathcal {G}}\) and \({\mathcal {A}}\) coincide for case (A) there exists a maximally permissive supervisor (see the discussion in Remark 6) which enables both b and d in s. This also constitutes a solution to the given supervisory control problem, as we assume that the plant only generates runs which correspond to words in \({\mathcal {A}}\). By this we know that it will always eventually transition from q to s, implying that the resulting closed loop behaviour fulfils the guarantee.

Transition structure of automaton M in Eq. 20 representing \({\mathcal {A}}\) and \({\mathcal {G}}\) for the instance of Problem 2 which is solved in Example 3

Full size image

Considering a third case (C) with problem parameters \({F_{\mathcal {A}}}=\{r,s\}, {F_{\mathcal {G}}}=\{s\}, {\Sigma }_{\text {uc}}={\Sigma }\) the fixed-point computation amounts to Win(M) = ∅, hence, the corresponding supervisory control problem has no solution. This is due to the fact that the controller cannot prevent the plant from alternating between r and q (as b ∈Σ_uc) and by this generating an accepting run on \({M_{{\mathcal {A}}}}\) which is not in \({\mathcal {G}}\).

This section provides a comparison between the reactive synthesis problem, Problem 1, as introduced in Section 3, and the supervisory control problem, Problem 2, as introduced in Section 4. For both problems, the system that one seeks to synthesise can be interpreted as a causal feedback which is meant to be operated in interaction with its respective environment. However, the problems differ in the interpretation of how the system and the environment interact. For reactive synthesis, the system operates in computation cycles with reading inputs and assigning outputs once per cycle. Thus, the system is driven by some mechanism that triggers the cycle and the input readings. In turn, the system drives its environment by output assignments. This contrasts the common interpretation in supervisory control, where the system passively observes past events to apply a control pattern, while the environment is responsible for the actual execution of transitions. However, these interpretations of the interaction do not show up explicitly either in the formal problem statement or in the synthesis algorithms. Thus, we may very well consider a reactive system where computation cycles are triggered by the environment and we may also consider supervisors that effectively apply singleton control patterns to actively execute plant transitions. Thus, regarding causality, the different interpretations of system interaction are irrelevant at this stage. Using this insight, we demonstrate how one can formally transform the two synthesis problems and their solutions into each other.

In Section 5.1, we transform the parameters of a reactive synthesis problem such that they constitute a supervisory control problem and we show how any solution of the latter problem can be transformed back to obtain a solution to the initial reactive synthesis problem. Furthermore, this solution results in a reactive module whose associated behaviour does not conflict with \(\mathcal {A}\), i.e., the computed module does not falsify the assumptions. While this is formalised on the language level, we show though examples how this practically results in the algorithmic solution of a reactive synthesis problem via the four-nested fixed-point from supervisory control, s.t. the latter property is ensured.

The converse transformation, i.e., to solve a supervisory control problem by reactive synthesis, requires additional assumptions to ensure that the resulting supervisor is non-conflicting. Section 5.2 first discusses a general transformation which ensures the latter property if the plant behaviour \({\mathcal {A}}\) is topologically closed. This transformation is then simplified for the special case of plant behaviours with alternating controllable and uncontrollable events. Section 5.3 finally shows, that for the latter problem class a weaker condition, namely strongly non-anticipation, exists, which ensures that the suggested transformation results in a supervisor which is non-conflicting. Again, all transformations are formalised on the language level and we show the resulting algorithmic solution procedures through examples.

5.1 Reactive synthesis via supervisory control

In this section, we show how a reactive synthesis problem can be solved using supervisory controller synthesis.

This is done in two steps. Given a particular instance of the reactive synthesis problem we (i) derive a corresponding supervisory control problem which we solve as outlined in Section 4.3, and (ii) convert the solution to a reactive module that solves the original reactive synthesis problem.

Step (i)

Given the reactive synthesis problem RS[U, Y, \(\mathcal {A}, \mathcal {G}]\), we are provided the non-empty and disjoint finite sets U and Y and two ω-languages \(\mathcal {A}, {\mathcal {G}}\subseteq (UY)^{\omega }\). To construct a corresponding supervisory control problem, a natural choice is to associate the assumption \(\mathcal {A}\) with the plant and the guarantee \(\mathcal {G}\) with the specification. This implies \({\Sigma }=U \dot {\cup } Y\) and our remaining choice is that of Σ_uc. We let Σ_uc = U and, hence, Y = Σ −Σ_uc, which will be justified below. Having set all parameters, we obtain the supervisory control problem \(\mathsf {SCT}[{\Sigma }, {\Sigma }_{\text {uc}}, \mathcal {A}, \mathcal {G}]\). To this end, we assume that \(\mathsf {SCT}[{\Sigma }, {\Sigma }_{\text {uc}}, \mathcal {A}, \mathcal {G}]\) exhibits a solution \(f:{\Sigma }^{*}\rightarrow {\Gamma }\) with associated behaviour \({\mathcal{L}}\).

Step (ii)

As our first observation, we recall from Lemma 2 that the behaviour \({{\mathcal{L}}}\) is topologically closed (SC1) and universally controllable (SC2). In contrast, reactive modules are characterised by (RM1) – (RM3) in Lemma 1, where topological closedness (RM1) matches (SC1) and the locally free input (RM2) is implied by universal controllability (SC2) and Y = Σ −Σ_uc. Thus, to transform \({\mathcal{L}}\) to qualify as the behaviour of a reactive module, we are left to address that the output locally processes the input (RM3).

At a first stage, we trim f to only enable those controllable events that can actually occur, i.e., we consider \(h:{\Sigma }^{*}\rightarrow {\Gamma }\) with

for all s ∈Σ^∗. This is not expected to affect the closed-loop behaviour and, indeed, the supervisor f constructed in Section 4.3 already possesses this property. At a second stage, we ensure that at any instance of time exactly one controllable event is enabled, i.e., we consider \(f^{\prime }:{\Sigma }^{*}\rightarrow {\Gamma }\) that satisfies

for all s ∈Σ^∗.

As an example, \(f^{\prime }\) can be constructed as a composition \(f^{\prime }=h^{\prime }\circ h\) where \(h^{\prime }:{\Gamma }\rightarrow {\Gamma }\) is a static filter such that

for all γ ∈Γ.

Although this second post-processing stage at instances enables an arbitrarily chosen additional controllable event, it does so only when the plant at hand will not accept any controllable event at all. Thus, the second post-processing stage is expected to restrict the closed-loop behaviour. Technically, \(f^{\prime }\) is a supervisor and, by Lemma 2, the associated behaviour \({\mathcal{L}}^{\prime }\) is non-empty and exhibits (SC1) and (SC2). Referring to the second post-processing stage, we obtain the following additional properties:

in support of (RM3).

In a third post-processing step, we intersect \({\mathcal{L}}^{\prime }\) with (UY )^ω in order to enforce alternating inputs and outputs, i.e.,

Although the latter construct will formally invalidate (SC2), it retains (RM2) and it does not affect the closed-loop configuration \(\mathcal {A}\cap {\mathcal{L}}^{\prime }\) since we have \(\mathcal {A}\subseteq (UY)^{\omega }\).

Result

We can now state our first main result, i.e., \({\mathcal{L}}^{\prime \prime }\) indeed solves the reactive synthesis problem RS[U, Y, \(\mathcal {A}, \mathcal {G}]\). A proof is given in Appendix B.

Theorem 1

Given non-empty alphabets U, Y, U ∩ Y = ∅, the assumption\(\mathcal {A}\subseteq (UY)^{\omega }\), and the guarantee\(\mathcal {G}\subseteq (UY)^{\omega }\), consider the reactive synthesis problemRS[U, Y, \(\mathcal {A}, \mathcal {G}]\). Let\({\Sigma }:=U \dot {\cup } Y\)and Σ_uc := U. If a supervisor\(f:{\Sigma }^{*}\rightarrow {\Gamma }\)with associated behaviour\({\mathcal{L}}\)solves the supervisory control problem\(\mathsf {SCT}[{\Sigma }, {\Sigma }_{\text {uc}}, \mathcal {A}, \mathcal {G}]\), then\({\mathcal{L}}^{\prime \prime }\), as defined by Eqs. 26, 27and 31, solvesRS[U, Y, \(\mathcal {A}, \mathcal {G}]\). If \({{\mathcal{L}}}\)isω-regular, then\(f^{\prime }\)can be chosen to be realisable by a finite automaton, and, in turn, \({\mathcal{L}}^{\prime \prime }\)is ω-regular.

By Theorem 1, for any reactive synthesis problem for which the corresponding supervisory control problem exhibits a solution, we can use this solution to construct a reactive module that solves the original reactive synthesis problem. For practical purposes, we therefore achieve the solution of an RS problem via SCT by using the synthesis algorithm from supervisory control, Section 4.3, and the additional post-processing given by Eqs. 26-31, as demonstrated by Example 4. However, since the requirement of non-conflictingness in the context of SCT is stronger than the requirement of the absence of deadlocks in the context of RS, we may encounter the situation of a solvable RS problem, for which the corresponding SCT problem exhibits no solution at all; see the following remark for more detail.

Remark 9

Although \(\mathcal {A}\) and \({\mathcal{L}}\) in Theorem 1 are non-conflicting by hypothesis, this property is in general not preserved by the proposed transformation, i.e., \(\mathcal {A}\) and \({\mathcal{L}}^{\prime \prime }\) may fail to be non-conflicting. However, if all problem parameters are ω-regular and if a realisation of \({\mathcal{L}}\) is obtained by the synthesis algorithm presented in Section 4.3, the situation becomes more favourable. Here, the transformations in Eqs. 26–31 effectively restrict the state feedback \(g\colon Q\rightarrow {\Gamma }\) given in Eq. 24 to enable exactly one controllable event in each state q ∈ Q in which the plant can execute a controllable event at all. This restriction preserves the fact that controllable events are only enabled if the respective transition decreases the state rank or if the state rank in the current state is (0,0). Non-conflictingness of \(\mathcal {A}\) and \({\mathcal{L}}^{\prime \prime }\) then follows exactly by the same arguments as for \(\mathcal {A}\) and \({\mathcal{L}}\) provided by the original literature (Thistle and Wonham 1992, 1994b). In particular, the resulting reactive module does not falsify the assumptions; see also Example 4. This insight is also used by Majumdar et al. (2019) where a non-conflicting reactive module is directly constructed by a four-nested fixed-point algorithm over a two-player game graph which is inspired by the one in Eq. 21. Majumdar et al. (2019) further give a self-contained proof of the desired non-conflictingness result in the framework of two-player games which is slightly different from the language-based setting of Theorem 1.

Example 4

Consider the reactive synthesis problem RS[U, Y, \(\mathcal {A}, \mathcal {G}]\) discussed in Example 2, which is solved using the automaton M depicted in Fig. 1. To solve the corresponding supervisory control problem \(\mathsf {SCT}[{\Sigma }, {\Sigma }_{\text {uc}}, \mathcal {A}, \mathcal {G}]\) instead, an automaton \(\check {{M}}\) conforming with Eq. 20 which corresponds to \(\mathsf {SCT}[{\Sigma }, {\Sigma }_{\text {uc}}, \mathcal {A}, \mathcal {G}]\) is needed. The only structural difference between M and \(\check {{M}}\) is that the former distinguishes environment and system states, while the latter distinguishes controllable (ticked) and uncontrollable transitions. However, due to the alternation of Σ_uc = U and Σ_c = Y in \({\mathcal {A}}\) and \({\mathcal {G}}\), these changes are only cosmetic. For convenience, we depicted \(\check {{M}}\) corresponding to \(\mathsf {SCT}[{\Sigma }, {\Sigma }_{\text {uc}}, \mathcal {A}, \mathcal {G}]\) in Fig. 3.

Automaton \(\check {{M}}\) representing \(\protect \mathsf {SCT}[{\Sigma }, {\Sigma }_{\text {uc}},\mathcal {A}, \mathcal {G}]\) in Example 4 which corresponds to \(\protect \mathsf {RS}[U, Y,\mathcal {A}, \mathcal {G}]\) represented by M in Fig. 1. Final states are \({F_{\mathcal {A}}}=\{q_{4}\}\) (blue) and \({F_{\mathcal {G}}}=\{q_{5}\}\) (red) and transitions labelled by controllable events Σ −Σ_uc are indicated by a tick

Full size image

Using Eq. 21 to solve SCT[Σ,Σ_uc, \(\mathcal {A}, \mathcal {G}]\) over \(\check {{M}}\) results in \({\mathsf {Win}^{}}(\check {{M}})=Q\) with rank(q₃) = (1,2), rank(q₄) = (1,1), rank(q₆) = (2,2). Defining a supervisor based on this ranking and extracting a reactive module via Eqs. 26-31 results in a system strategy which always transitions from q₃ to q₄. Comparing this solution to the one obtained in Example 2, we see that the four-nested fixed point in Eq. 21 allows to distinguish between transitioning from q₃ to q₄ or to q₆ and, as a consequence, chooses the former to not falsify the assumptions. This clearly constitutes a more desirable solution to problem RS[U, Y, \(\mathcal {A}, \mathcal {G}]\).

Interestingly, \({\mathcal {G}}\) is relatively topologically closed w.r.t \({\mathcal {A}}\), and we can therefore also compute a maximally permissive supervisor (see Remark 6). This supervisor enables every available transition in every state and therefore leaves the choice to the plant whether it transitions to q₄ or q₆ in q₃. As we assume that the plant only generates runs which correspond to words in \({\mathcal {A}}\), it will always eventually transition from q₃ to q₄, implying that the resulting closed loop fulfils the guarantee.

5.2 Supervisory control via reactive synthesis

We now consider a supervisory control problem and aim for a solution via reactive synthesis. Within this section, we discuss two different possible transformations and show that in both cases the resulting supervisor is non-conflicting if the plant behaviour \({\mathcal {A}}\) is topologically closed.

5.2.1 Control-patterns as system outputs

In this section, we match the ranges of the respective feedback maps without imposing any a-priori assumptions on the problem parameters. In this sense, our approach here is rather general. However, to obtain a qualifying supervisor, we will need to impose relevant restrictions in retrospect. Similar to Section 5.1, our approach is organised in two steps. Given a supervisory control problem, we (i) derive a corresponding reactive synthesis problem which we solve as outlined in Section 3.3, and (ii) convert the solution to a supervisor that solves the original supervisory control problem.

Step (i)

Given a supervisory control problem SCT[Σ,Σ_uc, \(\mathcal {A}, \mathcal {G}]\), we are provided an alphabet Σ, a set of uncontrollable events \({\Sigma }_{\text {uc}}\subseteq {\Sigma }\), a plant behaviour \(\mathcal {A}\subseteq {\Sigma }^{\omega }\) and an upper-bound specification \(\mathcal {G}\subseteq {\Sigma }^{\omega }\) on the closed-loop behaviour. As before, we associate the supervisory controller with the reactive module, i.e., the system to be designed. In order to define the input range U and the output range Y, recall from Section 4.1 that a supervisor is a map \(f: {\Sigma }^{*} \rightarrow {\Gamma }\) that applies a control pattern γ = f(s) after the system has generated the sequence s ∈Σ^∗. The system in turn generates the next event σ ∈Γ, and so forth. Therefore, a nearby choice of U and Y is given by Σ and Γ, respectively.

The interaction of the supervisor and the plant always starts with the former applying a control pattern γ = f(𝜖), i.e., the system to be designed has the first move. In contrast, in our description of reactive synthesis, any run begins with a move by the environment. We therefore introduce a distinguished dummy event 0∉Σ which will pass on the first move to the system to be designed; i.e.,

and define \(U:={\Sigma }^{\prime }\) and \(Y:={\Gamma }^{\prime }\).

With this choice, a reactive synthesis problem refers to ω-languages that are subsets of \((UY)^{\omega }=({\Sigma }^{\prime }{\Gamma }^{\prime })^{\omega }\) and we need to transform our problem parameters \(\mathcal {A}, \mathcal {G}\subseteq {\Sigma }^{\omega }\) accordingly. We begin with the specification \(\mathcal {G}\) by pre-pending the distinguished event \(0\in {\Sigma }^{\prime }\) and by interleaving any control-patterns between each two events from Σ to obtain

The plant \(\mathcal {A}\) is transformed similarly, while ensuring that once a control pattern \(\gamma \in {\Gamma }^{\prime }\) has been applied, the next event σ ∈Σ will be within γ. We obtain

This results in the reactive synthesis problem RS[U, Y, \({\mathcal {A}}^{\prime }, {\mathcal {G}}^{\prime }]\). To this end, we assume that RS[U, Y, \({\mathcal {A}}^{\prime }, {\mathcal {G}}^{\prime }]\) exhibits a solution \(r:U^{+}\rightarrow Y\) with associated behaviour \({\mathcal{L}}^{\prime }\).

Step (ii)

Given \({\mathcal{L}}^{\prime }\) from Step (i), we construct

as a candidate to solve SCT[Σ,Σ_uc, \(\mathcal {A}, \mathcal {G}]\). It is shown in Appendix C, Proposition 4, that \({{\mathcal{L}}}\) indeed satisfies (SC1), (SC2) and we have that \({\mathcal{L}}\subseteq \mathcal {A}\rightarrow \mathcal {G}\), as consequences of (RM1) and (RM2) holding for \({\mathcal{L}}^{\prime }\) and of \({\mathcal{L}}^{\prime }\subseteq \mathcal {A}^{\prime }\rightarrow \mathcal {G}^{\prime }\). In particular, \({\mathcal{L}}\) is the behaviour associated with a supervisor that enforces the upper bound specification \(\mathcal {K}=\mathcal {A} \cap {\mathcal{L}}\subseteq \mathcal {G}\). Furthermore, it is shown in Appendix C, Proposition 5 that \({\textup {pfx}}\ {\mathcal{L}}\) and \({\textup {pfx}} \ {\mathcal {A}}\) do not deadlock.

Referring back to Problem 2, we are left to verify that \(\mathcal {K}\) is non-empty and that \(\mathcal {A}\) and \({\mathcal{L}}\) are non-conflicting, or to give conditions under which this holds.

Result

Whenever \({\mathcal {A}}\) is topologically closed, we know that the absence of deadlocks in the closed loop, Eq. 4, implies non-conflictingness of \(\mathcal {A}\) and \({\mathcal{L}}\), Eq. 16. Hence we can use topologically closedness as a sufficient condition to conclude that the supervisor with associated behaviour \({\mathcal{L}}\) given in Eq. 35 solves \(\mathsf {SCT}[{\Sigma }, {\Sigma }_{\text {uc}}, \mathcal {A}, \mathcal {G}]\).

Theorem 2

Given a finite alphabet Σ with the non-empty set of uncontrollable events\({\Sigma }_{\text {uc}}\subseteq {\Sigma }\), a plant\(\mathcal {A}\subseteq {\Sigma }^{\omega }\)and a specification\(\mathcal {G}\subseteq {\Sigma }^{\omega }\), consider the supervisory control problemSCT[Σ,Σ_uc, \(\mathcal {A}, \mathcal {G}]\). Pre-process the parameters according to Eqs. 32-34to obtain\(U={\Sigma }^{\prime }, Y={\Gamma }^{\prime }\)and\(\mathcal {A}^{\prime }, {\mathcal {G}}^{\prime }\subseteq (UY)^{\omega }\). Let\({\mathcal{L}}^{\prime }\)denote a solution to the reactive synthesis problem\(\mathsf {RS}[{U}{Y}{{\mathcal {A}}^{\prime }}{{\mathcal {G}}^{\prime }}]\).

Ifthe plant\(\mathcal {A}\)is topologically closed, then\({\mathcal{L}}\)defined by Eq. 35solvesSCT[Σ,Σ_uc, \(\mathcal {A}, \mathcal {G}]\). If\({\mathcal{L}}^{\prime }\)isω-regular, then so is\({\mathcal{L}}\).

By the above theorem we have the following result. Given an instance of the supervisory control problem with topologically closed plant and assuming that the corresponding reactive synthesis problem has a solution, this solution can be transformed into a non-blocking supervisor solving the initial control problem. Technically, the overall procedure amounts to pre-processing the problem instance by Eqs. 32-34, using the reactive synthesis procedure discussed in Section 3.3 to compute a reactive module, and post-processing the latter by Eq. 35. This is illustrated by the following example.

Example 5

Consider the supervisory control problem SCT[Σ,Σ_uc, \(\mathcal {A}, \mathcal {G}]\) discussed in Example 3, s.t. M depicted in Fig. 2 represents \({\mathcal {G}}\) and \({\mathcal {A}}\) with \({F_{\mathcal {G}}}=\{s\}\) and \({F_{\mathcal {A}}}=\{s,r\}\). As M cannot generate infinite strings which do not visit either r or s infinitely often, it follows that \({\mathcal {A}}\) is topologically closed. To obtain the corresponding reactive synthesis problem \(\mathsf {RS}[{U}{Y}{{\mathcal {A}}^{\prime }}{{\mathcal {G}}^{\prime }}]\) (as defined in Eqs. 32-34), we manipulate M in Fig. 2 s.t. the resulting automaton \(\check {{M}}\) conforms with Eq. 7 and represents \({\mathcal {A}}^{\prime }\) and \({\mathcal {G}}^{\prime }\).

This results in splitting every state q ∈ Q of M into a system state q¹ and k environment states \({q^{0}_{k}}\) with k ∈{1,…, K} and K being the number of possible control patters available in q. Then the transition from q¹ to \({q^{0}_{k}}\) is labelled with the respective control pattern \(\gamma _{k}\subseteq {\Gamma }\). Outgoing transitions of \({q_{k}^{0}}\) mimic outgoing transitions of q in M, i.e., a transition \((q,\sigma ,q^{\prime })\in \delta \) of M is copied to all \(({q_{k}^{0}},\sigma ,q^{\prime 1})\in \check {\delta }\) of M for which σ ∈ γ_k. Finally, we add a dummy initial state d whose outgoing transition is labelled by the dummy event 0 and which leads to the system part p¹ of M’s initial state p.

Automaton \(\check {{M}}\) representing \(\protect \mathsf {RS}[U, Y, {\mathcal {A}}^{\prime }, {\mathcal {G}}^{\prime }]\) in Example 5, which corresponds to \(\protect \mathsf {SCT}[{\Sigma }, {\Sigma }_{\text {uc}}, \mathcal {A}, \mathcal {G}]\) represented by M in Fig. 2 with Σ_uc = Σ ∖{b} (including \({q^{0}_{2}}\)) and Σ_uc = Σ (excluding \({q^{0}_{2}}\)). The final state sets are T⁰ = {r⁰, s⁰} (blue) and T¹ = {s¹} (red)

Full size image

The resulting automaton \(\check {{M}}\) is depicted in Fig. 4, where all γ-labels are trimmed to the events actually available at its source state. The sets of final states are translated in the obvious way, resulting in T⁰ = {r⁰, s⁰} (blue) and T¹ = {s¹} (red). Depending on the controllability status of event b we get one or two possible control patterns in state q. I.e., if b ∈Σ_uc we obtain the automaton without \({q^{0}_{2}}\), while b ∈Σ∖Σ_uc results in the full automaton containing both \({q^{0}_{1}}\) and \({q^{0}_{2}}\).

We now use \(\check {{M}}\) as the input to the reactive synthesis algorithm in Section 3.3. If Σ_uc = Σ the system has no choice in any of the system states. Therefore, it cannot prevent the environment to always take transition b in q⁰. Hence, the set of winning states is empty which coincides with the solution of case (C) in Example 3. If Σ_uc = Σ ∖{b}, the system has a choice in q¹ and can apply the control pattern {d}, effectively disabling b in q of M in Fig. 2. This coincides with the solution obtained of case (B) in Example 3.

Equivalence of problem statements

Given the results in Theorems 1 and 2, we have established that for topologically closed plants both synthesis problems can be solved via the respective other one. However, our construction assumes that the respective target problem exhibits a solution. Since Theorem 2 uses a non-trivial transformation of the problem parameters \(\mathcal {A}\) and \(\mathcal {G}\), the two theorems alone do not establish equivalence of the two problems regarding solvability. For this purpose, we show in Appendix C, Proposition 6,

that our transformation of SCT[Σ,Σ_uc, \(\mathcal {A}, \mathcal {G}]\) to RS[U, Y, \({\mathcal {A}}^{\prime }, {\mathcal {G}}^{\prime }]\) retains solvability. Additionally referring to Theorem 2, this gives the following corollary.

Corollary 1

Let Σ be a finite alphabet with the non-empty set of uncontrollable events\({\Sigma }_{\text {uc}}\subseteq {\Sigma }, \mathcal {A}\subseteq {\Sigma }^{\omega }\)be a plant, \(\mathcal {G}\subseteq {\Sigma }^{\omega }\)be a upper bound specification and\(U={\Sigma }^{\prime }, Y={\Gamma }^{\prime }, \mathcal {A}^{\prime }\)and\(\mathcal {G}^{\prime }\)be defined by Eqs. 32-34.

If the plant\(\mathcal {A}\)is topologically closed, thenSCT[Σ,Σ_uc, \(\mathcal {A}, \mathcal {G}]\)has a (ω-regular) solution if and only ifRS[U, Y, \({\mathcal {A}}^{\prime }, {\mathcal {G}}^{\prime }]\) has a (ω-regular) solution.

The above corollary relates to the observation in Remark 4 and Remark 8 that the algorithmic solution of both problem statements reduce to the computation of the same 2-nested fixed point if \(\mathcal {A}\) is topologically closed. However, it should be noted, that the input automata to both algorithms differ (compare Figs. 2 and 4 for an example).

5.2.2 Input-output behaviours

The transformation proposed in Section 5.2.1 turned out technically involved because it needed to encode a mechanism to interleave plant symbols with control patterns in a single language. Therefore, we expect considerable simplifications when we restrict the discussion to plant behaviours in which controllable and uncontrollable events alternate. Technically, we now consider a supervisory control problem with parameters \({\Sigma }_{\text {uc}}\subsetneq {\Sigma }\) and \(\mathcal {A},\ \mathcal {G}\subseteq ({\Sigma }_{\text {uc}}({\Sigma } - {\Sigma }_{\text {uc}}))^{\omega }\). As we will match inputs and outputs with uncontrollable and controllable events, respectively, we refer to this class of behaviours as input-output behaviours. We again derive a solution of the given supervisory control problem via reactive synthesis in two steps.

Step (i)

Given a supervisory control problem SCT[Σ,Σ_uc, \(\mathcal {A}, \mathcal {G}]\) with input-output behaviours, we can choose the correspondence U := Σ_uc and Y := Σ −Σ_uc and obtain \(\mathcal {G},\ \mathcal {A}\subseteq (UY)^{\omega }\); i.e., our choice constitutes qualifying parameters for the reactive synthesis problem RS[U, Y, \(\mathcal {A}, \mathcal {G}]\). Let \({{\mathcal{L}}}\) denote a solution of \(\mathsf {RS}[U, Y, \mathcal {A}, \mathcal {G}]\).

Step (ii)

\({{\mathcal{L}}}\) satisfies (RM1)–(RM3) and we need to derive a behaviour that satisfies (SC1) and (SC2). Topological closedness (SC1) is immediate by (RM1). Regarding (SC2), we propose the following transformation:

It is shown in Appendix B, Proposition 7, that the above construct \(\mathcal {L^{\prime }}\) indeed satisfies (SC1) and (SC2) and, moreover, retains the absence of deadlocks, i.e., \({\textup {pfx}}\ {\mathcal{L}}^{\prime }\) and \({\textup {pfx}} \ {\mathcal {A}}\) do not deadlock.

For \(\mathcal {L^{\prime }}\) to solve the control problem, we are left to establish that its corresponding supervisor is non-blocking and that it enforces the language inclusion specification; technically, \(\mathcal {A}\) and \(\mathcal {L^{\prime }}\) must be non-conflicting with \(\emptyset \neq {\mathcal {A}}\cap {\mathcal{L}}^{\prime }\subseteq {\mathcal {G}}\).

Result

Using the same reasoning as in Section 5.2.1, we see that non-conflictingness of \(\mathcal {A}\) and \(\mathcal {L^{\prime }}\) is implied by the absence of deadlocks provided that \({\mathcal {A}}\) is topologically closed. Using this sufficient condition, we get the following result on the synthesis of supervisors for input-output behaviours via reactive synthesis.

Theorem 3

Given a finite alphabet Σ with the non-empty set of uncontrollable events\({\Sigma }_{\text {uc}}\subseteq {\Sigma }\), aninput-output plant behaviour\(\mathcal {A}\subseteq {\Sigma }^{\omega }\)and aninput-output specification behaviour\(\mathcal {G}\subseteq {\Sigma }^{\omega }\), consider the supervisory control problemSCT[Σ,Σ_uc, \(\mathcal {A}, \mathcal {G}]\). Let\({\mathcal{L}}\)denote a solution to the reactive synthesis problemRS[U, Y, \(\mathcal {A}, \mathcal {G}]\), whereU = Σ_uc, Y = Σ −Σ_uc.

Ifthe plant\(\mathcal {A}\)is topologically closed, then\(\mathcal {L^{\prime }}\)defined by Eq. 36solvesSCT[Σ,Σ_uc, \(\mathcal {A}, \mathcal {G}]\). If\({\mathcal{L}}\)isω-regular, then so is\({\mathcal{L}}^{\prime }\).

Given the results in Theorem 1 and Theorem 3, we have established that both synthesis problems can be solved via the respective other one under the assumption of a topologically closed plant. By additionally requiring that \({\mathcal {A}}\) and \({\mathcal {G}}\) are input-output behaviours, neither of the proposed transformations affects the problem parameters \(\mathcal {A}\) and \(\mathcal {G}\). Hence, both problem statements are equivalent w.r.t. solvability, as summarised in the following corollary, complementing Corollary 1.

Corollary 2

Given an alphabet Σ with the non-empty set of uncontrollable events\({\Sigma }_{\text {uc}}\subsetneq {\Sigma }\), letU = Σ_ucand Y = Σ −Σ_uc. For any non-empty topologically closed behaviour\(\mathcal {A}\subseteq (UY)^{\omega }\)and any upper bound\(\mathcal {G}\subseteq (UY)^{\omega }\), the supervisory control problem\(\mathsf {SCT}[{\Sigma }, {\Sigma }_{\text {uc}}, \mathcal {A}, \mathcal {G}]\)has a (ω-regular) solution if and only if the reactive synthesis problemRS[U, Y, \(\mathcal {A}, \mathcal {G}]\)has a (ω-regular) solution.

Theorem 1 and Theorem 3 show that in the special case of input-output behaviours a sound transformation is obtained by simply choosing U = Σ_uc and Y = Σ −Σ_uc and keeping \({\mathcal {A}}\) and \({\mathcal {G}}\) unchanged otherwise.

In this setting, the automaton M defined for reactive synthesis and for supervisory control in Eqs. 7 and 20, respectively, coincide; compare Figs. 1 and 3 for an example. Technically, states with outgoing transitions from U = Σ_uc (resp. Y = Σ −Σ_uc) correspond to environment states (resp. system states). Likewise, outgoing transitions from an environment state (resp. system state) are considered uncontrollable (resp. controllable). Therefore, the unconditioned version Pre(T) = Pre(T, ∅) of the pre-operator defined in Eq. 22 coincides with the controllable pre-operator Pre¹ defined in Eq. 9. Following up Remarks 4 and 8 for topologically closed ω-languages \(\mathcal {A}\), both synthesis algorithms compute the same 2-nested fixed-point, see Eqs. 12 and 25. Hence, for topologically closed input-output behaviours both solution techniques also coincide on the automaton level.

5.3 Non-falsifiable assumptions and strong non-anticipation

By our comparison so far the reactive synthesis problem can be solved via supervisory control. However, the converse transformation in general fails as a non-blocking supervisor by definition requires that \({\mathcal{L}}\) and \({\mathcal {A}}\) are non-conflicting and this requirement cannot be expressed by an upper-bound specification in the reactive synthesis problem under consideration. We have seen in Section 5.2 that topological closeness of \({\mathcal {A}}\) can be used as a sufficient condition to ensure that the solution \({\mathcal{L}}\) obtained via reactive synthesis is such that \({\mathcal{L}}\) does not conflict with \({\mathcal {A}}\).

In this section, we present two alternative weaker conditions for a non-conflicting closed loop which were independently developed in either field, and we discuss how they relate. Technically, both conditions address the situation of input-output behaviours and, in this regard, follow up our discussion in Section 5.2.2.

Non-falsifiable assumptions in reactive synthesis

Consider a reactive synthesis problem RS[U, Y, \(\mathcal {A}, \mathcal {G}]\) with solution \({{\mathcal{L}}}\), which implies that \({{\mathcal{L}}}\) and \({\mathcal {A}}\) do not deadlock. Hence, the closed-loop configuration can continue for infinitely many computation cycles to generate an ω-word \(\alpha \in ({\text {clo}} \mathcal {A}) \cap (\text {clo}{\mathcal{L}})\). Since \({\mathcal{L}}\) is closed, we also have \(\alpha \in {\mathcal{L}}\). However, one may fail on \(\alpha \in \mathcal {A}\), and, by the specification \({\mathcal{L}}\subseteq \mathcal {A} \rightarrow \mathcal {G}\), risk that \(\alpha \not \in \mathcal {G}\) (see e.g. Example 2). Technically, the problem statement of reactive synthesis does not prevent the construction of a reactive module such that there exists \(s\in ({\textup {pfx}}\ \mathcal {A}) \cap ({\textup {pfx}}\ {\mathcal{L}})\) but \(s\not \in {\textup {pfx}}(\mathcal {A} \cap {\mathcal{L}})\).

This implies for all extensions β ∈ (U ∪ Y )^ω with \(s\upbeta \in {\mathcal{L}}\) that \(s\upbeta \not \in \mathcal {A}\). For parameters \(\mathcal {G}\subseteq \mathcal {A}\) we obtain \(s\upbeta \not \in \mathcal {G}\), i.e., after the finitely many computation cycles represented by s it is known that the guarantee will not be satisfied.

This issue can be avoided if the given assumption \({\mathcal {A}}\) is non-falsifiable^{Footnote 11} in the following sense. Given the two player game interpretation used in the algorithmic synthesis of reactive modules (see Section 3.3), an assumption is called non-falsifiable, if the environment player has a winning strategy in the Büchi game (H, T⁰) over the game graph H. In this case, there exists a causal map by which the environment can organise its moves, which ensures that for any infinite play some final environment state q ∈ T⁰ is visited infinitely often, regardless of the moves chosen by the reactive module. In this sense, both players win and we have \(\alpha \in \mathcal {A} \cap {\mathcal{L}}\) for any ω-word generated in the closed-loop configuration.

Strong non-anticipation in supervisory control

A closely related issue has been identified in the context of supervisory control by Moor et al. (2011). Consider a supervisory control problem SCT[Σ,Σ_uc, \(\mathcal {A}, \mathcal {G}]\) with plant \(\mathcal {A}\subseteq {\Sigma }^{\omega }\) and specification \(\mathcal {G}\subseteq \mathcal {A}\), and let \({\mathcal{L}}\subseteq {\Sigma }^{\omega }\) denote a solution. As we ask for a non-blocking supervisor, we know that at no specific instance of time the supervisor can prevent the plant to attain its acceptance condition, i.e., for all s ∈ K_loc we have \(s\in {\textup {pfx}}(\mathcal {A} \cap {\mathcal{L}})\) and there exists β ∈Σ^ω such that \(s\upbeta \in \mathcal {A} \cap {\mathcal{L}}\). However, this does not rule out supervisors which require the plant to eventually take certain transitions that depend on future control patterns, i.e., the plant may need to anticipate the moves of the supervisor.

We illustrate this subtle issue by the following example adapted from Moor et al. (2011).

Example 6

Consider the automaton given in Figure 5 and assume that \({F_{\mathcal {A}}}=\{ \mathsf {AA},\mathsf {BB} \}\) and \({F_{\mathcal {G}}}=\{ \mathsf {AA} \}\). A supervisor solving the synthesis problem may therefore at some stage disable the transition from B to BB for all future. If the plant is not aware of this restriction, it might still organise its moves in the attempt to satisfy its acceptance condition by visiting BB infinitely often, e.g., by always transitioning form 0 to B. This results in an infinite sequence which falsifies the assumptions.

Transition structure of a Büchi-automaton realising a plant behaviour that needs to anticipate future control patterns in order to satisfy its acceptance condition. Accepting states are marked in red and controllable transitions are indicated by a tick

Full size image

To avoid the implicit need for cooperation, there is an interest in plant behaviours that can attain their acceptance conditions independently of the supervisor. A class of such plant behaviours has been characterised by Moor et al. (2011) for the special case of input-output behaviours. The reported results amount to a representation of \(\mathcal {A}\) as a union of topologically closed components that each exhibit Y = Σ −Σ_uc as a locally free input. It is further shown that this condition is equivalent to the controllability prefix of \(\mathcal {A}\) w.r.t. the closure \(\text {clo}\mathcal {A}\) to equal \({\textup {pfx}}\ \mathcal {A}\), i.e.,

where Y = Σ −Σ_uc takes the role the uncontrollable events.

The latter property is referred to as strong non-anticipation. Referring to the game theoretic interpretation of supervisory control used in the discussion of the synthesis algorithm in Section 4.3, Eq. 37 requires that the local plant\({\textup {pfx}}\ \mathcal {A}\) is always in a winning configuration regarding the satisfaction of its own acceptance condition, i.e., at any time the plant can decide to internally apply a causal feedback map to choose the next event such that the plant acceptance condition will be met regardless the control imposed by the supervisor. By strong non-anticipation, a non-conflicting closed loop, Eq. 16, is implied by the absence of deadlocks.

Since non-conflictingness imposes its formal requirements only on words within the local closed loop, \(({\textup {pfx}}\ \mathcal {A}) \cap ({\textup {pfx}}\ {\mathcal{L}})\), we may use the weaker condition

to conclude a non-conflicting closed loop from the absence of deadlocks; see Appendix D, Proposition 9, for a formal proof.

If we synthesise \({{\mathcal{L}}}\) by supervisory control, the closed loop will be non-conflicting by construction. To additionally ensure Eq. 38, we can pre-process the specification s.t.

Comparison

When comparing the game theoretic interpretations of non-falsifiable assumption and strong non-anticipation, the former requires the “environment to play clever” from the very beginning, whereas the latter allows the plant to start doing so eventually. This suggests that whenever an assumption is non-falsifiable we have

\(\epsilon \in \textstyle {{\text {cfx}_{{\text {clo}}\mathcal {A}, Y}}} (\mathcal {A})\), which is indeed always the case if Eq. 37 holds; see Appendix D, Proposition 8, for a formal proof. Hence, the condition of a non-falsifiable assumption is weaker then the condition of a strongly non-anticipating plant behaviour. More precisely, we have that (i) topological closedness of \(\mathcal {A}\) implies (ii) strong non-anticipation, which in turn implies (iii) (38), to finally imply (iv) \({\mathcal {A}}\) to be a non-falsifiable assumption. The converse implications, however, do not hold in general.

Result

Referring to the simple transformation discussed in Section 5.2.2, we consider an instance of the supervisory control problem SCT[Σ,Σ_uc, \(\mathcal {A}, \mathcal {G}]\) where \(\mathcal {A}\) and \({\mathcal {G}}\) are input-output behaviours, and the corresponding reactive synthesis problem \(\mathsf {RS}[U, Y, \mathcal {A}, \mathcal {G}]\), with U = Σ_uc, Y = Σ −Σ_uc. As the condition in Eq. 38 constitutes a closed-loop property, it can be verified after a solution \({{\mathcal{L}}}\) of \(\mathsf {RS}[U, Y, \mathcal {A}, \mathcal {G}]\) is computed. If this test passes, we can conclude that the absence of deadlocks, Eq. 4, implies a non-conflicting closed loop, Eq. 16. With this, we can use Eq. 38 as a sufficient condition to establish a solution of \(\mathsf {SCT}[{\Sigma }, {\Sigma }_{\text {uc}}, \mathcal {A}, \mathcal {G}]\) via \(\mathsf {RS}[U, Y, \mathcal {A}, \mathcal {G}]\) analogously to Theorem 3. Nevertheless, as Eq. 38 is weaker then topological closeness of \({\mathcal {A}}\), we obtain a generalisation of Theorem 3.

Theorem 4

Given the premises of Theorem 3,

\(\mathcal {L^{\prime }}\)defined by Eq. 36solves\(\mathsf {SCT}[{\Sigma }, {\Sigma }_{\text {uc}}, \mathcal {A}, \mathcal {G}]\)if Eq. 38holds. If\({\mathcal{L}}^{\prime }\)is ω-regular, then so is\({\mathcal{L}}\).

Again referring to Theorem 1 from Section 5.1, but now using Theorem 4 rather than Theorem 3, we obtain the following generalisation of Corollary 2.

Corollary 3

Given an alphabet Σ with\(\emptyset \neq {\Sigma }_{\text {uc}}\subsetneq {\Sigma }\), letU = Σ_ucandY = Σ −Σ_uc. For any non-empty behaviours\(\mathcal {A},\ {\mathcal {G}}\subseteq (UY)^{\omega }\)where\({\mathcal {A}}\)is strongly non-anticipating, the control problem\(\mathsf {SCT}[{\Sigma }, {\Sigma }_{\text {uc}}, \mathcal {A}, \mathcal {G}]\)has a (ω-regular) solution if and only if the reactive synthesis problemRS[U, Y, \(\mathcal {A}, \mathcal {G}]\)has a (ω-regular) solution.

Referring back to the discussion below Corollary 2, we still have that the automata realisations of the two corresponding problem instances are effectively identical. As \({\mathcal {A}}\) is not assumed to be topologically closed, we now have to use the three-nested fixed-point algorithm in Eq. 10 to solve the reactive synthesis problem and, in turn, to obtain a solution of supervisory control problem. Note that it is not evident how the four-nested fixed-point for supervisory controller synthesis (21) can be directly converted to a three-nested fixed-point to specifically address strongly non-anticipating plants.

Example 7

Consider the instance of Problem 2 represented by \(\check {{M}}\) depicted in Fig. 3 and the automaton M depicted in Fig. 1 representing the corresponding instance of Problem 1. Recall from Example 2 that a solution of the latter is given by a reactive module which always transitions from from q₃ to q₆. The only possible closed-loop run on M is hence given by the sequence q₀q₁q₂(q₃q₆)^ω, and this run generates an ω-word \(\alpha \in (\text {clo}\mathcal {A}) \cap {\mathcal{L}}\) but \(\alpha \not \in \mathcal {A}\). In particular, we have \({\textup {pfx}}\ \alpha \subseteq ({\textup {pfx}}\ \mathcal {A}) \cap ({\textup {pfx}}\ {\mathcal{L}})\) and, if our condition in Eq. 38 was satisfied, we had that pfx \(\alpha \subseteq \ \text {cfx}_{\text {clo}\mathcal {A}, Y}\mathcal {A}\). Here, the definition of the controllability prefix, Definition 2, requires that there exists a choice of uncontrollable events, by which the plant can enforce to attain its acceptance condition. However, this is not possible given that the choice of controllable events taken by the module only allows for the run q₀q₁q₂(q₃q₆)^ω. Therefore, Eq. 38 is not satisfied for this example. This is as expected, since the given solution to Problem 1 falsifies the assumptions.

We have described a variant of reactive synthesis (RS) with upper-bound language-inclusion specification which explicitly addresses environment assumptions and, thus, is a promising candidate when aiming for a comparison with supervisory control theory (SCT). For SCT, we have presented a variant that uses ω-languages as the base model and, hence, matches this characteristic feature of RS. For both domains we present technical problem statements and we derive behavioural characterisations of reactive modules and supervisors, respectively. This facilitates a technical comparison. In our attempt to transform problem instances from one domain of research to the other, we make the following core observations.

We succeed unconditionally in solving any instance of the considered RS problem by using SCT; see Section 5.1 (Theorem 1). On the practical side, our proposed transformation retains regularity and we may apply the four-nested fixed-point algorithm from SCT to obtain a reactive module. Notably, the obtained reactive module will not actively falsify the assumptions on the environment. This additional property is enforced by the SCT algorithm as it only computes solutions which do not conflict with the environment assumptions. As the latter property cannot be encoded as an ω-regular property, the four-nested fixed-point algorithm cannot result from a straightforward translation of an LTL synthesis problem into a μ-calculus formula over a two-player game. This provides a new perspective on algorithms ensuring solutions which do not falsify the assumptions, which is an active field of research in the RS community.

The reverse transformation does not work out in general. The reason is that the additional property of non-conflicting solutions required by SCT is not guaranteed by solutions to the RS problem. For this reason, we can only solve a synthesis problem from SCT by RS, if we ensure a non-conflicting closed-loop by imposing additional restrictions on the problem parameters. To this end, we identify three cases: topologically closed plants, Theorem 2, topologically closed plants with alternating inputs and outputs, Theorem 3, and strongly non-anticipating plants with alternating inputs and outputs, Theorem 4. The last, in our opinion, is of particular interest since the additional assumption of strong non-anticipation is weaker then topologically closedness and well motivated for hybrid systems or abstractions thereof, see Moor et al. (2011). It is furthermore both conceptionally and technically closely related to non-falsifiable assumptions, a condition developed independently in the RS community. Again, each of the proposed transformations retains regularity of the problem parameters and, hence, can be used to practically synthesise supervisors by algorithms from RS. Hence, for the considered class of plant behaviours we see that a three nested fixed-point computation suffices and may therefore expect computational benefits as a trade-off when imposing additional conditions on the supervisor synthesis problem.

Referring back to the transformation of RS problems via Theorem 1 into synthesis problems in SCT, it is observed that it affects the solutions but not the problem parameters. The same is true for the reverse transformations of input/output behaviours in Theorems 3 and 4. This establishes equivalence of the two problems regarding solvability for respective subclasses of plants as stated in Corollaries 2 and 3. Likewise, we establish by Corollary 1 the equivalence of the transformed problems regarding solvability for topologically closed but non-alternating plants behaviours. Moreover, we show that for topologically closed plant behaviours with alternating inputs and outputs both fixed-point algorithms collapse to the same 2-nested fixed-point. Using Corollary 2, this establishes equivalence of both synthesis algorithms in this case.