Synthesizing Approximate Implementations for Unrealizable Specifications
Abstract
The unrealizability of a specification is often due to the assumption that the behavior of the environment is unrestricted. In this paper, we present algorithms for synthesis in bounded environments, where the environment can only generate input sequences that are ultimately periodic words (lassos) with finite representations of bounded size. We provide automatatheoretic and symbolic approaches for solving this synthesis problem, and also study the synthesis of approximative implementations from unrealizable specifications. Such implementations may violate the specification in general, but are guaranteed to satisfy the specification on at least a specified portion of the boundedsize lassos. We evaluate the algorithms on different arbiter specifications.
1 Introduction
The objective of reactive synthesis is to automatically construct an implementation of a reactive system from a highlevel specification of its desired behaviour. While this idea holds a great promise, applying synthesis in practice often faces significant challenges. One of the main hurdles is that the system designer has to provide the right formal specification, which is often a difficult task [12]. In particular, since the system being synthesized is required to satisfy its requirements against all possible environments allowed by the specification, accurately capturing the designer’s knowledge about the environment in which the system will execute is crucial for being able to successfully synthesize an implementation.
Traditionally, environment assumptions are included in the specification, usually given as a temporal logic formula. There are, however less explored ways of incorporating information about the environment, one of which is to consider a bound on the size of the environment, that is, a bound on the size of the state space of a transition system that describes the possible environment behaviours. Restricting the space of possible environments can render an unrealizable specification into a realizable one. The temporal synthesis under such bounded environments was first studied in [6], where the authors extensively study the problem, in several versions, from the complexitytheoretic point of view.
In this paper, we follow a similar avenue of providing environment assumptions. However, instead of bounding the size of the state space of the environment, we associate a bound with the sequences of values of input signals produced by the environment. The infinite input sequences produced by a finitestate environment which interacts with a finite state system are ultimately periodic, and thus, each such infinite sequence \(\sigma \in \varSigma _I^\omega \), over the input alphabet \(\varSigma _I\), can be represented as a lasso, which is a pair (u, v) of finite words \(u\in \varSigma ^{*}_I\) and \(v \in \varSigma ^{+}_I\), such that \(\sigma =u\cdot v^\omega \). It is the length of such sequences that we consider a bound on. More precisely, given a bound \(k \in \mathbb {N}\), we consider the language of all infinite sequences of inputs that can be represented by a lasso (u, v) with \(u \cdot v = k\). The goal of the synthesis of lasso precise implementations is then to synthesize a system for which each execution resulting from a sequence of environment inputs in that language, satisfies a given linear temporal specification.
As an example, consider an arbiter serving two client processes. Each client issues a request when it wants to access a shared resource, and keeps the request signal up until it is done using the resource. The goal of the arbiter is to ensure the classical mutual exclusion property, by not granting access to the two clients simultaneously. The arbiter has to also ensure that each client request is eventually granted. This, however, is difficult since, first, a client might gain access to the resource and never lower the request signal, and second, the arbiter is not allowed to take away a grant unless the request has been set to false, or the client never sets the request to false in the future (the client has become unresponsive). The last two requirements together make the specification unrealizable, as the arbiter has no way of determining if a client has become unresponsive, or will lower the request signal in the future. If, however, the length of the lassos of the input sequences is bounded, then, after a sufficient number of steps, the arbiter can assume that if the request has not been set to false, then it will not be lowered in the future either, as the sequence of inputs must already have run at least once through it’s period that will be ultimately repeated from that point on.
This example shows that when the system designer has knowledge about the resources available to the environment processes, taking this knowledge into account can enable us to synthesize a system that is correct under this assumption.
In this paper we formally define the synthesis problem for lassoprecise implementations, that is, implementations that are correct for input lassos of bounded size, and describe an automatatheoretic approach to this synthesis problem. We also consider the synthesis of lassoprecise implementations of bounded size, and provide a symbolic synthesis algorithm based on quantified Boolean satisfiability.
Bounding the size of the input lassos can render some unrealizable specifications realizable, but, similarly to bounding the size of the environment, comes at the price of higher computational complexity. To alleviate this problem, we further study the synthesis of approximate implementations, where we relax the synthesis problem further, and only require that for a given \(\epsilon >0\) the ratio of input lassos of a given size for which the specification is satisfied, to the total number of input lassos of that size is at least \(1\epsilon \). We then propose an approximate synthesis method based on maximum model counting for Boolean formulas [5]. The benefits of the approximate approach are twofold. Firstly, it can often deliver highquality approximate solutions more efficiently than the lassoprecise synthesis method, and secondly, even when the specification is still unrealizable for a given lasso bound, we might be able to synthesize an implementation that is correct for a given fraction of the possible input lassos.
The rest of the paper is organized as follows. In Sect. 2 we discuss related work on environment assumptions in synthesis. In Sect. 3 we provide preliminaries on linear temporal properties and omegaautomata. In Sect. 3 we define the synthesis problem for lassoprecise implementations, and describe an automatatheoretic synthesis algorithm. In Sect. 5 we study the synthesis of lassoprecise implementations of bounded size, and provide a reduction to quantified Boolean satisfiability. In Sect. 6 we define the approximate version of the problem, and give a synthesis procedure based on maximum model counting. Finally, in Sect. 7 we present experimental results, and conclude in Sect. 8.
2 Related Work
Providing goodquality environment specifications (typically in the form of assumptions on the allowed behaviours of the environment) is crucial for the synthesis of implementations from highlevel specifications. Formal specifications, and thus also environment assumptions, are often hard to get right, and have been identified as one of the bottlenecks in formal methods and autonomy [12]. It is therefore not surprising, that there is a plethora of approaches addressing the problem of how to revise inadequate environment assumptions in the cases when these are the cause of unrealizability of the system requirements.
Most approaches in this direction build upon the idea of analyzing the cause of unrealizability of the specification and extracting assumptions that help eliminate this cause. The method proposed in [2] uses the game graph that is used to answer the realizability question in order to construct a Büchi automaton representing a minimal assumption that makes the specification realizable. The authors of [8] provide an alternative approach where the environment assumptions are gradually strengthened based on counterstrategies for the environment. The key ingredient for this approach is using a library of specification templates and user scenarios for the mining of assumptions, in order to generate goodquality assumptions. A similar approach is used in [1], where, however, assumption patterns are synthesized directly from the counterstrategy without the need for the user to provide patterns. A different line of work focuses on giving feedback to the user or specification designer about the reason for unrealizability, so that they can, if possible, revise the specification accordingly. The key challenge adressed there lies in providing easytounderstand feedback to users, which relies on finding a minimal cause for why the requirements are not achievable and generating a natural language explanation of this cause [11].
In the above mentioned approaches, assumptions are provided or constructed in the form of a temporal logic formula or an omegaautomaton. Thus, it is on the one hand often difficult for specification designers to specify the right assumptions, and on the other hand special care has to be taken by the assumption generation procedures to ensure that the constructed assumptions are simple enough for the user to understand and evaluate. The work [6] takes a different route, by making assumptions about the size of the environment. That is, including as an additional parameter to the synthesis problem a bound on the state space of the environment. Similarly to temporal logic assumptions, this relaxation of the synthesis problem can render unrealizable specifications into realizable ones. From the system designer point of view, however, it might be significantly easier to estimate the size of environments that are feasible in practice than to express the implications of this additional information in a temporal logic formula. In this paper we take a similar route to [6], and consider a bound on the cyclic structures in the environment’s behaviour. Thus, the closest to our work is the temporal synthesis for bounded environments studied in [6]. In fact, we show that the synthesis problem for lassoprecise implementations and the synthesis problem under bounded environments can be reduced to each other. However, while the focus in [6] is on the computational complexity of the bounded synthesis problems, here we provide both automatatheoretic, as well as symbolic approaches for solving the synthesis problem for environments with bounded lassos. We further consider an approximate version of this synthesis problem. The benefits of using approximation are twofold. Firstly, as shown in [6], while bounding the environment can make some specifications realizable, this comes at a high computational complexity price. In this case, approximation might be able to provide solutions of sufficient quality more efficiently. Furthermore, even after bounding the environment’s input behaviours, the specification might still remain unrealizable, in which case we would like to satisfy the requirements for as many input lassos as possible. In that sense, we get closer to synthesis methods for probabilistic temporal properties in probabilistic environments [7]. However, we consider nonprobabilistic environments (i.e., all possible inputs are equally likely), and provide probabilistic guarantees with desired confidence by employing maximum model counting techniques. Maximum model counting has previously been used for the synthesis of approximate nonreactive programs [5]. Here, on the other hand we are concerned with the synthesis of reactive systems from temporal specifications.
Bounding the size of the synthesized system implementation is a complementary restriction of the synthesis problem, which has attracted a lot of attention in recent years [4]. The computational complexity of the synthesis problem when both the system’s and the environment’s size is bounded has been studied in [6]. In this paper we provide a symbolic synthesis procedure for bounded synthesis of lassoprecise implementations based on quantified Boolean satisfiability.
3 Preliminaries
We now recall definitions and notation from formal languages and automata, and notions from reactive synthesis such as implementation and environment.
LinearTime Properties and Lassos. A lineartime property \(\varphi \) over an alphabet \(\varSigma \) is a set of infinite words \(\varphi \subseteq \varSigma ^\omega \). Elements of \(\varphi \) are called models of \(\varphi \). A lasso of length k over an alphabet \(\varSigma \) is a pair (u, v) of finite words \(u\in \varSigma ^{*}\) and \(v \in \varSigma ^{+}\) with \(u\cdot v~=k\) that induces the ultimately periodic word \(u \cdot v^\omega \). We call \(u\cdot v\) the base of the lasso or ultimately periodic word, and k the length of the lasso.
If a word \(w\in \varSigma ^*\) is a prefix of a word \(\sigma \in \varSigma ^*\cup \varSigma ^\omega \), we write \(w< \sigma \). For a language \(L \subseteq \varSigma ^* \cup \varSigma ^\omega \), we define \( Prefix (L) = \{w \in \varSigma ^* \mid \exists \sigma \in L: w < \sigma \}\) is the set of all finite words that are prefixes of words in L.
Implementations. We represent implementations as labeled transition systems. Let I and O be finite sets of input and output atomic propositions respectively. A \(2^O\)labeled \(2^I\)transition system is a tuple \(\mathcal T = (T,t_0,\tau ,o)\), consisting of a finite set of states T, an initial state \(t_0\in T\), a transition function \(\tau :T\times 2^I \rightarrow T\), and a labeling function \(o:T\rightarrow 2^O\). We denote by \(\mathcal T\) the size of an implementation \(\mathcal T\), defined as \(\mathcal T = T\). A path in \(\mathcal T\) is a sequence \(\pi :\mathbb N \rightarrow T \times 2^I\) of states and inputs that follows the transition function, i.e., for all \(i \in \mathbb N\) if \( \pi (i) = (t_i,e_i)\) and \(\pi (i + 1) = (t_{i+1}, e_{i+1})\), then \(t_{i+1} = \tau (t_i, e_i)\). We call a path initial if it starts with the initial state: \(\pi (0) = (t_0 , e )\) for some \(e \in 2^I\). For an initial path \(\pi \), we call the sequence \(\sigma _{\pi }:i \mapsto (o(t_i) \cup e_i) \in (2^{I \cup O})^\omega \) the trace of \(\pi \). We call the set of traces of a transition system \(\mathcal T\) the language of \(\mathcal T\), denoted \(L(\mathcal T)\).
Finitestate environments can be represented as labelled transition systems in a similar way, with the difference that the inputs are the outputs of the implementation, and the states of the environment are labelled with inputs for the implementation. More precisely, a finitestate environment is a \(2^I\)labeled \(2^O\)transition system \(\mathcal E = (E,s_0,\rho ,\iota )\). The composition of an implementation \(\mathcal T\) and an environment \(\mathcal E\) results in a set of traces of \(\mathcal T\), which we denote \(L_{\mathcal E}(\mathcal T)\), where \(\sigma =\sigma _0\sigma _1\ldots \in L_{\mathcal E}(\mathcal T)\) if and only if \(\sigma \in L(\mathcal T)\) and there exists an initial path \(s_0s_1\ldots \) in \(\mathcal E\) such that for all \(i \in \mathbb {N}\), \(s_{i+1} = \rho (s_i,\sigma _{i+1}\cap O)\) and \(\sigma _i \cap I = \iota (s_i)\).
LinearTime Temporal Logic. We specify properties of reactive systems (implementations) as formulas in Lineartime Temporal Logic (LTL) [9]. We consider the usual temporal operators Next Open image in new window , Until Open image in new window , and the derived operators Release Open image in new window , which is the dual operator of Open image in new window , Eventually Open image in new window and Globally Open image in new window . LTL formulas are defined over a set of atomic propositions \(\textit{AP} \). We denote the satisfaction of an LTL formula \(\varphi \) by an infinite sequence \(\sigma \in (2^{AP})^\omega \) of valuations of the atomic propositions by \(\sigma \models \varphi \) and call \(\sigma \) a model of \(\varphi \). For an LTL formula \(\varphi \) we define the language \(L(\varphi )\) of \(\varphi \) to be the set \(\{\sigma \in (2^{AP})^\omega \mid \sigma \models \varphi \}\).
For a set of atomic propositions \(\textit{AP} = O \cup I\), we say that a \(2^O\)labeled \(2^I\)transition system \(\mathcal T\) satisfies an LTL formula \(\varphi \), if and only if \(L(\mathcal T) \subseteq L(\varphi )\), i.e., every trace of \(\mathcal T\) satisfies \(\varphi \). In this case we call \(\mathcal T\) a model of \(\varphi \), denoted \(\mathcal T\models \varphi \). If \(\mathcal T\) satisfies \(\varphi \) for an environment \(\mathcal E\), i.e. \(L_\mathcal E(\mathcal T)\subseteq L(\varphi )\), we write \(\mathcal T\models _{\mathcal E}\varphi \).
For \(I \subseteq AP\) and \(\sigma \in (2^{AP})^* \cup (2^{AP})^\omega \), we denote with \(\sigma _{I}\) the projection of \(\sigma \) on I, obtained by the sequence of valuations of the propositions from I in \(\sigma \).
Automata Over Infinite Words. The automatatheoretic approach to reactive synthesis relies on the fact that an LTL specification can be translated to an automaton over infinite words, or, alternatively, that the specification can be provided directly as such an automaton. An alternating parity automaton over an alphabet \(\varSigma \) is a tuple \(\mathcal {A} = (Q,q_0,\delta ,\mu )\), where Q denotes a finite set of states, \(Q_0 \subseteq Q\) denotes a set of initial states, \(\delta \) denotes a transition function, and \(\mu : Q \rightarrow C \subset \mathbb {N}\) is a coloring function. The transition function \(\delta : Q \times \varSigma \rightarrow \mathbb {B}^+(Q)\) maps a state and an input letter to a positive Boolean combination of states [14].
A tree T over a set of directions D is a prefixclosed subset of \(D^*\). The empty sequence \(\epsilon \) is called the root. The children of a node \(n\in T\) are the nodes \(\{n\cdot d \in T \mid d\in D\}\). A \(\varSigma \)labeled tree is a pair (T, l), where \(l:T \rightarrow \varSigma \) is the labeling function. A run of \(\mathcal {A} = (Q,q_0,\delta ,\mu )\) on an infinite word \(\sigma = \alpha _0\alpha _1\dots \in \varSigma ^\omega \) is a Qlabeled tree (T, l) that satisfies the following constraints: (1) \(l(\epsilon ) = q_0\), and (2) for all \(n \in T\), if \(l(n)=q\), then \(\{ l(n')\mid n' \text { is a child of } n\}\) satisfies \(\delta (q,\alpha _{n})\).
A run tree is accepting if every branch either hits a true transition or is an infinite branch \(n_0n_1n_2 \dots \in T\), and the sequence \(l(n_0)l(n_1)l(n_2)\dots \) satisfies the parity condition, which requires that the highest color occurring infinitely often in the sequence \(\mu (l(n_0))\mu (l(n_1))\mu (l(n_2))\dots \in \mathbb N^\omega \) is even. An infinite word \(\sigma \) is accepted by an automaton \(\mathcal A\) if there exists an accepting run of \(\mathcal A\) on \(\sigma \). The set of infinite words accepted by \(\mathcal {A}\) is called its language, denoted \(L(\mathcal {A})\).
A nondeterministic automaton is a special alternating automaton, where for all states q and input letters \(\alpha \), \(\delta (q,\alpha )\) is a disjunction. An alternating automaton is called universal if, for all states q and input letters \(\alpha \), \(\delta (q,\alpha )\) is a conjunction. A universal and nondeterministic automaton is called deterministic.
A parity automaton is called a Büchi automaton if and only if the image of \(\mu \) is contained in \(\{1,2\}\), a coBüchi automaton if and only if the image of \(\alpha \) is contained in \(\{0,1\}\). Büchi and coBüchi automata are denoted by \((Q,Q_0,\delta ,F)\), where \(F\subseteq Q\) denotes the states with the higher color. A run graph of a Büchi automaton is thus accepting if, on every infinite path, there are infinitely many visits to states in F; a run graph of a coBüchi automaton is accepting if, on every path, there are only finitely many visits to states in F.
The next theorem states the relation between LTL and alternating Büchi automata, namely that every LTL formula \(\varphi \) can be translated to an alternating Büchi automaton with the same language and size linear in the length of \(\varphi \).
Theorem 1
[13] For every LTL formula \(\varphi \) there is an alternating Büchi automaton \(\mathcal A\) of size \(O(\varphi )\) with \(L(\mathcal A) = L(\varphi )\), where \(\varphi \) is the length of \(\varphi \).
Automata Over Finite Words. We also use automata over finite words as acceptors for languages consisting of prefixes of traces. A nondeterministic finite automaton over an alphabet \(\varSigma \) is a tuple \(\mathcal A= (Q,Q_0,\delta ,F)\), where Q and \(Q_0 \subseteq Q\) are again the states and initial states respectively, \(\delta : Q \times \varSigma \rightarrow 2^Q\) is the transition function and F is the set of accepting states. A run on a word \(a_1\ldots a_n\) is a sequence of states \(q_0q_1\ldots q_n\), where \(q_0 \in Q_0\) and \(q_{i+1} \in \delta (q_i,a_i)\). The run is accepting if \(q_n \in F\). Deterministic finite automata are defined similarly with the difference that there is a single initial state \(q_0\), and that the transition function is of the form \(\delta : Q\,{\times }\,\varSigma \rightarrow Q\). As usual, we denote the set of words accepted by a nondeterministic or deterministic finite automaton \(\mathcal A\) by \(L(\mathcal A)\).
4 Synthesis of LassoPrecise Implementations
In this section we first define the synthesis problem for environments producing input sequences representable as lassos of length bounded by a given number. We then provide an automatatheoretic algorithm for this synthesis problem.
4.1 LassoPrecise Implementations
We begin by formally defining the language of sequences of input values representable by lassos of a given length k. For the rest of the section, we consider lineartime properties defined over a set of atomic propositions \(\textit{AP} \). The subset \(I\subseteq \textit{AP} \) consists of the input atomic propositions controlled by the environment.
Definition 1
(Bounded Model Languages). Let \(\varphi \) be a lineartime property over a set of atomic propositions \(\textit{AP} \), let \(\varSigma = 2^{\textit{AP} }\), and let \(I \subseteq \textit{AP} \).
We say that an infinite word \(\sigma \in \varSigma ^\omega \) is an Ikmodel of \(\varphi \), for a bound \(k\in \mathbb {N}\), if and only if there are words \(u \in (2^I)^*\) and \(v \in (2^I)^+\) such that \(u\cdot v = k \) and \(\sigma _{I} = u\cdot v^\omega \). The language of Ikmodels of the property \(\varphi \) is defined by the set \(L_k^{I}(\varphi )=\{\sigma \in \varSigma ^\omega \mid \sigma \text { is a } I\text {}k\text {model of } \varphi \}\).
Note that a model of \(\varphi \) might be induced by lassos of different length and by more than one lasso of the same length, e.g, \(a^\omega \) is induced by (a, a) and \((\epsilon , a a)\). The next lemma establishes that if a model of \(\varphi \) can be represented by a lasso of length k then it can also be represented by a lasso of any larger length.
Lemma 1
For a lineartime property \(\varphi \) over \(\varSigma =2^{\textit{AP} }\), subset \(I \subseteq \textit{AP} \) of atomic propositions, and bound \(k\in \mathbb {N}\), we have \(L_k^I(\varphi )\subseteq L_{k'}^I(\varphi )\) for all \(k'> k. \)
Proof
Let \(\sigma \in L_k^{I}(\varphi )\). Then, \(\sigma \models \varphi \) and there exists \((u,v) \in (2^{I})^*\times (2^{I})^+\) such that \(u\cdot v=k\) and \(\sigma _I= u\cdot v^\omega \). Let \(v=v_1\dots v_k\). Since \( u\cdot v_1 (v_2\dots v_k v_1)^\omega = u\cdot (v_1\dots v_k)^\omega = \sigma _{I}\), we have \(\sigma \in L_{k+1}^{I}(\varphi )\). The claim follows by induction. \(\square \)
Using the definition of Ikmodels, the language of infinite sequences of environment inputs representable by lassos of length k can be expressed as \(L_k^I(\varSigma ^\omega )\).
Definition 2
(klassoprecise Implementations). For a lineartime property \(\varphi \) over \(\varSigma =2^{\textit{AP} }\), subset \(I \subseteq \textit{AP} \) of atomic propositions, and bound \(k\in \mathbb {N}\), we say that a transition system \(\mathcal T\) is a klassoprecise implementation of \(\varphi \), denoted \(\mathcal T\models _{k,I} \varphi \), if it holds that \(L_k^I(L(\mathcal T)) \subseteq \varphi \).
That is, in a klassoprecise implementation \(\mathcal T\) all the traces of \(\mathcal T\) that belong to the language \(L_k^I(\varSigma ^\omega )\) are Ikmodels of the specification \(\varphi \).
Problem definition: Synthesis of LassoPrecise Implementations
Given a lineartime property \(\varphi \) over atomic propositions \(\textit{AP} \) with input atomic propositions I, and given a bound \(k \in \mathbb {N}\), construct an implementation \(\mathcal T\) such that \(\mathcal T\models _{k,I} \varphi \), or determine that such an implementation does not exist.
Another way to bound the behaviour of the environment is to consider a bound on the size of its state space. The synthesis problem for bounded environments asks for a given linear temporal property \(\varphi \) and a bound \(k \in \mathbb {N}\) to synthesize a transition system \(\mathcal T\) such that for every possible environment \(\mathcal E\) of size at most k, the transition system \(\mathcal T\) satisfies \(\varphi \) under environment \(\mathcal E\), i.e., \(T\models _{\mathcal E} \varphi \).
We now establish the relationship between the synthesis of lassoprecise implementations and synthesis under bounded environments. Intuitively, the two synthesis problems can be reduced to each other since an environment of a given size, interacting with a given implementation, can only produce ultimately periodic sequences of inputs representable by lassos of length determined by the sizes of the environment and the implementation. This intuition is formalized in the following proposition, stating the connection between the two problems.
Proposition 1
 (1)
If \(\mathcal T\models _{\mathcal E} \varphi \) for all environments \(\mathcal E\) of size at most k, then \(\mathcal T\models _{k,I} \varphi \).
 (2)
If \(\mathcal T\models _{k\cdot \mathcal T,I} \varphi \), then \(\mathcal T\models _{\mathcal E} \varphi \) for all environments \(\mathcal E\) of size at most k.
Proof
For (1), let \(\mathcal T\) be a transition system such that \(\mathcal T\models _{\mathcal E} \varphi \) for all environments \(\mathcal E\) of size at most k. Assume, for the sake of contradiction, that \(\mathcal T\not \models _{k,I} \varphi \). Thus, that there exists a word \(\sigma \in L(\mathcal T)\), such that \(\sigma \in L_{k}^{I}(\varSigma ^\omega )\) and \(\sigma \not \models \varphi \).
Since \(\sigma \in L_{k}^{I}(\varSigma ^\omega )\), we can construct an environment \(\mathcal E\) of size at most k that produces the sequence of inputs \(\sigma _{I}\). Since \(\mathcal E\) is of size at most k, we have that \(\mathcal T\models _{\mathcal E} \varphi \). Thus, since \(\sigma \in L_{\mathcal E}(\mathcal T)\), we have \(\sigma \models \varphi \), which is a contradiction.
For (2), let \(\mathcal T\) be a transition system such that \(\mathcal T\models _{k\cdot \mathcal T,I} \varphi \). Assume, for the sake of contradiction that there exists an environment \(\mathcal E\) of size at most k such that \(\mathcal T\not \models _{\mathcal E} \varphi \). Since \(\mathcal T\not \models _{\mathcal E} \varphi \), there exists \(\sigma \in L_{\mathcal E}(\mathcal T)\) such that \(\sigma \not \models \varphi \). As the number of states of \(\mathcal E\) is at most k, the input sequences it generates can be represented as lassos of size \(k\cdot \mathcal T\). Thus, \(\sigma \in L_{k\cdot \mathcal T}^{I}(\varSigma ^\omega )\). This is a contradiction with the choice of \(\mathcal T\), according to which \(\mathcal T\models _{k\cdot \mathcal T,I} \varphi \). \(\square \)
4.2 AutomataTheoretic Synthesis of LassoPrecise Implementations
We now provide an automatatheoretic algorithm for the synthesis of lassoprecise implementations. The underlying idea of this approach is to first construct an automaton over finite traces that accepts all finite prefixes of traces in \(L_k^I(\varSigma ^\omega )\). Then, combining this automaton and an automaton representing the property \(\varphi \) we can construct an automaton whose language is nonempty if and only if there exists an klassoprecise implementation of \(\varphi \).
The next theorem presents the construction of a deterministic finite automaton for the language \( Prefix (L_k^{I}(\varSigma ^\omega ))\).
Theorem 2
For any set \(\textit{AP} \) of atomic propositions, subset \(I\subseteq \textit{AP} \), and bound \(k\in \mathbb {N}\) there is a deterministic finite automaton \(\mathcal A_k\) over alphabet \(\varSigma =2^{\textit{AP} }\), with size \((2^{I}+1)^k \cdot (k+1)^k\), such that \(L(\mathcal A_k)= \{w \in \varSigma ^* \mid \exists \sigma \in L_k^{I}(\varSigma ^\omega ). ~w <\sigma \}.\)
Idea & Construction. For given \(k\in \mathbb {N}\) we first define an automaton Open image in new window over Open image in new window , such that Open image in new window That, is Open image in new window is the set of all finite prefixes of infinite words over Open image in new window that can be represented by a lasso of length k. We can then define the automaton \(\mathcal A_k\) as the automaton that for each \(w \in \varSigma ^*\) simulates Open image in new window on the projection \(w_{I}\) of w.

\(q_0 = (\#^k,(1,2,\dots ,k))\),
Proof
States of the form \((w\cdot \alpha \cdot \#^{m},t)\) with \(m \ge 1\) store the portion of the input word read so far, for input words of length smaller than k. In states of this form we have \(t=(1,2,\ldots , k)\), which implies that all such states are accepting. In turn, this means that \(\mathcal A_k\) accepts all words of length smaller or equal to k. This is justified by the fact that, each word of length smaller or equal to k is a prefix of an infinite word in Open image in new window , obtained by repeating the prefix infinitely often. Now, let us consider words of length greater than k.
In states of the form \((u,(i_1,\ldots ,i_k))\), with Open image in new window , the word u stores the first k letters of the input word. Intuitively, the tuple \((i_1,\ldots ,i_k)\) stores the information about the loops that are still possible, given the portion of the input word that is read thus far. To see this, let us consider a word Open image in new window such that \(w = l > k\), and let \(q_0 q_1 \dots q_l\) be the run of \(\mathcal A_k\) on w. The state \(q_l\) is of the form \(q_l = (w(1)\ldots w(k), (i_1^l,\ldots ,i_k^l))\). It can be shown by induction on l that for each j we have \(i_j^l \ne \) if and only if w is of the form \(w=w'\cdot w''\cdot w'''\) where \(w' = w(1)\ldots w(j1)\), \(w'' = (w(j)\ldots w(k))^k\) for some \(k \ge 0\), and \(w''' = (w(j)\ldots w(i_j^l1))\). Thus, if \(i_j^l \ne \), then it is possible to have a loop starting at position j, and \(i_j^l\) is such that \((w(j)\ldots w(i_j^l1))\) is the prefix of \(w(j)\ldots w(k)\) appearing after the (possibly empty) sequence of repetitions of \(w(j)\ldots w(k)\). This means, that if \(i_j^l \ne \), then w is a prefix of the infinite word Open image in new window . Therefore, if the run of \(\mathcal A_k\) on a word w with \(w > k\) is accepting, then there exists Open image in new window such that \(w <\sigma \).
For the other direction, suppose that for each j, we have \(i_j^l=\). Take any j, and consider the first position m in the run \(q_0 q_1\ldots q_l\) where \(i_j^m=\). By the definition of \(\delta \) we have that \(w(m) \ne w(i_j^{m1})\). This means that the prefix \(w(1)\ldots w(m)\) cannot be extended to the word \(w(1)\ldots w(j1)(w(j)\ldots w(k))^\omega \). Since for every \(j\in \{1,\ldots ,k\}\) we can find such a position m, it holds that there does not exist Open image in new window such that \( w <\sigma \). This concludes the proof. \(\square \)
The automaton constructed in the previous theorem has size which is exponential in the length of the lassos. In the next theorem we show that this exponential blowup is unavoidable. That is, we show that every nondeterministic finite automaton for the language \( Prefix (L_k^{I}(\varSigma ^\omega ))\) is of size at least \(2^{\varOmega (k)}\).
Theorem 3
For any bound \(k\in \mathbb {N}\) and sets of atomic propositions \(\textit{AP} \) and \(\emptyset \ne I \subseteq \textit{AP} \), every nondeterministic finite automaton \(\mathcal N\) over the alphabet \(\varSigma =2^{\textit{AP} }\) that recognizes \(L = \{w \in \varSigma ^* \mid \exists \sigma \in L_k^{I}(\varSigma ^\omega ). ~w <\sigma \}\) is of size at least \(2^{\varOmega (k)}\).
Proof
Let \(\mathcal N= (Q,Q_0,\delta ,F)\) be a nondeterministic finite automaton for L. For each \(w \in \varSigma ^k\), we have that \(w\cdot w \in L\). Therefore, for each \(w \in \varSigma ^k\) there exists at least one accepting run \(\rho =q_0 q_1 \ldots q_f\) of \(\mathcal N\) on \(w\cdot w\). We denote with \(q(\rho ,m)\) the state \(q_m\) that appears at the position indexed m of a run \(\rho \).
Let \(a \in 2^I\) be a letter in \(2^I\), and let \(\varSigma ' = \varSigma \setminus \{ a' \in \varSigma \mid a'_{I} = a\}\). Let \(L' \subseteq L\) be the language \(L' = \{w \in \varSigma ^k \mid \exists w' \in (\varSigma ')^{k1},a'\in \varSigma :~w = w'\cdot a' \text { and }a'_{I}=a\}\). That is, \(L'\) consists of the words of length k in which letters \(a'\) with \(a'_I=a\) appear in the last position and only in the last position.
Assume that this does not hold, i.e., \(Q_k < 2^{k1}\). Since \(L' \ge 2^{k1}\), this implies that there exist \(w_1,w_2 \in L'\), such that \(w_1_I \ne w_2_I\) and there exists accepting runs \(\rho _1\) and \(\rho _2\) of \(\mathcal N\) on \(w_1\cdot w_1\) and \(w_2\cdot w_2\) respectively, such that \(q(\rho _1,k) = q(\rho _2,k)\). That is, there must be two words in \(L'\) with \(w_1_I \ne w_2_I\), which have accepting runs on \(w_1\cdot w_1\) and \(w_2 \cdot w_2\) visiting the same state at position k.
We now construct a run \(\rho _{1,2}\) on the word \(w_1 \cdot w_2\) that follows \(\rho _1\) for the first k steps on \(w_1\), ending in state \(q(\rho _1,k)\), and from there on follows \(\rho _2\) on \(w_2\). It is easy to see that \(\rho _{1,2}\) is a run on the word \(w_1 \cdot w_2\). The run is accepting, since \(\rho _2\) is accepting. This means that \(w_1 \cdot w_2 \in L\), which we will show leads to contradiction.
To see this, recall that \(w_1 = w_1'\cdot a'\) and \(w_2 = w_2' \cdot a''\), and \(w_1_I \ne w_2_I\), and \(a'_I=a''_I=a\). Since \(w_1\cdot w_2 \in L\), we have that \(w_1'\cdot a' \cdot w_2' \cdot a'' < \sigma \) for some \(\sigma \in L_k^{I}(\varSigma ^\omega )\). That is, there exists a lasso for some word \(\sigma \), and \(w_1'\cdot a' \cdot w_2' \cdot a''\) is a prefix of this word. Since a does not appear in \(w_2'_{I}\), this means that the loop in this lasso is the whole word \(w_1_I\), which is not possible, since \(w_1_I \ne w_2_I\).
This is a contradiction, which shows that \(Q \ge Q_k \ge 2^{k1}\). Since \(\mathcal N\) was an arbitrary nondeterministic finite automaton for L, this implies that the minimal automaton for L has at least \(2^{\varOmega (k)}\) states, which concludes the proof. \(\square \)
Using the automaton from Theorem 2, we can transform every property automaton \(\mathcal A\) into an automaton that accepts words representable by lassos of length less than or equal to k if and only if they are in \(L(\mathcal A)\), and accepts all words that are not representable by lassos of length less than or equal to k.
Theorem 4
Let \(\textit{AP} \) be a set of atomic propositions, and let \(I \subseteq \textit{AP} \). For every (deterministic, nondeterministic or alternating) parity automaton \(\mathcal A\) over \(\varSigma =2^{\textit{AP} }\), and \(k \in \mathbb {N}\), there is a (deterministic, nondeterministic or alternating) parity automaton \(\mathcal A'\) of size \(2^{O(k)} \cdot \mathcal A\), s.t., \(L(\mathcal A') = (L_k^I(\varSigma ^\omega )\cap L(\mathcal A)) \cup (\varSigma ^\omega \setminus L_k^I(\varSigma ^\omega ))\).
Proof

Open image in new window (when \(\mathcal A\) is deterministic \(Q_0'\) is a singleton set);

Open image in new window where Open image in new window is the Boolean expression obtained from \(\delta (q,\alpha )\) by replacing every state \(q'\) by the state Open image in new window ;
Intuitively, the automaton \(\mathcal A'\) is constructed as the product of \(\mathcal A\) and \(\mathcal D\), where runs entering a state in \(\mathcal D\) that is not accepting in \(\mathcal D\) are accepting in \(\mathcal A'\). To see this, recall from the construction in Theorem 2 that once \(\mathcal D\) enters a state in Open image in new window it remains in such a state forever. Thus, by setting the color of all states Open image in new window where Open image in new window to 0, we ensure that words containing a prefix rejected by \(\mathcal D\) have only runs in which the highest color appearing infinitely often is 0. Thus, we ensure that all words that are not representable by lassos of length less than or equal to k are accepted by \(\mathcal A'\), while words representable by lassos of length less than or equal to k are accepted if and only if they are in \(L(\mathcal A)\). \(\square \)
The following theorem is a consequence of the one above, and provides us with an automatatheoretic approach to solving the lassoprecise synthesis problem.
Theorem 5
(Synthesis). Let \(\textit{AP} \) be a set of atomic propositions, and \(I \subseteq \textit{AP} \) be a subset of \(\textit{AP} \) consisting of the atomic propositions controlled by the environment. For a specification, given as a deterministic parity automaton \(\mathcal P\) over the alphabet \(\varSigma = 2^{\textit{AP} }\), and a bound \(k \in \mathbb {N}\), finding an implementation \(\mathcal T\), such that, \(\mathcal T\models _{k,I} \mathcal P\) can be done in time polynomial in the size of the automaton \(\mathcal P\) and exponential in the bound k.
5 Bounded Synthesis of LassoPrecise Implementations
For a specification \(\varphi \) given as an LTL formula, a bound n on the size of the synthesized implementation and a bound k on the lassos of input sequences, bounded synthesis of lassoprecise implementations searches for an implementation \(\mathcal T\) of size n, such that \(\mathcal T\models _{k,I} \varphi \). Using the automata constructions in the previous section we can construct a universal coBüchi automaton for the language \(L_k^I(\varphi ) \cup (\varSigma ^\omega \setminus L_k^I(\varSigma ^\omega ))\) and construct the constraint system as presented in [4]. This constraint system is exponential in both \(\varphi \) and k. In the following we show how the problem can be encoded as a quantified Boolean formula of size polynomial in \(\varphi \) and k.
Theorem 6
For a specification given as an LTL formula \(\varphi \), and bounds \(k \in \mathbb {N}\) and \(n\in \mathbb {N}\), there exists a quantified Boolean formula \(\phi \), such that, \(\phi \) is satisfiable if and only if there is a transition system \(\mathcal T=(T,t_0,\tau ,o)\) of size n with \(\mathcal T\models _{k,I} \varphi \). The size of \(\phi \) is in \(O(\varphi  + n^2 + k^2)\). The number of variables of \(\phi \) is equal to \(n\cdot (n\cdot 2^{I} +O) + k\cdot (I+1) +n\cdot k(O+n+1)\).
An assignment to the variables satisfies the formula in line (6), if it represents a deterministic transition system (\(\varphi _{\text {det}}\)) in which lassos of length \(n\cdot k\) (\(\varphi _{\text {lasso} \wedge \varphi _{\in \mathcal T}^{n,k}}\)) satisfy the property \(\varphi \) (\(\llbracket \varphi \rrbracket _0^{(k, n\cdot k)})\)). These constraints are defined as follows.
\(\varphi _{\text {det}}\): A transition system is deterministic if for each state t and input i there is exactly one transition \(\tau _{t,i,t'}\) to some state \(t'\): \(\bigwedge \limits _{t \in T} ~\bigwedge \limits _{i \in 2^I} ~\bigvee \limits _{t' \in T} (\tau _{t,i,t'} \wedge \bigwedge \limits _{t' \not =t''} \overline{\tau _{t,i,t''}})\).
\(h<m\)  \(h=m\)  

\(\llbracket i \rrbracket ^{k,m}_h\)  \( \bigwedge \limits _{0\le j' <k}(l_{j'} \rightarrow i_{\varDelta (h,k,j')})\)  \(\bigvee _{j=0}^{m1} (l'_j \wedge \bigwedge \limits _{0\le j' <k}(l_{j'} \rightarrow i_{\varDelta (j,k,j')}))\) 
\(\llbracket \lnot i \rrbracket ^{k,m}_h\)  \(\bigwedge \limits _{0\le j' <k}(l_{j'} \rightarrow \lnot i_{\varDelta (h,k,j')})\)  \(\bigvee _{j=0}^{m1} (l'_j \wedge \bigwedge \limits _{0\le j' <k}(l_{j'} \rightarrow \lnot i_{\varDelta (j,k,j')}))\) 
\(\llbracket o \rrbracket ^{k,m}_h\)  \(o_h\)  \(\bigvee _{j=0}^{m1} (l'_j \wedge o_j)\) 
\(\llbracket \lnot o \rrbracket ^{k,m}_h\)  \(\lnot o_h\)  \(\bigvee _{j=0}^{m1} (l'_j \wedge \lnot o_j)\) 
6 Synthesis of Approximate Implementations
Definition 3
(\(\epsilon \)kApproximation). For a specification \(\varphi \), a bound k, and an error rate \(\epsilon \), we say that a transition system \(\mathcal T\) approximately satisfies \(\varphi \) with an error rate \(\epsilon \) for lassos of length at most k, denoted by \(\mathcal T\models _{k,I}^\epsilon \varphi \), if and only if, \(\frac{\{\sigma \mid \sigma \in L^I_k(L(\mathcal T)), \sigma \models \varphi \}}{L_k^I((2^I)^\omega )} \ge 1\epsilon \). We call \(\mathcal T\) an \(\epsilon \)kapproximation of \(\varphi \).
Theorem 7
For a specification given as a deterministic parity automaton P, a bound k and a error rate \(0 \le \epsilon \le 1\), checking whether there is an implementation \(\mathcal T\), such that, \(\mathcal T\models _{k,I}^\epsilon P\) can be done in time polynomial in P and exponential in k.
Proof
For a given \(\epsilon \) and k, we construct a nondeterministic parity tree automaton \(\mathcal N\) that accepts all \(\epsilon \)kapproximations with respect to L(P). For \(\epsilon \), we can compute the minimal number m of lassos from \(L_k^I((2^I)^\omega )\) for which an \(\epsilon \)kapproximation has to satisfy the specification. In its initial state, the automaton \(\mathcal N\) guesses m many lassos and accepts a transition system if it does not violate the specification on any of these lassos. The latter check is done by following the structure of the automaton constructed for P using Theorem 4. In order to check whether there is an \(\epsilon \)kapproximation for P, we solve the emptiness game of \(\mathcal N\). The size of \(\mathcal N\) is \((2^k)^{m+1} \cdot P\). \(\square \)
6.1 Symbolic Approach
In the following, we present a symbolic approach for finding \(\epsilon \)kapproximations based on maximum model counting. We show that we can build a constraint system and apply a maximum model counting algorithm to compute a transition system that satisfies a specification for a maximum number of input sequences.
Definition 4
(Maximum Model Counting [5]). Let X, Y and Z be sets of propositional variables and \(\phi \) be a formula over X, Y and Z. Let x denote an assignment to X, y an assignment to Y, and z an assignment to Z. The maximum model counting problem for \(\phi \) over X and Y is computing a solution for \(\max \limits _{x}\#y.\exists z. \phi (x,y,z). \)
Experimental results for the symbolic approaches. The rate in the approximate approach is the rate of input lassos on which the specification is satisfied.
Instance  QBF  MaxCount  

Spec.  Proc.  #States  Bound  Result  #Gates  \(\forall \)  \(\exists \)  Time  #Max  #Count  Rate  Time 
RoundRobin Arbiter  2  2  4  Unreal  15556  48  12  9.91 s  12  8  0.5  26 s 
2  3  2  Unreal  5338  40  24  2.45 s  24  4  0.88  161 s  
2  4  2  Real  13414  60  12  12.15 s  40  4  0.88  283 s  
Greedy Arbiter  1  2  2  Real  1597  20  10  0.41 s  10  4  1.0  0.79 s 
1  2  3  Unreal  4749  30  10  1.95 s  10  6  0.88  3.86 s  
1  3  3  Unreal  16861  48  21  17.26 s  21  6  0.88  20.83 s  
1  4  3  Real  43692  78  36  3 min 7.44 s  36  6  1.0  2 min 43 s  
1  4  4    169829  104  36  TO  36  8    TO  
2  4  2  Real  24688  62  72  1 min. 24 s  72  6    TO  
2  4  3  Unreal  103433  93  72  27 min 15.2  72  12    TO  
3  2  2  Unreal  3985  93  72  1.39 s  38  8  0.65  4.18 s 
The formulas \(\varphi _{\text {det}}\), \(\varphi _{\text {lasso}}\), \(\varphi _{\in \mathcal T}^{n,k}\) and \(\llbracket \varphi \rrbracket _0^{k,n\cdot k} \) are defined as in the previous section. The formula \(\llbracket k \rrbracket _0 \) is defined over that variables in line (13) and makes sure that input lasso that represent the same infinite sequence are not counted twice by unrolling the lasso to size 2k.
Theorem 8
For a specification given as an LTL formula \(\varphi \), and bounds k and n, and an error rate \(\epsilon \), the propositional formula \(\phi \) defined above is of size \(O(\varphi  + n^2 + k^2)\). The number of variables of \(\phi \) is equal to \(n\cdot (n\cdot 2^{I} +O) + k\cdot (k\cdot I+ I+1) +n\cdot k(O+n+1)\).
7 Experimental Results
The results are presented in Table 1. As usual in synthesis, the size of the instances grows quickly as the size bound and number of processes increase. Inspecting the encoding constraints shows that the constraint for the specification is responsible for more than 80% of the number of gates in the encoding. The results show that, using the approach we proposed, we can synthesize implementations for unrealizable specifications by bounding the environment. The results for the approximate synthesis method further demonstrate that for the unrealizable cases one can still obtain approximative implementations that satisfy the specification on a large number of input sequences.
8 Conclusion
In many cases, the unrealizability of a specification is due to the assumption that the environment has unlimited power in producing inputs to the system. In this paper, we have investigated the problem of synthesizing implementations under bounded environment behaviors. We have presented algorithms for solving the synthesis problem for bounded lassos and the synthesis of approximate implementations that satisfy the specification up to a certain rate.
We have also provided polynomial encodings of the problems into quantified Boolean formulas and maximum model counting instances. Our experiments demonstrate the principal feasibility of the approach. Our experiments also show that the instances can quickly become large. While this is a common phenomenon for synthesis, there clearly is a lot of room for optimization and experimentation with both the solvers for quantified Boolean expressions and for maximum model counting.
References
 1.Alur, R., Moarref, S., Topcu, U.: Counterstrategy guided refinement of GR(1) temporal logic specifications. In: Formal Methods in ComputerAided Design, FMCAD 2013, Portland, OR, USA, October 20–23, 2013, pp. 26–33. IEEE (2013)Google Scholar
 2.Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Environment assumptions for synthesis. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 147–161. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540853619_14CrossRefGoogle Scholar
 3.Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7–34 (2001)CrossRefGoogle Scholar
 4.Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Software Tools Technol. Transf. 15(5–6), 519–539 (2013)CrossRefGoogle Scholar
 5.Fremont, D.J., Rabe, M.N., Seshia, S.A.: Maximum model counting. Technical Report UCB/EECS2016169, EECS Department, University of California, Berkeley, Nov 2016. This is the extended version of a paper to appear at AAAI 2017Google Scholar
 6.Kupferman, O., Lustig, Y., Vardi, M.Y., Yannakakis, M.: Temporal synthesis for bounded systems and environments. In: Schwentick, T., Dürr, C. (eds.) 28th International Symposium on Theoretical Aspects of Computer Science, STACS 2011, March 10–12, 2011, Dortmund, Germany, vol. 9 of LIPIcs, pages 615–626. Schloss Dagstuhl  LeibnizZentrum fuer Informatik (2011)Google Scholar
 7.Kwiatkowska, M., Parker, D.: Automated verification and strategy synthesis for probabilistic systems. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 5–22. Springer, Cham (2013). https://doi.org/10.1007/9783319024448_2CrossRefzbMATHGoogle Scholar
 8.Li, W., Dworkin, L., Seshia, S.A.: Mining assumptions for synthesis. In: Singh, S., Jobstmann, B., Kishinevsky, M., Brandt, J. (eds.) 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011, Cambridge, UK, 11–13 July, 2011, pp. 43–50. IEEE (2011)Google Scholar
 9.Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS 1977, Washington, DC, USA, 1977. IEEE Computer Society (1977)Google Scholar
 10.Rabe, M.N., Tentrup, L.: Caqe: a certifying QBF solver. In: Proceedings of the 15th Conference on Formal Methods in Computeraided Design (FMCAD 2015), pp. 136–143, September 2015Google Scholar
 11.Raman, V., Lignos, C., Finucane, C., Lee, K.C.T., Marcus, M.P., KressGazit, H.: Sorry dave, i’m afraid I can’t do that: explaining unachievable robot tasks using natural language. In: Newman, P., Fox, D., Hsu, D. (eds.), Robotics: Science and Systems IX, Technische Universität Berlin, Berlin, Germany, June 24  June 28, 2013 (2013)Google Scholar
 12.Rozier, K.Y.: Specification: the biggest bottleneck in formal methods and autonomy. In: Blazy, S., Chechik, M. (eds.) VSTTE 2016. LNCS, vol. 9971, pp. 8–26. Springer, Cham (2016). https://doi.org/10.1007/9783319488691_2CrossRefGoogle Scholar
 13.Vardi, M.Y.: Nontraditional applications of automata theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 575–597. Springer, Heidelberg (1994). https://doi.org/10.1007/3540578870_116CrossRefGoogle Scholar
 14.Vardi, M.Y.: Alternating automata and program verification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol. 1000, pp. 471–485. Springer, Heidelberg (1995). https://doi.org/10.1007/BFb0015261CrossRefGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.