






\subsubsection{Robotic Navigation.}
We applied our method to the strategy synthesis for a robotic museum guide. The robot has to give a tour of the exhibitions in a specific order, which constitutes the hard specification. Preferably, it also avoids certain locations, such as the library, or the passage when it is occupied. These preferences are encoded in the soft specifications. There is one input variable that designates the occupancy of the passage, and eight output variables defining the position of the robot. 
The full set of specifications is given in Appendix~\ref{sec:robot-nav-appx}.

Table~\ref{tab:inst-robot} summarizes the results. With implementation bound of 8, the hard specification is realizable and a partial satisfaction of soft specifications is achieved. This strategy always selects the passage to transition from Exhibition 1 to Exhibition 2 and hence, avoids the library. It also violates the requirement of not entering the staff's office once, to acquire access to Exhibition 2. With implementation bound 10, a better strategy (with higher objective value) that alternates between entering the library and the passage is synthesized. This strategy is actually the optimal one with respect to the defined quantitative metric.

\begin{table*}[b!]\centering\footnotesize
	\begin{tabular*}{1\linewidth}{ccccccccccccccc}
		\toprule
		&& \multicolumn{3}{c}{Encoding} && \multicolumn{3}{c}{Solution} && \multicolumn{5}{c}{Time (s)} \\
		\cline{3-5} \cline{7-9} \cline{11-15}
		$|\trans|$ & \phantom{00} & \# vars & \phantom{0} & \# clauses & \phantom{00} & sat. & \phantom{0} & $\Sigma weights$ & \phantom{00} & Spot & \phantom{0} & Open-WBO & \phantom{0} & enc.+solve \\
		\midrule
		2 && 2837 && 18974 && UNSAT && 0 (39) && 0.61 && 0.0088 && 0.10 \\
		4 && 14573 && 98152 && UNSAT && 0 (39) && 0.61 && 0.057 && 0.46 \\
		6 && 40857 && 271474 && UNSAT && 0 (39) && 0.61 && 2.54 && 3.7 \\
		8 && 72057 && 482414 && SAT && 25 (39) && 0.61 && 2853 && 2856 \\
		10 && 135839 && 894892 && SAT && 30 (39) && 0.61 && time-out && time-out \\
		\bottomrule
	\end{tabular*}
	\caption{Results of applying synthesis with maximum realizability to the robotic navigation example, with different bounds on implementation size $|\trans|$. We report on the number of variables and clauses in the encoding, the satisfiability of hard constraints, the value (and bound) of the MaxSAT objective function, the running times of Spot and Open-WBO, and the time of the solver plus the time for generating the encoding.}
	\label{tab:inst-robot}
\end{table*}

\vspace{-.3cm}
\subsubsection{Power Distribution Network.}
We consider the problem of dynamic reconfiguration of power distribution networks. A power network consists of a set $\supplies$ of power supplies (generators) and a set $\loads$ of loads (consumers). The network is a bipartite graph with edges between supplies and loads, where each supply is connected to multiple loads and each load is connected to multiple supplies. Each power supply has an associated capacity, which determines how many loads it can power at a given point in time. Thus, it is possible that not all loads can be powered all the time. Some loads are critical and must be powered continuously, while others are not and should be powered when possible. Some loads can be initializing, meaning they must be powered only initially for several steps. Additionally, power supplies can become faulty during operation, which necessitates dynamic network reconfiguration.

\begin{table*}[b!]\centering\footnotesize

\begin{tabular*}{1\linewidth}{@{}c|ccccccccccccccccccc@{}}
\toprule
&& &\multicolumn{5}{c}{Network} &&\multicolumn{5}{c}{Load characterization} && \multicolumn{5}{c}{Specifications} \\
\cline{4-8} \cline{10-14} \cline{16-20}
& \begin{tabular}{c@{}} Instance \\ \# \end{tabular} & \phantom{ }\phantom{ }\phantom{ } & $|\supplies|$ & \phantom{} & $|\loads|$ & \phantom{} &  $\caps$ & \phantom{ }\phantom{ }\phantom{ } & crit. & \phantom{} & non-crit. & \phantom{} & init. & \phantom{ } \phantom{ }\phantom{ } \phantom{} & $|\inpv|$ & \phantom{} & $|\outv|$ & \phantom{} & \begin{tabular}{@{}c@{}} \# Soft \\ \; spec. \end{tabular}\\
\midrule
fully     & 1 && 3 && 3 &&  1 && 1 && 2 && 0 &&  2 && 9 && 2 \\
connected, & 2 && 3 && 6 &&  2 && 2 && 4 && 0 &&  2 && 18 && 4 \\
switching & 3 && 3 && 3 &&  1 && 0 && 2 && 1 &&  2 && 9 && 2 \\
allowed & 4 && 3 && 6 &&  2 && 1 && 4 && 1 &&  2 && 18 && 4 \\
\midrule
sparse,&5 && 4 && 2 &&  1 && 1 && 1 && 0 &&  3 && 4 && 1 \\
switching&6 && 4 && 4 &&  1 && 1 && 3 && 0 &&  3 && 8 && 3 \\
allowed&7 && 4 && 6 &&  1 && 1 && 5 && 0 &&  3 && 12 && 5 \\
&8 && 4 && 8 &&  1 && 1 && 7 && 0 &&  3 && 16 && 7 \\
\midrule
sparse,&9 && 4 && 2 &&  1 && 1 && 1 && 0 &&  3 && 4 && 5 \\
switching&10 && 4 && 4 &&  1 && 1 && 3 && 0 &&  3 && 8 && 11 \\
restricted&11 && 4 && 6 &&  1 && 1 && 5 && 0 &&  3 && 12 && 17 \\
&12 && 4 && 8 &&  1 && 1 && 7 && 0 &&  3 && 16 && 23 \\
\bottomrule
\end{tabular*}
\caption{Power distribution network instances. 
 An instance is determined by the number supplies $|\supplies|$, the number of loads $|\loads|$, the capacity of supplies $\caps$, the number of critical, non-critical and initializing loads. We also show the number of input $|\inpv|$ and output $|\outv|$ propositions and the number of soft specifications.}
\label{tab:def-inst}
\vspace{-.5cm}
\end{table*}

We apply our method to the problem of synthesizing a relay-switching strategy from LTL specifications. The input propositions $\inpv$ determine which, if any, of the supplies are faulty at each step. We are given an upper bound on the number of supplies that can be simultaneously faulty. The set $\outv$ of output propositions contains one proposition $\slp$ for each load $l \in \loads$  and each supply $p \in \supplies$ that are connected. The meaning of $\slp$ is that $l$ is powered by $p$.

The hard specifications assert that the critical loads must always be powered, the initializing loads should be powered initially, a load is powered by at most one supply, the capacity of supplies is not exceeded, and when a supply is faulty it is not in use.
The soft specifications state that non-critical loads are always powered, and that a powered load should remain powered unless its supply fails.

The full specifications are given in Appendix~\ref{sec:power-net-appx}. Table~\ref{tab:def-inst} describes the instances to which we applied our synthesis method. Power supplies have the same capacity $\caps$ (number of loads they can power) and at most one can be faulty. We consider three categories of instances, depending on the network connectivity (full or sparse), and whether we restrict frequent switching of supplies.
In Table~\ref{tab:inst-stat-1}, we report results for the instances from the first and the last category (for the middle category, see Appendix~\ref{sec:power-net-appx}). In the first set of instances in Table~\ref{tab:inst-stat-1}, we see the effect of specifications with large number of variables (due to full connectivity), where the bottleneck is the LTL to automata translation. In the second set in Table~\ref{tab:inst-stat-1} the limiting factor is the number of soft specifications, leading to large weights and variable numbers in the MaxSAT formulation.

\begin{table*}[!htbp]\centering\footnotesize
	\begin{tabular*}{1\linewidth}{@{}c|cccccccccccccc@{}}
		\toprule
		&& && \multicolumn{3}{c}{Encoding} && \multicolumn{1}{c}{Solution} && \multicolumn{5}{c}{Time (s)} \\
		\cline{5-7} \cline{9-9} \cline{11-15}
		\begin{tabular}{@{}c@{}} Instance \\ \# \end{tabular} & \phantom{0} & $|\trans|$ & \phantom{0} & \# vars & \phantom{0} & \# clauses & \phantom{0} & $\Sigma weights$ & \phantom{0} & Spot & \phantom{0} & Open-WBO & \phantom{0} & enc.+solve \\
		\midrule
		1 && 2 && 278 && 3599 && 11 (14) && 0.14 && 0.0040 && 0.071 \\
		  && 4 && 1102 && 20427 && 11 (14) && 0.14 && 0.017 && 0.14 \\
		  && 6 && 2958 && 60007 && 11 (14) && 0.14 && 0.64 && 0.97 \\
		  && 8 && 4966 && 106495 && 11 (14) && 0.14 && 71 && 71 \\
		\midrule
		2 && 2 && 516 && 14261 && 74 (84) && 85 && 0.013 && 0.16 \\
		&& 4 && 1988 && 81861 && 74 (84) && 85 && 0.079 && 0.59 \\
		&& 6 && 5292 && 240949 && 74 (84) && 85 && 2.2 && 3.6 \\
		&& 8 && 8844 && 427997 && 74 (84) && 85 && 1402 && 1405 \\
		\midrule
		3 && 2 && 334 && 7983 && 11 (14) && 0.29 && 0.032 && 0.12 \\
		&& 4 && 1510 && 45259 && 13 (14) && 0.29 && 0.021 && 0.26 \\
		&& 6 && 4302 && 132295 && 13 (14) && 0.29 && 0.099 && 0.77 \\
		&& 8 && 7334 && 235007 && 13 (14) && 0.29 && 1.0 && 2.2 \\
		\midrule
		4 && 2 && 572 && 38997 && 74 (84) && 200 && 0.023 && 0.37 \\
		&& 4 && 2396 && 224325 && 78 (84) && 200 && 0.14 && 1.5 \\
		&& 6 && 6636 && 659413 && 78 (84) && 200 && 1.1 && 4.9 \\
		&& 8 && 11212 && 1171933 && 78 (84) && 200 && 142 && 150 \\
		\midrule\midrule
		9 && 2 && 1047 && 10328 && 137 (155) && 0.18 && 0.0072 && 0.14 \\
		&& 4 && 3479 && 59298 && 137 (155) && 0.18 && 0.071 && 0.45 \\
		&& 6 && 8559 && 176428 && 137 (155) && 0.18 && 6.0 && 7.1 \\
		&& 8 && 26235 && 610246 && N/A (155) && 0.18 && time-out && time-out \\
		\midrule
		10 && 2 && 2153 && 22714 && 1403 (1463) && 0.48 && 0.015 && 0.27 \\
		&& 4 && 7113 && 130416 && 1403 (1463) && 0.48 && 0.60 && 1.5 \\
		&& 6 && 17505 && 387814 && 1403 (1463) && 0.48 && 716 && 718 \\
		&& 8 && 53693 && 1340908 && N/A (1463) && 0.48 && time-out && time-out \\
		\midrule
		11 && 2 && 3259 && 37596 && 5093 (5219) && 1.9 && 0.023 && 0.42 \\
		&& 4 && 10747 && 216254 && 5093 (5219) && 1.9 && 1.1 && 2.4 \\
		&& 6 && 26451 && 642976 && 5093 (5219) && 1.9 && 801 && 808 \\
		&& 8 && 81151 && 2222770 && N/A (5219) && 1.9 && time-out && time-out \\
		\midrule
		12 && 2 && 4365 && 61342 && 12503 (12719) && 27 && 0.031 && 0.74 \\
		&& 4 && 14381 && 355084 && 12503 (12719) && 27 && 2.6 && 4.8 \\
		&& 6 && 35397 && 1056826 && N/A (12719) && 27 && time-out && time-out \\
		&& 8 && 108609 && 3655032 && N/A (12719) && 27 && time-out && time-out \\
		\bottomrule
	\end{tabular*}
	\caption{Results of applying synthesis with maximum realizability on the instances in Table~\ref{tab:def-inst}, with different bounds on implementation size $|\trans|$. We report on the number of variables and clauses in the encoding, the value (and bound) of the objective function in the MaxSAT instance,  the running times of Spot and Open-WBO, and the time of the solver plus the time for generating the encoding.}
	\label{tab:inst-stat-1}
\end{table*}

\comment{
In large power networks, multiple generators act as power supplies that must provide power to numerous loads that represent the consumers. When continuously running, each of these components may become faulty which demands a network reconfiguration. The relays in the network perform such transitions between configurations. 

Here, we consider the problem of dynamic reconfiguration of a generic power distribution network. The system determines the configuration of the network through variables representing the relays' positions. Since the faults in the components are unpredictable, they can be represented by the environment. However, to ensure realizability of the problem, we restrict the number of faulty components. 

Let $\mathcal{P} = \{P_1, P_2, ..., P_m\}$ denote the set of power supplies and $\mathcal{L} = \{L_1, L_2, ..., L_n\}$ to denote the set of consumer components. Each power supply has limited power capacity, represented by $P^+_i$ while each load has a power demand, represented by $P^-_i$. Depending on the network architecture, each of the loads has access to a subset of power supplies, i.e., $A_L(L_i) \subseteq \mathcal{P}$ where $A_L(L_i)$ determines the power supplies that are accessible by load $L_i$. On the other hand, each power supply is accessible to a subset of loads. Let $A_P(P_i) \subseteq \mathcal{L}$ denote the load components that can connect to power supply $P_i$. Such architecture can be illustrated via a bipartite graph where the connectivity matrix defines set functions $A_L$ and $A_P$. 
Furthermore, some of the components are in the same subsystem whose operation requires all those loads to be powered. We capture this by introducing disjoint classes of loads $\mathcal{C} = \{C_1, C_2, ..., C_k\}$ where $C_i \subseteq \mathcal{L}$ and $C_i \cap C_j = \emptyset ,\; \forall i\neq j$. Additionally, the relative importance of subsystems imposes a set of weights that show the priorities of providing power to the loads. Let $w_1, w_2, ..., w_k$ to denote the weights associated with classes. If a subsystem must always be powered, its corresponding weight is set to $\infty$.

This framework allows us to model a generic power distribution network on an abstract level. For instance, the network shown in Fig.[-a] with 2 power supplies and 4 loads can be abstracted into the graph of Fig.[-b]. For such model, we aim to synthesis a planner that dynamically assigns the loads to healthy power supplies. The planner has to respect the connectivity structure of the network and should try to maximally power the subsystems. We cast this optimization according to the lexicographical ordering introduced in section [] and predefined weights over the soft constraints. 

We define a set of variables along a series of LTL constraints that model the problem and capture the desired requirements of the system. When the number of faulty generators upperbounded by $l$, the environment can be defined as $l$ integer variables $e_1, e_2, ..., e_l; \; e_i \in \{0, 1, ..., n\}$, where a non-zero assignment shows a faulty generator.\footnote{Two environment variables can be non-zero and have the same value. While this will be redundant, it does not affect the encoding.} The system variables are $s_{i \rightarrow j}$'s such that $s_{i \rightarrow j} = 1$ if load $i$ is assigned to power supply $j$ and $s_{i \rightarrow j} = 0$ otherwise. Note that not all the power supplies are available to a consumer, therefore, for the $i^{th}$ consumer, the range that $j$ varies over depends on the available suppliers for that load. 

A critical load must always be powered. This leads to hard constraint
\begin{equation}
\square \left( \bigvee_{j \in A_L(L_i)} s_{i \rightarrow j} \right) \,, 
\quad \forall \ i \in \{1, 2, ..., n\} \ s.t. \ w_i = \infty.
\end{equation}
A non-critical load being powered introduces a soft constraint, i.e.,
\begin{equation}
\square \left( \bigvee_{j \in A_L(L_i)} s_{i \rightarrow j} \right) \,, 
\quad \forall \ i \in \{1, 2, ..., n\} \ s.t. \ w_i < \infty,
\end{equation}
which if it is not realizable, we relax it according to the proposed lexicographical ordering. A load should only be assigned to one power supply:
\begin{equation}
\bigwedge_{i \in \{1, 2, ..., n\}}
\bigwedge_{j_1 \in A_L(L_i)}
\square \left(s_{i \rightarrow j_1} 
\rightarrow \bigwedge_{j_2 \in A_L(L_i), j_2 \neq j_1}\neg s_{i \rightarrow j_2}\right),
\end{equation}
or equivalently,
\begin{equation}
\square \left(\neg s_{i \rightarrow j_1} \lor \neg s_{i \rightarrow j_2}\right) \,,
\qquad \forall \ i \in \{1, 2, ..., n\}, \forall \ j_1, j_2 \in \{1, 2, ..., m\}, j_1 \neq j_2.
\end{equation}
Let the capacity of the power sources to be dependent on the number of loads that are attached to them, i.e., the power requirements of all load components are similar. Therefore, the constrained capacity of power supplies is expressed in the following constraint:
\begin{equation}
\bigwedge_{j \in \{1, 2, ..., m\}} 
\bigwedge_{\substack{{L \subseteq A_P(P_j)} \\ {|L| = P^+_j}}}
\square \left( \bigwedge_{i_1 \in L} s_{i_1 \rightarrow j} \rightarrow
\bigwedge_{i_2 \in A_P(P_j) \backslash L} \neg s_{i_2 \rightarrow j} \right).
\end{equation}
When a power supply becomes faulty, we require the loads to be disconnected from it:\footnote{Depending on the response time, one can add ``next'' operator to expect disconnection in future time steps.}
\begin{equation}
\bigwedge_{k \in \{1, 2, ..., l\}}
\bigwedge_{j \in \{1, 2, ..., m\}}
\square \left( e_k = j \rightarrow 
\bigwedge_{i \in A_P(P_j)} \neg s_{i \rightarrow j} \right).
\end{equation}

\begin{equation}
\bigwedge_{i \in \{1, 2, ..., n\}}
\bigwedge_{j \in A_L(L_i)}
\square \left( 
s_{i \rightarrow j} \land \LTLnext \left( \neg 
\bigvee_{k \in \{1, 2, ..., l\}} e_k = j \right)
\rightarrow \LTLnext s_{i \rightarrow j} \right) 
\end{equation}

\begin{equation}
\bigvee_{j \in A_L(L_i)} s_{i \rightarrow j} \land 
\LTLnext \left( \bigvee_{j \in A_L(L_i)} s_{i \rightarrow j} \right) 
\land \ldots \land
\LTLnext^{t_{init}} \left( \bigvee_{j \in A_L(L_i)} s_{i \rightarrow j} \right)
\,, \quad \forall \ i \in \mathcal{L}_{init}
\end{equation}
}
\subsubsection{Maximum Realizability with Soft LTL Specifications.}\label{sec:soft-ltl}
The first generalization of the maximum realizability problem that we consider is the setting where the soft specifications can be arbitrary LTL formulas, and not just safety properties of specific form. More precisely, each soft specification $\softSpec$ is an LTL formula for which we are also given a vector $\Relax(\softSpec)$ of LTL formulas that defines the possible relaxations of $\softSpec$. Formally, $\Relax(\softSpec) = (\psi_{0},\ldots,\psi_{m})$, where $\psi_{0} = \softSpec$, and for every $0 \leq k < m$ it holds that $\trans \models \psi_{k}$ implies $\trans \models \psi_{k+1}$ for every transition system $\trans$. That is, $\psi_{0},\ldots,\psi_{m}$ are ordered according to strength.
In particular, if $\trans \models \softSpec$, then $\trans \models \psi_k$ for each $\psi_k$ in $\Relax(\softSpec)$.
For example, if $\softSpec = \LTLglobally p$ for some atomic proposition $p$, we can take $\Relax(\softSpec) = (\LTLglobally p,\LTLfinally\LTLglobally p,\LTLglobally\LTLfinally p)$.

As in Section~\ref{sec:quantitative-semantics} we define the value of $\softSpec$ for given $\Relax(\softSpec) = (\psi_{0},\ldots,\psi_{m})$ to be $\val\trans\softSpec = (v_1,\ldots,v_m)$, where $v_k = 1$ if $\trans \models \psi_k$, and $v_k = 0$ otherwise.

For a conjunction $\softSpec_1\wedge\ldots\wedge\softSpec_n$ of soft specifications with given $\Relax(\softSpec_j) = (\psi_{j,0},\ldots,\psi_{j,m})$ for each $j \in \{1,\ldots,n\}$, we define the value
$\val\trans{\softSpec_1 \wedge \ldots \wedge \softSpec_n} = \big(
\sum_{i=1}^n v_{i,m},
\ldots,
\sum_{i=1}^n v_{i,0}
\big),$ where
$\val\trans{\softSpec_i} = (v_{i,0},\ldots,v_{i,m})$ for $i \in \{1,\ldots,n\}$.

The maximum realizability problem asks for given LTL specification $\spec$ and soft LTL specifications 
$\softSpec_1,\ldots,\softSpec_n$ with given $\Relax(\softSpec_j) = (\psi_{j,0},\ldots,\psi_{j,m})$, to determine whether there exists a transition system $\trans$ such that $\trans\models\spec$, and if the answer is positive, to construct a transition system $\trans^*$ such that $\trans^* \models \spec$, and for every $\trans$ with $\trans\models\spec$ it holds that $\val\trans{\softSpec_1 \wedge \ldots \wedge \softSpec_n} \leq \val{\trans^*}{\softSpec_1 \wedge \ldots \wedge \softSpec_n}$.
The bounded maximum realizability problem is defined in the obvious way.

We can adapt the MaxSAT approach from Section~\ref{sec:maxsat} to solve the bounded maximum realizability problem in this setting as follows. 

First, for each $\psi_{j,k}$ in $\Relax(\softSpec_j)$, we construct a universal co-B\"uchi automaton $\autA_{j,k} = (Q_{j,k},q_0^{j,k},\delta_{j,k},F_{j,k})$ such that $\trans \in \lang{\autA_{j,k}}$ if and only if $\trans \models \psi_{j,k}$.
In the MaxSAT encoding, the hard constraints for the annotation $\anot_{j,k}$  are
\begin{align*}
C_{j,k}\defeq\bigwedge_{q,q' \in Q_{j,k}}\bigwedge_{s,s' \in S}\bigwedge_{\inpval \in \ialphabet}
\Bigg( &
\big(
\anotbjk_{s,q} \wedge
\delta^{j,k}_{s,q,\inpval,q'}\wedge 
\tau_{s,\inpval,s'}
\big) \rightarrow 
\succa_{\anot}^{j,k}(s,q,s',q',\inpval)
\Bigg).
\end{align*}
Generalizing the encoding, for each $j \in \{1,\ldots,n\}$ and $k \in \{0,\ldots,m\}$ we now have one soft constraint
$\soft_{j,k}\defeq  \bigvee_{l=0}^k \anotbjl_{s_0,q^{j,l}}$ with weight $n^k$.

\smallskip
\noindent 
{\bf Maximum Realizability with Priorities.}
In the definitions in Section~\ref{sec:max-realizability} and the paragraph above, all soft specifications have the same priority. Now, we extend the maximum realizability setting with priorities for the soft specifications given as part of the input to the problem.

\smallskip
\noindent
{\it Soft specifications with priority ordering.} We begin with a simple setting where soft specifications are simply ordered in decreasing priority, without assigning any numerical weight for each formula's preference. More specifically, we assume that the soft specifications $\softSpec_1,\ldots,\softSpec_n$ are ordered such that, for every $i \in \{1,\ldots,n\}$, we have that $\softSpec_i$ has higher priority than $\softSpec_j$ for all $j > i$. 

Now, given a vector $\Relax(\softSpec_j) = (\psi_{j,0},\ldots,\psi_{j,m})$ for $\softSpec_j$  we define the value of $\softSpec_j$ in a transition system $\trans$ to be the number of specifications in $\Relax(\softSpec_j)$ satisfied by $\trans$, i.e., $\val\trans{\softSpec_j} = | \{k \in \{0,\ldots,m\} \mid \trans\models \psi_{j,k}\}|$. The value of $\softSpec_1\wedge\ldots\wedge\softSpec_n$ is then defined as $\val\trans{\softSpec_1 \wedge \ldots \wedge \softSpec_n} = (\val\trans{\softSpec_1},\ldots,\val\trans{\softSpec_n})$. The values of transition systems are compared according to the lexicographic ordering of vectors in $\{0,\ldots,m+1\}^n$, giving priority of $\softSpec_i$ over $\softSpec_j$ for $i < j$.

The MaxSAT approach can be adapted for this value function in the same way as above. The difference is in the weights of the soft constraints for the annotations $\anot_{j,k}$: for each
$j \in \{1,\ldots, n\}$ and $k \in \{1,\ldots,m\}$ we have a soft constraint  $\soft_{j,k} \; \defeq \;  \bigvee_{l=0}^k \anotbjl_{s_0,q^{j,l}}$ with weight $w_{j,k}$, where 
$w_{j,k} = 1 $ if $j=n$ or $k < m$, and $w_{j,k} = \sum_{j' = j+1}^n \sum_{k = 1}^m w_{j',k} + 1$ otherwise.

\smallskip
\noindent
{\it Soft specifications with given weights.}
We also consider the weighted maximum realizability problem, in which, together with $\Relax(\softSpec)$ for each soft specification $\softSpec$, the user also provides numerical weights for the formulas in $\Relax(\softSpec)$. That is, for each $j \in \{1,\ldots,n\}$ and $k \in \{1,\ldots,m\}$ we are given a weight $w_{j,k}$ for $\psi_{j,k}$. These weights specify the priority of each of the soft specifications.

The MaxSAT formulation is then adapted to incorporate the given weights, by using them for the corresponding soft constraints. Namely, for each $j$ and $k$, the corresponding soft constraint $\soft_{j,k}  \; \defeq \;  \bigvee_{l=0}^k \anotbjl_{s_0,q^{j,l}}$ has weight $w_{j,k}$.

\comment{
\begin{theorem}\label{thm:optimal-bound-general}
Given an LTL specification $\spec$ and a soft specification $\gphi_1 \wedge\ldots \wedge\gphi_n$ together with a vector of formulas $\Relax(\softSpec_j) = (\psi_{j,0},\ldots,\psi_{j,m})$ for each $\softSpec_j$,
if there is a transition system $\trans$ with  $\trans \models \spec$, then there exists $\trans^*$ such that:
\begin{itemize}
\item $\val\trans{\softSpec_1 \wedge \ldots \wedge \softSpec_n} \leq \val{\trans^*}{\softSpec_1 \wedge \ldots \wedge \softSpec_n}$ for all $\trans$ with $\trans \models \spec$,
\item $\trans^* \models \spec$ and $|\trans^*| \leq (2^{b+\log b})!^2$, where
\end{itemize}
$b = \max\{|\subf{\spec\wedge\softSpec_1'\wedge\ldots\wedge\softSpec_n'}| \mid \softSpec_i' \in \Relax(\softSpec_i) \text{ for }i=1,\ldots,n\}$.
\end{theorem}
}

\begin{appxthm}\label{thm:optimal-bound-general-appx}
Given an LTL specification $\spec$ and a soft specifications $\gphi_1,\ldots,\gphi_n$ together with a vector of formulas $\Relax(\softSpec_j) = (\psi_{j,0},\ldots,\psi_{j,m})$ for each $\softSpec_j$,
if there is a transition system $\trans$ with  $\trans \models \spec$, then there exists $\trans^*$ such that:
\begin{itemize}
\item $\val\trans{\softSpec_1 \wedge \ldots \wedge \softSpec_n} \leq \val{\trans^*}{\softSpec_1 \wedge \ldots \wedge \softSpec_n}$ for all $\trans$ with $\trans \models \spec$, and
\item $\trans^* \models \spec$ and $|\trans^*| \leq (2^{b+\log b})!^2$,
\end{itemize}
where $b = \max\{|\subf{\spec\wedge\softSpec_1'\wedge\ldots\wedge\softSpec_n'}| \mid \softSpec_i' \in \Relax(\softSpec_i) \text{ for }i=1,\ldots,n\}$.
\end{appxthm}
\begin{proof}
The proof is a generalization of the proof of Theorem~\ref{thm:optimal-bound-safety}. First, we need to establish the analogue of Lemma~\ref{lem:value-as-ltl} for the general case. 

\begin{appxlemma}\label{lem:value-as-ltl-general-appx}
For every transition system $\trans$, soft specifications $\gphi_1,\ldots,\gphi_n$, and vector of formulas $\Relax(\softSpec_j) = (\psi_{j,0},\ldots,\psi_{j,m})$ for each $\softSpec_j$, if $\val\trans{\gphi_1 \wedge \ldots \wedge \gphi_n} = v$, then there exists an LTL formula $\psi_v$ such that $\trans \models \psi_v$ and the following hold:
\begin{itemize}
\item[(1)] $\psi_v = \softSpec_1'\wedge\ldots\wedge\softSpec_n'$, where $\softSpec_i' \in\Relax(\softSpec_i)  \text{ for }i=1,\ldots,n$, 
\item[(2)] for every $\trans'$, if $\trans' \models \psi_v$, then $\val{\trans'}{\gphi_1 \wedge \ldots \wedge \gphi_n} \geq v$.
\end{itemize}
\end{appxlemma}
The proof of Lemma~\ref{lem:value-as-ltl-general-appx} is analogous to the proof of Lemma~\ref{lem:value-as-ltl-appx}. Then, with the help of Lemma~\ref{lem:value-as-ltl-general-appx} we can establish the theorem in the same way as Theorem~\ref{thm:optimal-bound-safety}. \qed
\end{proof}


\section{Introduction}\label{sec:intro}
\input{intro.tex}

\section{Maximum Realizability Problem}\label{sec:problem}
\input{problem.tex}



\section{Preliminaries}
\input{prelim.tex}


\section{From Maximum Realizability to MaxSAT}\label{sec:maxsat-encoding}
\input{maxsat.tex}


\section{Experimental Evaluation}\label{sec:experiments}
\input{experiments.tex}


\newpage
\bibliographystyle{plain}

\subsection{Bounded Maximum Realizability}
To establish an upper bound on the minimal (in terms of size) optimal implementation, we make use of an important property of the function $\mathit{val}$ defined in Section~\ref{sec:quantitative-semantics}. Namely, the property that for each of the possible values of $\gphi_1 \wedge\ldots \wedge\gphi_n$  there is a corresponding LTL formula that encodes this value in the classical LTL semantics, as we formally state in the next lemma.

\begin{lemma}\label{lem:value-as-ltl}
For every transition system $\trans$ and soft safety specifications $\gphi_1,\ldots,$ $\gphi_n$, if $\val\trans{\gphi_1 \wedge \ldots \wedge \gphi_n} = v$, then there exists an LTL formula $\psi_v$ such that $\trans \models \psi_v$ and the following conditions hold
\begin{itemize}
\item[(1)] $\psi_v = \softSpec_1'\wedge\ldots\wedge\softSpec_n'$, where $\softSpec_i' \in\{\gphi_i,\fgphi_i,\gfphi_i,\true\} \text{ for }i=1,\ldots,n$, 
\item[(2)] for every $\trans'$, if $\trans' \models \psi_v$, then $\val{\trans'}{\gphi_1 \wedge \ldots \wedge \gphi_n} \geq v$.
\end{itemize}
\end{lemma}

The following theorem is a consequence of Lemma~\ref{lem:value-as-ltl}. 
\begin{theorem}\label{thm:optimal-bound-safety}
Given an LTL specification $\spec$ and soft safety specifications $\gphi_1,\ldots,$ $\gphi_n$,  
if there exists a transition system $\trans \models \spec$, then there exists  $\trans^*$ such that
\begin{itemize}
\item [(1)] $\val\trans{\gphi_1 \wedge \ldots \wedge \gphi_n} \leq \val{\trans^*}{\gphi_1 \wedge \ldots \wedge \gphi_n}$ for all $\trans$ with $\trans \models \spec$,
\item[(2)] $\trans^* \models \spec$ and $|\trans^*| \leq \left((2^{(b+\log b)})!\right)^2$,
\end{itemize}
 where $b = \max\{|\subf{\spec\wedge\softSpec_1'\wedge\ldots\wedge\softSpec_n'}| \mid \forall i:\ \softSpec_i' \in\{\gphi_i,\fgphi_i,\gfphi_i\}\}$.
\end{theorem}

The bound above is estimated based on the size of the specifications, using a worst-case bound on the size of the corresponding automata. Given automata for all the specifications $\gphi_i,\fgphi_i$ and $\gfphi_i$, a potentially better bound can be estimated based on the size of these automata.

Lemma~\ref{lem:value-as-ltl} immediately provides a naive synthesis procedure, which searches for an optimal implementation by enumerating possible $\psi_v$ formulas and solving the corresponding realizability questions. The total number of these formulas is $4^n$, where $n$ is the number of soft specifications. The approach that we propose avoids this rapid growth, by reducing the optimization problem to a single MaxSAT instance, and thus it also makes use of  the power of MaxSAT solvers.

\subsection{Automata and Annotations for Soft Safety Specifications}\label{sec:automata-safety}
Let $\gphi$ be an LTL formula, where $\varphi$ is a syntactically safe LTL formula.

The first step in the MaxSAT reduction is the construction of a universal B\"uchi automaton for each soft safety specification $\gphi$ and its modification to incorporate the relaxation of $\gphi$ to $\fgphi$, as we now describe.

\begin{proposition}\label{prop:aut-globally}
Given an LTL formula $\gphi$ where $\varphi$ is syntactically safe, we can construct a universal B\"uchi automaton  $\autB_{\scriptsize \gphi} = (Q_{\scriptsize \gphi},q_0^{\scriptsize \gphi},\delta_{\scriptsize \gphi},F_{\scriptsize \gphi})$ such that 
 $\lang{\autB_{\scriptsize \gphi}} = \{\trans \mid \trans \models \gphi\}$, and $\autB_{\scriptsize \gphi}$ has a unique non-accepting sink state, that is, there exists a unique state $\rej_\varphi \in Q_{\scriptsize \gphi}$ such that 
$F_{\scriptsize \gphi} = Q_{\scriptsize \gphi} \setminus \{\rej_\varphi\}$, and for every $\sigma \in \Sigma$ it holds that $\{q \in Q_{\scriptsize \gphi} \mid (\rej_\varphi,\sigma,q) \in \delta_{\scriptsize \gphi}\}  = \{\rej_\varphi\}$.
\end{proposition}

From $\autB_{\scriptsize \gphi}$, which has at most $2^{\mathcal{O}(|\varphi|)}$ states, we obtain a universal automaton $\relaxfg(\gphi)$ constructed by redirecting all the transitions leading  to $\rej_\varphi$ to the initial state $q_0^{\scriptsize \gphi}$. Formally, 
$\relaxfg(\gphi) = (Q,q_0,\delta,F)$, where $Q = Q_{\scriptsize \gphi} \setminus \{\rej_\varphi\}$, $q_0 = q_0^{\scriptsize \gphi}$, $F = F_{\scriptsize \gphi}$ and the transition relation is defined as
\[\delta = \left(\delta_{\scriptsize \gphi} \setminus \{(q,\sigma,q') \in \delta_{\scriptsize \gphi}\mid q' = \rej_\varphi\}\right) \cup \{(q,\sigma,q_0) \mid (q,\sigma,\rej_\varphi)\in \delta_{\scriptsize \gphi}\}.\]

\noindent
Let $\Rej(\relaxfg(\gphi)) = \{(q,\sigma,q_0) \in \delta \mid (q,\sigma,\rej_\varphi) \in \delta_{\scriptsize \gphi}\}$ be the set of transitions in $\relaxfg(\gphi)$ that correspond to transitions in $\autB_{\scriptsize \gphi}$ leading to $\rej_\varphi$. 

The next proposition formalizes the property that a transition system $\trans$ is accepted by $\autB_{\scriptsize \gphi}$ iff the run graph of $\relaxfg(\gphi)$ on $\trans$ does not contain an edge corresponding to a transition in $\Rej(\relaxfg(\gphi))$. 
\begin{proposition}\label{prop:rej-trans}
Let $\trans$ be a transition system and let $G = (V,E)$ be the run graph of $\relaxfg(\gphi)$ on $\trans$. Then, $\trans \in\lang{\autB_{\scriptsize \gphi}}$ iff for every  $((s,q),\sigma,(s',q')) \in E$ with $(q,\sigma,q') \in  \Rej(\relaxfg(\gphi))$, $(s,q)$ is not reachable from $(s_0,q_0)$ in $G$.
\end{proposition}

We define an annotation function $\anotfg : S \times Q \to \natsbot$ for a transition system $\trans = (S,s_0,\tau)$ and the automaton $\relaxfg(\gphi) = (Q,q_0,\delta,F)$. The value of $\anotfg$ for the initial node of the run graph determines whether $\trans$ satisfies $\gphi$ or $\fgphi$.
A function $\anotfg : S \times Q \to \natsbot$ is \emph{\fgvalid}\ annotation if it is such that
\begin{itemize}
\item[\emph{(1)}] $\anotfg(s_0,q_0) \neq \bot$, i.e., the pair of initial states is labelled with a number, and 
\item[\emph{(2)}] if $\anotfg(s,q) \neq \bot$, then for every edge $((s,q),\sigma,(s',q'))$ in the run graph of $\relaxfg(\gphi)$ on $\trans$ we have that $\anotfg(s',q') \neq \bot$, and
\begin{itemize}
\item if $(q,\sigma,q') \in\Rej(\relaxfg(\gphi))$, then $\anotfg(s',q') >  \anotfg(s,q)$, and 
\item if $(q,\sigma,q') \not\in\Rej(\relaxfg(\gphi))$, then $\anotfg(s',q') \geq  \anotfg(s,q)$.
\end{itemize}
\end{itemize}

This definition  guarantees that if $\anotfg$ is a bounded \fgvalid\ annotation for $\trans$ and $\relaxfg(\gphi)$, then the number of rejecting edges in each path in the run graph of $\relaxfg(\gphi)$ on $\trans$ is finite, which implies $\trans \models \fgphi$ as stated below.\looseness=-1

\begin{proposition}\label{prop:anotfg}
Let $\trans = (S,s_0,\tau)$ be a finite-state transition system, and $G = (V,E)$ be the run graph of  $\relaxfg(\gphi)$ on $\trans$. Then, $\trans \models \fgphi$ if and only if there exists a \fgvalid\ $|\trans|$-bounded annotation for $\trans$ and $\relaxfg(\gphi)$. 
\end{proposition}

If the run graph of $\relaxfg(\gphi)$ on $\trans$ contains a reachable edge which belongs to $\relaxfg(\gphi)$, then we can conclude that $\trans\not\models\gphi$. However, if each infinite path in the run graph contains only a finite number of occurrences of edges in $\relaxfg(\gphi)$, then $\trans\models\fgphi$. In particular, we have that if $\anotfg(s_0,q_0) \in \nats$, then $\trans \models \fgphi$, and if $\anotfg$ is $c$-bounded and $\anotfg(s_0,q_0) = c$, then $\trans \models \gphi$.

This property of $\anotfg$ allows us to capture the satisfaction of $\gphi$ and of $\fgphi$ with soft clauses for the same annotation function in the MaxSAT formulation.

\subsection{MaxSAT Encoding of Bounded Maximum Realizability}\label{sec:maxsat}

Let $\autA = (Q,q_0,\delta,F)$ be a universal co-B\"uchi automaton for the LTL formula $\spec$.

For each syntactically safe formula $\gphij$, $j \in\{1,\ldots,n\}$, we consider two universal automata:
the universal automaton $\autB_j = \relaxfg(\gphi_j)= (Q_j,q_0^j,\delta_j,F_j)$ constructed as described in Section~\ref{sec:automata-safety} and 
a universal co-B\"uchi automaton $\autA_j = (\widehat Q_j,\widehat q_0^j,\widehat\delta_j,\widehat F_j)$ for the formula $\gfphi_j$. 
Given a bound $b$ on the size of the sought transition system, we encode the bounded maximum realizability problem as a MaxSAT problem with the following sets of variables and constraints.

{\bf Variables:} The MaxSAT formulation includes the variables from the SAT formulation of the bounded synthesis problem, which represent the sought transition system $\trans$ and the sought valid annotation of the run graph of $\autA$ on $\trans$. Additionally, it includes variables for representing the annotations $\anotfg_j$ and $\anot_j$ for $\autB_j$ and $\autA_j$ respectively, similarly to $\anot$ in the SAT encoding. More precisely, the annotations for $\anotfg_j$ and $\anot_j$ are represented respectively by variables $\anotfgbj_{s,q}$ and $\anotfgnj_{s,q}$  where $s\in S$ and $q \in Q_j$, and $\anotbj_{s,q}$ and $\anotnj_{s,q}$ where $s\in S$ and $q \in \widehat Q_j$.

The set of constraints includes $C_\tau$ and $C_\anot$ from the SAT formulation as hard constraints, as well as the following constraints for the new annotations.

{\bf Hard constraints for valid annotations:}
For each $j=1,\ldots,n$, let
\begin{align*}
C_\anotfg^{j}\defeq\bigwedge_{q,q' \in Q_j}\bigwedge_{s,s' \in S}\bigwedge_{\inpval \in \ialphabet}
\Big( &
\big(
\anotfgbj_{s,q} \wedge
\delta^j_{s,q,\inpval,q'}\wedge 
\tau_{s,\inpval,s'}
\big) \rightarrow 
\succa_{\anotfg}^j(s,q,s',q',\inpval) 
\Big),
\\
C_\anot^{j}\defeq\bigwedge_{q,q' \in \widehat Q_j}\bigwedge_{s,s' \in S}\bigwedge_{\inpval \in \ialphabet}
\Big( &
\big(
\anotbj_{s,q} \wedge
\widehat\delta^j_{s,q,\inpval,q'}\wedge 
\tau_{s,\inpval,s'}
\big) \rightarrow 
\succa_{\anot}^j(s,q,s',q',\inpval)
\Big),
\end{align*}
\begin{align*}
\text{where }\succa_\anotfg^j(s,q,s',q',\inpval) \defeq \anotfgbj_{s',q'} \wedge &
\big(\rej^j(s,q,q',\inpval) \rightarrow \anotfgnj_{s',q'} > \anotfgnj_{s,q}\big) \wedge
\\&
\big(\neg\rej^j(s,q,q',\inpval) \rightarrow \anotfgnj_{s',q'} \geq \anotfgnj_{s,q}\big)
,
 \end{align*}
and $\rej^j(s,q,q',\inpval)$ is a formula over $o_{s,\inpval}$ obtained from $\Rej(\autB_j)$.
The formula $\succa_{\anot}^j(s,\widehat q,s',\widehat q',\inpval)$ is analogous to 
$\succa_{\anot}(s,q,s',q',\inpval)$ defined in Section~\ref{sec:bounded-synthesis}.

{\bf Soft constraints for valid annotations:}
For each $j=1,\ldots,n$ we define
\[
\begin{array}{lllll}
\soft_{\tiny\LTLglobally}^{j} & \quad \defeq \quad &  \anotfgb_{s_0,q_0^j} \wedge (\anotfgn_{s_0,q_0^j} = b) & \qquad & \text{with weight }1,\\
\soft_{\tiny\LTLfinally\LTLglobally}^{j} & \quad \defeq \quad & \anotfgb_{s_0,q_0^j} & \quad & \text{with weight }n, \text{ and }\\
\soft_{\tiny\LTLglobally\LTLfinally}^{j} & \quad \defeq \quad & \anotfgb_{s_0,q_0^j} \vee \anotb_{s_0,\widehat  q_0^j} & \quad & \text{with weight }n^2,\\
\end{array}
\]
where $b \in \nats$ is the bound on the size of the transition system.

The definition of the soft constraints guarantees that $\trans \models \gphi_j$ if and only if there exist corresponding annotations that satisfy all three of the soft constraints for $\gphi_j$. Similarly, if $\trans \models \fgphi_j$, then $\soft_{\tiny\LTLfinally\LTLglobally}^{j}$ and $\soft_{\tiny\LTLglobally\LTLfinally}^{j}$ can be satisfied.

The weights are selected in a way that reflects the ordering of transition systems with respect to their satisfaction of $\gphi_1 \wedge \ldots \wedge \gphi_n$, as stated below.

\begin{lemma}\label{lem:encoding-weights}
Let $\trans'$ and $\trans''$ be transition systems such that $\trans' \models \spec$ and $\trans'' \models \spec$. Let $a'$ and $a''$ be variable assignments satisfying the constraint system, such that $a'$ is an optimal assignment consistent with $\trans'$, and $a''$ is an optimal assignment consistent with $\trans''$. Furthermore, let $w'$ and $w''$ be the sums of the weights of the soft clauses satisfied in $a'$ and $a''$ respectively. Then, it holds that
$\val{\trans'}{\gphi_1 \wedge \ldots \wedge \gphi_n} < \val{\trans''}{\gphi_1 \wedge \ldots \wedge \gphi_n} \text{ iff } w' < w''.$
\end{lemma}

The next results establish the size and correctness of the encoding.

\begin{theorem}\label{thm:encoding-correctness}
Let $\autA$ be a given co-B\"uchi automaton for $\varphi$, and for each $j \in \{1,\ldots,n\}$, let $\autB_j = \relaxfg(\gphi_j)$ be the universal automaton for $\gphi_j$ constructed as in Section~\ref{sec:automata-safety}, and let $\autA_j$ be a universal co-B\"uchi automaton for $\gfphi_j$. 
The constraint system for bound $b \in \nats$ is satisfiable if and only if there exists an implementation $\trans$ with $|\trans| \leq b$  such that $\trans \models \varphi$. Furthermore, from the optimal satisfying assignment to the variables $\tau_{s,\inpval,s'}$ and $o_{s,\inpval}$, one can extract a transition system $\trans^*$ such that for every transition system $\trans$ with $|\trans| \leq b$ and $\trans \models \varphi$ it holds that $\val\trans{\gphi_1 \wedge \ldots \wedge \gphi_n} \leq \val{\trans^*}{\gphi_1 \wedge \ldots \wedge \gphi_n}$.
\end{theorem}

\begin{proposition}\label{prop:encoding-size}
Let $\autA$ be a given co-B\"uchi automaton for $\varphi$, and for each $j \in \{1,\ldots,n\}$, let $\autB_j = \relaxfg(\gphi_j)$ be the universal B\"uchi automaton for $\gphi_j$ constructed as in Section~\ref{sec:automata-safety}, and let $\autA_j$ be a universal co-B\"uchi automaton for $\gfphi$. 
The constraint system for bound $b \in \nats$ has weights in $\mathcal{O}(n^2)$,
\[
\begin{array}{l}
\mathcal{O}\Big(
(b^2 + b \cdot |\outv|)\cdot 2^{|\inpv|} +  
b \cdot |Q|\cdot (1+ \log(b \cdot |Q|)) +\\ 
\phantom{\mathcal{O}(}\sum_{j=1}^n\big(b \cdot |Q_j| (1 + \log(b\cdot |Q_j|))\big)
+ \sum_{j=1}^n\big(b \cdot |\widehat Q_j| (1 + \log(b\cdot |\widehat Q_j|))\big)
\Big)
\end{array}\]
variables, and its size (before conversion to CNF) is
\[
\begin{array}{l}
\mathcal{O}\Big(
|Q|^2 \cdot b^2 \cdot 2^{|\inpv|} \cdot (d + \log(b\cdot |Q|)) + \\
\phantom{\mathcal{O}(}\sum_{j=1}^n\big(|Q_j|^2 \cdot b^2 \cdot 2^{|\inpv|} \cdot (d_j + r_j + \log(b\cdot |Q_j|))\big) +
\\
\phantom{\mathcal{O}(}\sum_{j=1}^n\big(|\widehat Q_j|^2 \cdot b^2 \cdot 2^{|\inpv|} \cdot (\widehat d_j + \log(b\cdot |\widehat Q_j|))\big)
\Big), 
\end{array}\]
\[
\begin{array}{lllllll}
\text{ where} &d &=& \max_{s,q,\inpval,q'}|\delta_{s,q,\inpval,q'}|,&
d_j &=& \max_{s,q,\inpval,q'}|\delta_{s,q,\inpval,q'}^j|,\\
&\widehat d_j &=& \max_{s,q,\inpval,q'}|\widehat \delta_{s,q,\inpval,q'}^j|, \text{ and } &
r_j &=& \max_{s,q,\inpval,q'}|\rej^j(s,q,q',\inpval)|.
\end{array}
\]
\end{proposition}
\subsection{Bounded Synthesis}\label{sec:bounded-synthesis}

A \emph{B\"uchi automaton} over a finite alphabet $\alphabet$ is a tuple $\autA = (Q,q_0,\delta,F)$, where $Q$ is a finite set of states, $q_0$ is the initial state, $\delta \subseteq Q \times \alphabet \times Q$ is the transition relation, and $F \subseteq Q$ is a subset of the set of states. A run of $\autA$ on an infinite word $w=\sigma_0\sigma_1\ldots \in \alphabet^\omega$ is an infinite sequence $q_0,q_1,\ldots$ of states, where $q_0$ is the initial state and for every $i \geq 0$ it holds that $(q_i,\sigma_i,q_{i+1}) \in \delta$. 

A run of a B\"uchi automaton is accepting if it contains infinitely many occurrences of states in $F$. A \emph{co-B\"uchi automaton} $\autA = (Q,q_0,\delta,F)$ differs from a B\"uchi automaton in the accepting condition: a run of a co-B\"uchi automaton is accepting if it contains only \emph{finitely many} occurrences of states in $F$. For a B\"uchi automaton the states in $F$ are called \emph{accepting states}, while for a co-B\"uchi automaton they are called \emph{rejecting states}.
A \emph{nondeterministic} automaton $\autA$ accepts a word $w \in \alphabet^\omega$ if \emph{some} run of $\autA$ on $w$ is accepting.
A \emph{universal} automaton $\autA$ accepts a word $w \in \alphabet^\omega$ if \emph{every} run of $\autA$ on $w$ is accepting.

The \emph{run graph} of a universal automaton $\autA = (Q,q_0,\delta,F)$ on a transition system $\trans = (S,s_0,\tau)$ is the unique graph $G = (V,E)$ with set of nodes $V = S \times Q$ and set of labelled edges $E \subseteq V \times \alphabet \times V$ such that $((s,q),\sigma,(s',q')) \in E$ iff $(q,\sigma,q') \in \delta$ and $\tau(s,\sigma\cap \inpv) = (s',\sigma\cap \outv)$.
That is, $G$ is the product of $\autA$ and $\trans$.

A run graph of a universal B\"uchi (resp.\ co-B\"uchi) automaton is accepting if every infinite path $(s_0,q_0),(s_1,q_1), \ldots$ contains infinitely many (resp. finitely) many occurrences of states $q_i$ in $F$. A transition system $\trans$ is accepted by a universal automaton $\autA$ if the unique run graph of $\autA$ on $\trans$ is accepting. We denote with  $\lang\autA$ the set of transition systems accepted by $\autA$.

The bounded synthesis approach is based on the following property.
\begin{lemma}[\cite{KupfermanV05}]\label{lem:ltl-ucba}
For every LTL formula $\varphi$ we can construct a universal co-B\"uchi automaton $\autA_\varphi$ that has at most $2^{O(|\varphi|)}$ states and is such that for every transition system $\trans$ it holds that $\trans \in \lang{\autA_\varphi}$ if and only if $\trans \models \varphi$.
\end{lemma}

An \emph{annotation} of a transition system $\trans = (S,s_0,\tau)$  with respect to a universal co-B\"uchi automaton $\autA = (Q,q_0,\delta,F)$ is a function $\anot : S \times Q \to \natsbot$ that maps nodes of the run graph of $\autA$ on $\trans$ to the set $\natsbot$. Intuitively, such an annotation is valid if every node $(s,q)$ that is reachable from the node $(s_0,q_0)$ is annotated with a natural number, which is an upper bound on the number of rejecting states on any path from $(s_0,q_0)$ to $(s,q)$. 

Formally, an annotation $\anot : S \times Q \to \natsbot$ is \emph{valid} if
\begin{itemize}
\item $\anot(s_0,q_0) \neq \bot$, i.e., the pair of initial states is labelled with a number, and 
\item whenever $\anot(s,q) \neq \bot$, then for every edge $((s,q),\sigma,(s',q'))$ in the run graph of $\autA$ on $\trans$ we have that $(s',q')$ is annotated with a number (i.e., $\anot(s',q')\neq \bot$), such that
$\anot(s',q') \geq  \anot(s,q)$, and if $q' \in F$, then $\anot(s',q') >  \anot(s,q)$.
\end{itemize}

Valid annotations of finite-state systems correspond to accepting run graphs. An annotation $\anot$ is $c$-bounded if $\anot(s,q) \in \{0,\ldots,c\}\cup\{\bot\}$ for all $s \in S$ and $q \in Q$.\looseness=-1

The synthesis method proposed in \cite{ScheweF07a,FinkbeinerS13} employs the following result in order to 
reduce the bounded synthesis problem to checking the satisfiability of propositional formulas. A transition system $\trans$ is accepted by a universal co-B\"uchi automaton $\autA = (Q,q_0,\delta,F)$ iff there exists a $(|\trans|\cdot|F|)$-bounded valid annotation for $\trans$ and $\autA$. One can estimate a bound on the size of the transition system, which allows to reduce the synthesis problem to its bounded version. Namely, if there exists a transition system that satisfies an LTL formula $\varphi$, then there exists a transition system  satisfying $\varphi$ with  at most $\big(2^{(|\subf\varphi| +\log |\varphi|)}\big)!^2$ states.
\looseness=-1

Let $\autA = (Q,q_0,\delta,F)$ be a universal co-B\"uchi automaton for the LTL formula $\spec$.
Given a bound $b$ on the size of the sought transition system $\trans$, the bounded synthesis problem can be encoded as a satisfiability problem with the following sets of propositional variables and constraints.

{\bf Variables:} The variables represent the sought transition system $\trans$, and the sought valid annotation $\anot$ of the  run graph of $\autA$ on $\trans$. A transition system with $b$ states $S = \{1,\ldots,b\}$ is represented by  Boolean variables $\tau_{s,\inpval,s'}$ and $o_{s,\inpval}$ for every $s, s' \in S$, $\inpval \in \ialphabet$, and output proposition $o \in \outv$. The variable $\tau_{s,\inpval,s'}$ encodes the existence of transition from $s$ to $s'$ on input $\inpval$, and the variable $o_{s,\inpval}$ encodes $o$ being true in the output from state $s$ on input $\inpval$.

The annotation $\anot$ is  represented by the following variables. For each $s\in S$ and $q \in Q$, the annotation is represented by a Boolean variable $\anotb_{s,q}$ and a vector $\anotn_{s,q}$ of $\log(b\cdot |F|)$ Boolean variables: the variable $\anotb_{s,q}$ encodes the reachability of $(s,q)$ from the initial node in the corresponding run graph, and the vector of variables $\anotn_{s,q}$ represents the bound for the node $(s,q)$. 

{\bf Constraints for input-enabled $\trans$}:
$C_\tau \defeq\bigwedge_{s \in S}\bigwedge_{\inpval \in \ialphabet}\bigvee_{s' \in S} \tau_{s,\inpval,s'}$.

{\bf Constraints for valid annotation:}\\
$
\begin{array}{lll}
C_\anot & \defeq & 
\anotb_{s_0,q_0} \wedge\\&& 
\bigwedge_{q,q' \in Q}\bigwedge_{s,s' \in S}\bigwedge_{\inpval \in \ialphabet}
\Big( 
\big(
\anotb_{s,q} \wedge 
\delta_{s,q,\inpval,q'} \wedge 
\tau_{s,\inpval,s'}
\big) \rightarrow 
\succa_\anot(s,q,s',q')
\Big),
\end{array}
$\\
where $\delta_{s,q,\inpval,q'}$ is a formula over the variables $o_{s,\inpval}$ that characterizes the transitions in $\autA$ between  $q$ and $q'$ on labels consistent with $\inpval$, and
$\succa_\anot(s,q,s',q')$ is a formula  over the annotation variables such that
$\succa_\anot(s,q,s',q') \defeq (\anotb_{s',q'} \wedge (\anotn_{s',q'} > \anotn_{s,q}))$ if $q' \in F$, and
$\succa_\anot(s,q,s',q') \defeq (\anotb_{s',q'} \wedge (\anotn_{s',q'} \geq \anotn_{s,q}))$ if $q' \not\in F$.

\subsection{Maximum Satisfiability (MaxSAT)}\label{sec:prelim-maxsat}
While the bounded synthesis problem can be encoded into SAT, for the synthesis of a transition system that satisfies a set of soft specifications as well as possible, we need to solve an optimization problem. In the next section we will reduce the bounded maximum realizability problem to a \emph{partial weighted MaxSAT problem}.

\emph{MaxSAT} is a Boolean optimization problem. Similarly to SAT, instances of MaxSAT are given as propositional formulas in conjunctive normal form (CNF). That is, a MaxSAT instance is a conjunction of clauses, each of which is a disjunction of literals, where a literal is a Boolean variable or its negation. The objective in MaxSAT is to compute a variable assignment that maximizes the number of satisfied clauses. In \emph{weighted MaxSAT}, each clause is associated with a positive numerical weight and the objective is now to maximize the sum of the weights of the satisfied clauses. Finally, in \emph{partial weighted MaxSAT}, there are two types of clauses, namely \emph{hard} and \emph{soft} clauses, where only the soft clauses are associated with weights. In order to be a solution to a partial weighted MaxSAT formula, a variable assignment must satisfy all the hard clauses. An optimal solution additionally maximizes the sum of the weights of the soft clauses.
 
In the encoding in the next section we use hard clauses for the hard specification, and soft clauses to capture the soft specifications in the maximum realizability problem. The weights for the soft clauses  will encode the lexicographic ordering  on values of conjunctions of soft specifications. 
\subsection{Specifications, Transition Systems, and the Synthesis Problem}\label{sec:basic-definitions}


Linear-time temporal logic (LTL) is a standard specification language for formalizing requirements on the behaviour of reactive systems. Given a finite set $\props$ of atomic propositions, the set of LTL formulas is generated by the grammar
$\varphi := p \mid \true \mid \false \mid \neg \varphi \mid \varphi_1 \wedge \varphi_2 \mid \varphi_1 \vee \varphi_2 \mid \LTLnext  \varphi  \mid \varphi_1 \LTLuntil \varphi_2 \mid \varphi_1 \LTLrelease \varphi_2,$
where $p \in \props$  is an atomic proposition, $\LTLnext$ is the \emph{next} operator, $\LTLuntil$ is the \emph{until} operator, and $\LTLrelease$ is the \emph{release} operator. As usual, we  define the derived operators 
\emph{finally}: $\LTLfinally \varphi = \true \LTLuntil \varphi$ and 
\emph{globally}: $\LTLglobally \varphi = \false \LTLrelease \varphi$. An LTL formula $\varphi$ is in negation normal form (NNF) if all the negations appear only in front of atomic propositions. Since every LTL formula can be converted to an equivalent one in NNF, we consider only formulas in NNF.
A \emph{syntactically safe} LTL formula is an LTL formula which contains no occurrences of the $\LTLuntil$ operator in its NNF. 

Let $\Sigma = 2^{\props}$ be the finite alphabet consisting of the valuations of the propositions $\props$. A letter $\sigma \in \Sigma$ is interpreted as the valuation that assigns value $\trueval$ to all $p \in \sigma$ and $\falseval$ to all $p \in \props \setminus \sigma$. LTL formulas are interpreted over infinite words $w \in\alphabet^\omega$. If a word $w \in \alphabet^\omega$ satisfies an LTL formula $\varphi$, we write $w \models \varphi$. The definition of the semantics of LTL can be found for instance in~\cite{BaierKatoen08}. 
We denote with $|\varphi|$ the length of $\varphi$, and with $\subf\varphi$ the set of its subformulas.

In the rest of the paper we assume that the set $\props$ of atomic propositions is partitioned into disjoint sets of \emph{input} propositions $\inpv$ and \emph{output} propositions $\outv$.

A \emph{transition system} over a set of input propositions $\inpv$ and a set of output propositions $\outv$ is a tuple $\trans = (S,s_0,\tau)$, where $S$ is a set of states, $s_0$ is the initial state, and the transition function $\tau : S \times \ialphabet \to S \times \oalphabet$ maps a state $s$ and a valuation $\inpval \in \ialphabet$ of the input propositions  to a successor state $s'$ and a valuation $\outval \in \oalphabet$ to the output propositions. 
Let $\props = \inpv \cup \outv$ be the set of all propositions. For $\sigma \in \Sigma = 2^{\props}$ we denote $\sigma \cap \inpv$ by $\inpval$, and $\sigma \cap \outv$ by $\outval$.

If the set $S$ is finite, then $\trans$ is a finite-state transition system. In this case we define the size $|\trans|$ of $\trans$ to be the number of its states, i.e.,  $|\trans| \defeq |S|$.

An \emph{execution} of $\trans$ is an infinite sequence $s_0, (\inpval_0 \cup \outval_0), s_1, (\inpval_1 \cup \outval_1), s_2\ldots$ such that $s_0$ is the initial state, and $(s_{i+1},\outval_i) = \tau(s_i,\inpval_i)$ for every $i \geq 0$. The corresponding sequence $(\inpval_0 \cup \outval_0),(\inpval_1 \cup \outval_1),\ldots \in \alphabet^\omega$ is called a trace. We denote with $\Traces(\trans)$ the set of all traces of a transition system $\trans$. 

We say that a transition system $\trans$ satisfies an LTL formula $\varphi$ over atomic propositions $\props = \inpv \cup \outv$, denoted $\trans \models \varphi$, if $w \models \varphi$ for every $w \in \Traces(\trans)$.

The \emph{realizability problem for LTL} is to determine whether for a given LTL formula $\varphi$ there exists a transition system $\trans$ that satisfies $\varphi$. The \emph{LTL synthesis problem} asks to construct such a transition system if one exists.

Often, the specification  is a combination of multiple requirements,  which might not be realizable in conjunction. In such a case, in addition to reporting the unrealizability to the system designer, we would like the synthesis procedure to construct an implementation that satisfies the specification ``as much as possible''. Such implementation is particularly useful in the case where some of the requirements  describe desirable but not necessarily essential properties of the system. To determine what ``as much as possible'' formally means, a quantitative semantics of the specification language is necessary. In the next subsection we provide such semantics for a fragment of LTL. The quantitative interpretation is based on the semantics of LTL formulas of the form $\gphi$.

\subsection{Quantitative Semantics of Soft Safety Specifications}\label{sec:quantitative-semantics}
Let $\gphi_1,\ldots,\gphi_n$ be LTL specifications, where each $\softSpec_i$ is a syntactically safe LTL formula. In order to formalize the maximal satisfaction of $\gphi_1\wedge\ldots\wedge\gphi_n$, we first give a quantitative semantics of formulas of the form $\gphi$.

\vspace{-.3cm}
\paragraph{Quantitative semantics of safety specifications.} 
For an LTL formula of the form $\gphi$ and a transition system $\trans$, we define \emph{the value $\val\trans{\gphi}$ of $\gphi$ in $\trans$} as
\[
\val\trans\gphi \defeq
\begin{cases}
(1,1,1) & \text{if } \trans\models\LTLglobally\varphi,\\
(0,1,1) & \text{if } \trans\not\models\LTLglobally\varphi \text{ and } \trans\models\LTLfinally\LTLglobally\varphi,\\
(0,0,1) & \text{if } \trans\not\models\LTLglobally\varphi \text{ and } \trans\not\models\LTLfinally\LTLglobally\varphi, \text{ and }\trans\models\LTLglobally\LTLfinally\varphi,\\
(0,0,0) & \text{if } \trans\not\models\LTLglobally\varphi, \text{ and } \trans\not\models\LTLfinally\LTLglobally\varphi, \text{ and }\trans\not\models\LTLglobally\LTLfinally\varphi.\\
\end{cases}
\]

Thus, the value of $\gphi$ in a transition system $\trans$ is a vector $(v_1,v_2,v_3) \in \{0,1\}^3$, where the value $(1,1,1)$ corresponds to the $\true$ value in the classical semantics of LTL. When $\trans\not\models\gphi$, the values $(0,1,1)$, $(0,0,1)$ and $(0,0,0)$ capture the extent to which $\varphi$ holds or not along the traces of $\trans$. For example, if $\val\trans\gphi =(0,0,1)$, then $\varphi$ holds infinitely often on each trace of $\trans$, but there exists a trace of $\trans$ on which $\varphi$ is violated infinitely often. When $\val\trans\gphi =(0,0,0)$, then on some trace of $\trans$, $\varphi$ holds for at most finitely many positions.

Note that by the definition of $\mathit{val}$, if $\val\trans\gphi = (v_1,v_2,v_3)$, then
\emph{(1)} $v_1=1$ iff $\trans\models \gphi$,
\emph{(2)} $v_2=1$ iff $\trans\models \fgphi$, and
\emph{(3)} $v_3=1$ iff $\trans\models \gfphi$.
Thus, the lexicographic ordering on $\{0,1\}^3$ captures the preference of one transition system over another with respect to the  quantitative satisfaction of $\gphi$.

\begin{example}\label{ex:one-safety}
Consider a robot working as a museum guide. We want to synthesize a transition system representing a navigation strategy for the robot. One of the requirements is that its tour should visit the special exhibition infinitely often, formalized in LTL as $\LTLglobally\LTLfinally \specex$. We also desire that the robot never enters the staff's office, formalized as $\LTLglobally\neg\office$. Now, suppose that initially the key for the special exhibition is in the office. Thus, in order to satisfy $\LTLglobally\LTLfinally \specex$, the robot must violate $\LTLglobally\neg\office$. In any case, a strategy in which the office is entered only once, which satisfies $\fg \neg\office$ is preferable to one which enters the office over and over again, and only satisfies $\gf\neg\office$.
Thus, we want to synthesize a strategy $\trans$ with maximal value $\val\trans{\LTLglobally\neg\office}$.
\end{example}

\vspace{-.2cm}
In order to compare implementations with respect to their satisfaction of a conjunction $\gphi_1 \wedge \ldots \wedge \gphi_n$ of several safety specifications, we will extend the above definition. We consider the case when the specifier has not expressed any preference for the individual conjuncts. Consider the following example.

\vspace{-.2cm}
\begin{example}\label{ex:two-safety} We consider again the museum guide robot, now with two soft safety specifications. The specification $\LTLglobally (\occupied \rightarrow \neg \enter\_{\passage})$ requires that the robot does not enter the narrow passage if it is occupied. The second one, $\LTLglobally \neg\enter\_\library$, requires that the robot never enters the library. Passing through the library is an alternative to using the passage. Now, unless these specifications are given priorities, it is preferable to satisfy each of $(\occupied \rightarrow \neg \enter\_{\passage})$ and $\neg\enter\_\library$ infinitely often, rather than avoid entering the library by going through a occupied passage every time, or vice versa. 
\end{example}

\vspace{-.3cm}
\paragraph{Quantitative semantics of conjunctions.} 
To capture the idea illustrated in Example~\ref{ex:two-safety}, we define a value function, which intuitively 
gives higher values to transition systems in which a fewer number of soft specifications have low values. Formally, let \emph{the value of $\gphi_1 \wedge \ldots \wedge \gphi_n$ in $\trans$} be
\[\val\trans{\gphi_1 \wedge \ldots \wedge \gphi_n} \defeq \big(
\sum_{i=1}^n v_{i,3},
\sum_{i=1}^n v_{i,2},
\sum_{i=1}^n v_{i,1}
\big),\] 
where
$\val\trans{\gphi_i} = (v_{i,1},v_{i,2},v_{i,3})$ for $i \in \{1,\ldots,n\}$. To compare transition systems according to these values, we use lexicographic ordering on $\{0,\ldots,n\}^3$.

\begin{example}\label{ex:two-safety-val}  For the specifications in Example~\ref{ex:two-safety}, the value function defined above assigns value $(2,0,0)$ to a  system that satisfies  $\gf (\occupied \rightarrow \neg \enter\_{\passage})$ and $\gf\neg\enter\_\library$, but satisfies neither of $\fg (\occupied \rightarrow \neg \enter\_{\passage})$ and $\fg\neg\enter\_\library$. It assigns the smaller value $(1,1,1)$
to an implementation that satisfies $\LTLglobally (\occupied \rightarrow \neg \enter_{\passage})$, but not $\gf\neg\enter\_\library$.
\end{example}

Note that in the definition above we have reversed the order of the sums of the values $v_1, v_2$ and $v_3$, with the sum over  $v_3$ being the first, and the sum over $v_1$ being last. In this way, a transition system that satisfies all soft requirements to some extent is considered better in the lexicographic ordering than a transition system that satisfies one of them and violates all the others. We could instead consider the inverse lexicographic ordering, thus giving preference to satisfying some soft specification, over having some lower level of satisfaction over all of them. The next example illustrates the differences between these two variations.

\begin{example}\label{ex:ordering}
For the two soft specifications from Example~\ref{ex:two-safety}, reversing the order of the sums in the definition of $\val\trans{\gphi_1 \wedge \ldots \wedge \gphi_n}$ results in giving the higher value $(1,1,1)$ to a transition system that satisfies $\LTLglobally (\occupied \rightarrow \neg \enter\_{\passage})$ but not $\gf\neg\enter\_\library$, and the lower value $(0,0,2)$ to the one that guarantees only $\gf (\occupied \rightarrow \neg \enter\_{\passage})$ and $\gf\neg\enter\_\library$. The most suitable ordering usually depends on the specific application. 
\end{example}

In Appendix~\ref{sec:generalizations} we discuss generalizations of the framework, where
the user provides a set of relaxations for each of the soft specifications, and possibly a priority ordering among the soft specifications, or numerical weights.

\vspace{-.3cm}
\subsection{Maximum realizability}\label{sec:max-realizability}
Using the definition of quantitative satisfaction of soft safety specifications, we now define the maximum realizability problem, which asks to synthesize a transition system that satisfies a given \emph{hard} LTL specification, and is optimal with respect to the satisfaction of a conjunction of \emph{soft} safety specifications.

{\bf Maximum realizability problem:} Given an LTL formula $\spec$ and formulas $\gphi_1,\ldots,\gphi_n$, where each $\softSpec_i$ is a syntactically safe LTL formula, the maximum realizability problem asks to determine if there exists a transition system $\trans$ such that $\trans \models \spec$, and if the answer is positive, to synthesize a transition system $\trans$ such that $\trans \models \spec$, and such that for every transition system $\trans'$ with $\trans'\models \spec$ it holds that $\val\trans{\gphi_1 \wedge \ldots \wedge \gphi_n} \geq \val{\trans'}{\gphi_1 \wedge \ldots \wedge \gphi_n}$.

{\bf Bounded maximum realizability problem:} Given an LTL formula $\spec$ and formulas $\gphi_1,\ldots,\gphi_n$, where each $\softSpec_i$ is a syntactically safe LTL formula, and a bound $b$, the bounded maximum realizability problem asks to determine if there exists a transition system $\trans$ with $|\trans| \leq b$ such that $\trans \models \spec$, and if the answer is positive, to synthesize a transition system $\trans$ such that $\trans \models \spec$, $|\trans| \leq b$ and such that for every transition system $\trans'$ with $\trans'\models \spec$ and $|\trans'| \leq b$, it holds that $\val\trans{\gphi_1 \wedge \ldots \wedge \gphi_n} \geq \val{\trans'}{\gphi_1 \wedge \ldots \wedge \gphi_n}$.



\subsubsection{Robotic Navigation.}
We applied our method to the strategy synthesis for a robotic museum guide. The robot has to give a tour of the exhibitions in a specific order, which constitutes the hard specification. Preferably, it also avoids certain locations, such as the library, or the passage when it is occupied. These preferences are encoded in the soft specifications. There is one input variable that designates the occupancy of the passage, and eight output variables defining the position of the robot. 
The full set of specifications is given in Appendix~\ref{sec:robot-nav-appx}.

Table~\ref{tab:inst-robot} summarizes the results. With implementation bound of 8, the hard specification is realizable and a partial satisfaction of soft specifications is achieved. This strategy always selects the passage to transition from Exhibition 1 to Exhibition 2 and hence, avoids the library. It also violates the requirement of not entering the staff's office once, to acquire access to Exhibition 2. With implementation bound 10, a better strategy (with higher objective value) that alternates between entering the library and the passage is synthesized. This strategy is actually the optimal one with respect to the defined quantitative metric.

\begin{table*}[b!]\centering\footnotesize
	\begin{tabular*}{1\linewidth}{ccccccccccccccc}
		\toprule
		&& \multicolumn{3}{c}{Encoding} && \multicolumn{3}{c}{Solution} && \multicolumn{5}{c}{Time (s)} \\
		\cline{3-5} \cline{7-9} \cline{11-15}
		$|\trans|$ & \phantom{00} & \# vars & \phantom{0} & \# clauses & \phantom{00} & sat. & \phantom{0} & $\Sigma weights$ & \phantom{00} & Spot & \phantom{0} & Open-WBO & \phantom{0} & enc.+solve \\
		\midrule
		2 && 2837 && 18974 && UNSAT && 0 (39) && 0.61 && 0.0088 && 0.10 \\
		4 && 14573 && 98152 && UNSAT && 0 (39) && 0.61 && 0.057 && 0.46 \\
		6 && 40857 && 271474 && UNSAT && 0 (39) && 0.61 && 2.54 && 3.7 \\
		8 && 72057 && 482414 && SAT && 25 (39) && 0.61 && 2853 && 2856 \\
		10 && 135839 && 894892 && SAT && 30 (39) && 0.61 && time-out && time-out \\
		\bottomrule
	\end{tabular*}
	\caption{Results of applying synthesis with maximum realizability to the robotic navigation example, with different bounds on implementation size $|\trans|$. We report on the number of variables and clauses in the encoding, the satisfiability of hard constraints, the value (and bound) of the MaxSAT objective function, the running times of Spot and Open-WBO, and the time of the solver plus the time for generating the encoding.}
	\label{tab:inst-robot}
\end{table*}

\vspace{-.3cm}
\subsubsection{Power Distribution Network.}
We consider the problem of dynamic reconfiguration of power distribution networks. A power network consists of a set $\supplies$ of power supplies (generators) and a set $\loads$ of loads (consumers). The network is a bipartite graph with edges between supplies and loads, where each supply is connected to multiple loads and each load is connected to multiple supplies. Each power supply has an associated capacity, which determines how many loads it can power at a given point in time. Thus, it is possible that not all loads can be powered all the time. Some loads are critical and must be powered continuously, while others are not and should be powered when possible. Some loads can be initializing, meaning they must be powered only initially for several steps. Additionally, power supplies can become faulty during operation, which necessitates dynamic network reconfiguration.

\begin{table*}[b!]\centering\footnotesize

\begin{tabular*}{1\linewidth}{@{}c|ccccccccccccccccccc@{}}
\toprule
&& &\multicolumn{5}{c}{Network} &&\multicolumn{5}{c}{Load characterization} && \multicolumn{5}{c}{Specifications} \\
\cline{4-8} \cline{10-14} \cline{16-20}
& \begin{tabular}{c@{}} Instance \\ \# \end{tabular} & \phantom{ }\phantom{ }\phantom{ } & $|\supplies|$ & \phantom{} & $|\loads|$ & \phantom{} &  $\caps$ & \phantom{ }\phantom{ }\phantom{ } & crit. & \phantom{} & non-crit. & \phantom{} & init. & \phantom{ } \phantom{ }\phantom{ } \phantom{} & $|\inpv|$ & \phantom{} & $|\outv|$ & \phantom{} & \begin{tabular}{@{}c@{}} \# Soft \\ \; spec. \end{tabular}\\
\midrule
fully     & 1 && 3 && 3 &&  1 && 1 && 2 && 0 &&  2 && 9 && 2 \\
connected, & 2 && 3 && 6 &&  2 && 2 && 4 && 0 &&  2 && 18 && 4 \\
switching & 3 && 3 && 3 &&  1 && 0 && 2 && 1 &&  2 && 9 && 2 \\
allowed & 4 && 3 && 6 &&  2 && 1 && 4 && 1 &&  2 && 18 && 4 \\
\midrule
sparse,&5 && 4 && 2 &&  1 && 1 && 1 && 0 &&  3 && 4 && 1 \\
switching&6 && 4 && 4 &&  1 && 1 && 3 && 0 &&  3 && 8 && 3 \\
allowed&7 && 4 && 6 &&  1 && 1 && 5 && 0 &&  3 && 12 && 5 \\
&8 && 4 && 8 &&  1 && 1 && 7 && 0 &&  3 && 16 && 7 \\
\midrule
sparse,&9 && 4 && 2 &&  1 && 1 && 1 && 0 &&  3 && 4 && 5 \\
switching&10 && 4 && 4 &&  1 && 1 && 3 && 0 &&  3 && 8 && 11 \\
restricted&11 && 4 && 6 &&  1 && 1 && 5 && 0 &&  3 && 12 && 17 \\
&12 && 4 && 8 &&  1 && 1 && 7 && 0 &&  3 && 16 && 23 \\
\bottomrule
\end{tabular*}
\caption{Power distribution network instances. 
 An instance is determined by the number supplies $|\supplies|$, the number of loads $|\loads|$, the capacity of supplies $\caps$, the number of critical, non-critical and initializing loads. We also show the number of input $|\inpv|$ and output $|\outv|$ propositions and the number of soft specifications.}
\label{tab:def-inst}
\vspace{-.5cm}
\end{table*}

We apply our method to the problem of synthesizing a relay-switching strategy from LTL specifications. The input propositions $\inpv$ determine which, if any, of the supplies are faulty at each step. We are given an upper bound on the number of supplies that can be simultaneously faulty. The set $\outv$ of output propositions contains one proposition $\slp$ for each load $l \in \loads$  and each supply $p \in \supplies$ that are connected. The meaning of $\slp$ is that $l$ is powered by $p$.

The hard specifications assert that the critical loads must always be powered, the initializing loads should be powered initially, a load is powered by at most one supply, the capacity of supplies is not exceeded, and when a supply is faulty it is not in use.
The soft specifications state that non-critical loads are always powered, and that a powered load should remain powered unless its supply fails.

The full specifications are given in Appendix~\ref{sec:power-net-appx}. Table~\ref{tab:def-inst} describes the instances to which we applied our synthesis method. Power supplies have the same capacity $\caps$ (number of loads they can power) and at most one can be faulty. We consider three categories of instances, depending on the network connectivity (full or sparse), and whether we restrict frequent switching of supplies.
In Table~\ref{tab:inst-stat-1}, we report results for the instances from the first and the last category (for the middle category, see Appendix~\ref{sec:power-net-appx}). In the first set of instances in Table~\ref{tab:inst-stat-1}, we see the effect of specifications with large number of variables (due to full connectivity), where the bottleneck is the LTL to automata translation. In the second set in Table~\ref{tab:inst-stat-1} the limiting factor is the number of soft specifications, leading to large weights and variable numbers in the MaxSAT formulation.

\begin{table*}[!htbp]\centering\footnotesize
	\begin{tabular*}{1\linewidth}{@{}c|cccccccccccccc@{}}
		\toprule
		&& && \multicolumn{3}{c}{Encoding} && \multicolumn{1}{c}{Solution} && \multicolumn{5}{c}{Time (s)} \\
		\cline{5-7} \cline{9-9} \cline{11-15}
		\begin{tabular}{@{}c@{}} Instance \\ \# \end{tabular} & \phantom{0} & $|\trans|$ & \phantom{0} & \# vars & \phantom{0} & \# clauses & \phantom{0} & $\Sigma weights$ & \phantom{0} & Spot & \phantom{0} & Open-WBO & \phantom{0} & enc.+solve \\
		\midrule
		1 && 2 && 278 && 3599 && 11 (14) && 0.14 && 0.0040 && 0.071 \\
		  && 4 && 1102 && 20427 && 11 (14) && 0.14 && 0.017 && 0.14 \\
		  && 6 && 2958 && 60007 && 11 (14) && 0.14 && 0.64 && 0.97 \\
		  && 8 && 4966 && 106495 && 11 (14) && 0.14 && 71 && 71 \\
		\midrule
		2 && 2 && 516 && 14261 && 74 (84) && 85 && 0.013 && 0.16 \\
		&& 4 && 1988 && 81861 && 74 (84) && 85 && 0.079 && 0.59 \\
		&& 6 && 5292 && 240949 && 74 (84) && 85 && 2.2 && 3.6 \\
		&& 8 && 8844 && 427997 && 74 (84) && 85 && 1402 && 1405 \\
		\midrule
		3 && 2 && 334 && 7983 && 11 (14) && 0.29 && 0.032 && 0.12 \\
		&& 4 && 1510 && 45259 && 13 (14) && 0.29 && 0.021 && 0.26 \\
		&& 6 && 4302 && 132295 && 13 (14) && 0.29 && 0.099 && 0.77 \\
		&& 8 && 7334 && 235007 && 13 (14) && 0.29 && 1.0 && 2.2 \\
		\midrule
		4 && 2 && 572 && 38997 && 74 (84) && 200 && 0.023 && 0.37 \\
		&& 4 && 2396 && 224325 && 78 (84) && 200 && 0.14 && 1.5 \\
		&& 6 && 6636 && 659413 && 78 (84) && 200 && 1.1 && 4.9 \\
		&& 8 && 11212 && 1171933 && 78 (84) && 200 && 142 && 150 \\
		\midrule\midrule
		9 && 2 && 1047 && 10328 && 137 (155) && 0.18 && 0.0072 && 0.14 \\
		&& 4 && 3479 && 59298 && 137 (155) && 0.18 && 0.071 && 0.45 \\
		&& 6 && 8559 && 176428 && 137 (155) && 0.18 && 6.0 && 7.1 \\
		&& 8 && 26235 && 610246 && N/A (155) && 0.18 && time-out && time-out \\
		\midrule
		10 && 2 && 2153 && 22714 && 1403 (1463) && 0.48 && 0.015 && 0.27 \\
		&& 4 && 7113 && 130416 && 1403 (1463) && 0.48 && 0.60 && 1.5 \\
		&& 6 && 17505 && 387814 && 1403 (1463) && 0.48 && 716 && 718 \\
		&& 8 && 53693 && 1340908 && N/A (1463) && 0.48 && time-out && time-out \\
		\midrule
		11 && 2 && 3259 && 37596 && 5093 (5219) && 1.9 && 0.023 && 0.42 \\
		&& 4 && 10747 && 216254 && 5093 (5219) && 1.9 && 1.1 && 2.4 \\
		&& 6 && 26451 && 642976 && 5093 (5219) && 1.9 && 801 && 808 \\
		&& 8 && 81151 && 2222770 && N/A (5219) && 1.9 && time-out && time-out \\
		\midrule
		12 && 2 && 4365 && 61342 && 12503 (12719) && 27 && 0.031 && 0.74 \\
		&& 4 && 14381 && 355084 && 12503 (12719) && 27 && 2.6 && 4.8 \\
		&& 6 && 35397 && 1056826 && N/A (12719) && 27 && time-out && time-out \\
		&& 8 && 108609 && 3655032 && N/A (12719) && 27 && time-out && time-out \\
		\bottomrule
	\end{tabular*}
	\caption{Results of applying synthesis with maximum realizability on the instances in Table~\ref{tab:def-inst}, with different bounds on implementation size $|\trans|$. We report on the number of variables and clauses in the encoding, the value (and bound) of the objective function in the MaxSAT instance,  the running times of Spot and Open-WBO, and the time of the solver plus the time for generating the encoding.}
	\label{tab:inst-stat-1}
\end{table*}

\comment{
In large power networks, multiple generators act as power supplies that must provide power to numerous loads that represent the consumers. When continuously running, each of these components may become faulty which demands a network reconfiguration. The relays in the network perform such transitions between configurations. 

Here, we consider the problem of dynamic reconfiguration of a generic power distribution network. The system determines the configuration of the network through variables representing the relays' positions. Since the faults in the components are unpredictable, they can be represented by the environment. However, to ensure realizability of the problem, we restrict the number of faulty components. 

Let $\mathcal{P} = \{P_1, P_2, ..., P_m\}$ denote the set of power supplies and $\mathcal{L} = \{L_1, L_2, ..., L_n\}$ to denote the set of consumer components. Each power supply has limited power capacity, represented by $P^+_i$ while each load has a power demand, represented by $P^-_i$. Depending on the network architecture, each of the loads has access to a subset of power supplies, i.e., $A_L(L_i) \subseteq \mathcal{P}$ where $A_L(L_i)$ determines the power supplies that are accessible by load $L_i$. On the other hand, each power supply is accessible to a subset of loads. Let $A_P(P_i) \subseteq \mathcal{L}$ denote the load components that can connect to power supply $P_i$. Such architecture can be illustrated via a bipartite graph where the connectivity matrix defines set functions $A_L$ and $A_P$. 
Furthermore, some of the components are in the same subsystem whose operation requires all those loads to be powered. We capture this by introducing disjoint classes of loads $\mathcal{C} = \{C_1, C_2, ..., C_k\}$ where $C_i \subseteq \mathcal{L}$ and $C_i \cap C_j = \emptyset ,\; \forall i\neq j$. Additionally, the relative importance of subsystems imposes a set of weights that show the priorities of providing power to the loads. Let $w_1, w_2, ..., w_k$ to denote the weights associated with classes. If a subsystem must always be powered, its corresponding weight is set to $\infty$.

This framework allows us to model a generic power distribution network on an abstract level. For instance, the network shown in Fig.[-a] with 2 power supplies and 4 loads can be abstracted into the graph of Fig.[-b]. For such model, we aim to synthesis a planner that dynamically assigns the loads to healthy power supplies. The planner has to respect the connectivity structure of the network and should try to maximally power the subsystems. We cast this optimization according to the lexicographical ordering introduced in section [] and predefined weights over the soft constraints. 

We define a set of variables along a series of LTL constraints that model the problem and capture the desired requirements of the system. When the number of faulty generators upperbounded by $l$, the environment can be defined as $l$ integer variables $e_1, e_2, ..., e_l; \; e_i \in \{0, 1, ..., n\}$, where a non-zero assignment shows a faulty generator.\footnote{Two environment variables can be non-zero and have the same value. While this will be redundant, it does not affect the encoding.} The system variables are $s_{i \rightarrow j}$'s such that $s_{i \rightarrow j} = 1$ if load $i$ is assigned to power supply $j$ and $s_{i \rightarrow j} = 0$ otherwise. Note that not all the power supplies are available to a consumer, therefore, for the $i^{th}$ consumer, the range that $j$ varies over depends on the available suppliers for that load. 

A critical load must always be powered. This leads to hard constraint
\begin{equation}
\square \left( \bigvee_{j \in A_L(L_i)} s_{i \rightarrow j} \right) \,, 
\quad \forall \ i \in \{1, 2, ..., n\} \ s.t. \ w_i = \infty.
\end{equation}
A non-critical load being powered introduces a soft constraint, i.e.,
\begin{equation}
\square \left( \bigvee_{j \in A_L(L_i)} s_{i \rightarrow j} \right) \,, 
\quad \forall \ i \in \{1, 2, ..., n\} \ s.t. \ w_i < \infty,
\end{equation}
which if it is not realizable, we relax it according to the proposed lexicographical ordering. A load should only be assigned to one power supply:
\begin{equation}
\bigwedge_{i \in \{1, 2, ..., n\}}
\bigwedge_{j_1 \in A_L(L_i)}
\square \left(s_{i \rightarrow j_1} 
\rightarrow \bigwedge_{j_2 \in A_L(L_i), j_2 \neq j_1}\neg s_{i \rightarrow j_2}\right),
\end{equation}
or equivalently,
\begin{equation}
\square \left(\neg s_{i \rightarrow j_1} \lor \neg s_{i \rightarrow j_2}\right) \,,
\qquad \forall \ i \in \{1, 2, ..., n\}, \forall \ j_1, j_2 \in \{1, 2, ..., m\}, j_1 \neq j_2.
\end{equation}
Let the capacity of the power sources to be dependent on the number of loads that are attached to them, i.e., the power requirements of all load components are similar. Therefore, the constrained capacity of power supplies is expressed in the following constraint:
\begin{equation}
\bigwedge_{j \in \{1, 2, ..., m\}} 
\bigwedge_{\substack{{L \subseteq A_P(P_j)} \\ {|L| = P^+_j}}}
\square \left( \bigwedge_{i_1 \in L} s_{i_1 \rightarrow j} \rightarrow
\bigwedge_{i_2 \in A_P(P_j) \backslash L} \neg s_{i_2 \rightarrow j} \right).
\end{equation}
When a power supply becomes faulty, we require the loads to be disconnected from it:\footnote{Depending on the response time, one can add ``next'' operator to expect disconnection in future time steps.}
\begin{equation}
\bigwedge_{k \in \{1, 2, ..., l\}}
\bigwedge_{j \in \{1, 2, ..., m\}}
\square \left( e_k = j \rightarrow 
\bigwedge_{i \in A_P(P_j)} \neg s_{i \rightarrow j} \right).
\end{equation}

\begin{equation}
\bigwedge_{i \in \{1, 2, ..., n\}}
\bigwedge_{j \in A_L(L_i)}
\square \left( 
s_{i \rightarrow j} \land \LTLnext \left( \neg 
\bigvee_{k \in \{1, 2, ..., l\}} e_k = j \right)
\rightarrow \LTLnext s_{i \rightarrow j} \right) 
\end{equation}

\begin{equation}
\bigvee_{j \in A_L(L_i)} s_{i \rightarrow j} \land 
\LTLnext \left( \bigvee_{j \in A_L(L_i)} s_{i \rightarrow j} \right) 
\land \ldots \land
\LTLnext^{t_{init}} \left( \bigvee_{j \in A_L(L_i)} s_{i \rightarrow j} \right)
\,, \quad \forall \ i \in \mathcal{L}_{init}
\end{equation}
}
\subsubsection{Maximum Realizability with Soft LTL Specifications.}\label{sec:soft-ltl}
The first generalization of the maximum realizability problem that we consider is the setting where the soft specifications can be arbitrary LTL formulas, and not just safety properties of specific form. More precisely, each soft specification $\softSpec$ is an LTL formula for which we are also given a vector $\Relax(\softSpec)$ of LTL formulas that defines the possible relaxations of $\softSpec$. Formally, $\Relax(\softSpec) = (\psi_{0},\ldots,\psi_{m})$, where $\psi_{0} = \softSpec$, and for every $0 \leq k < m$ it holds that $\trans \models \psi_{k}$ implies $\trans \models \psi_{k+1}$ for every transition system $\trans$. That is, $\psi_{0},\ldots,\psi_{m}$ are ordered according to strength.
In particular, if $\trans \models \softSpec$, then $\trans \models \psi_k$ for each $\psi_k$ in $\Relax(\softSpec)$.
For example, if $\softSpec = \LTLglobally p$ for some atomic proposition $p$, we can take $\Relax(\softSpec) = (\LTLglobally p,\LTLfinally\LTLglobally p,\LTLglobally\LTLfinally p)$.

As in Section~\ref{sec:quantitative-semantics} we define the value of $\softSpec$ for given $\Relax(\softSpec) = (\psi_{0},\ldots,\psi_{m})$ to be $\val\trans\softSpec = (v_1,\ldots,v_m)$, where $v_k = 1$ if $\trans \models \psi_k$, and $v_k = 0$ otherwise.

For a conjunction $\softSpec_1\wedge\ldots\wedge\softSpec_n$ of soft specifications with given $\Relax(\softSpec_j) = (\psi_{j,0},\ldots,\psi_{j,m})$ for each $j \in \{1,\ldots,n\}$, we define the value
$\val\trans{\softSpec_1 \wedge \ldots \wedge \softSpec_n} = \big(
\sum_{i=1}^n v_{i,m},
\ldots,
\sum_{i=1}^n v_{i,0}
\big),$ where
$\val\trans{\softSpec_i} = (v_{i,0},\ldots,v_{i,m})$ for $i \in \{1,\ldots,n\}$.

The maximum realizability problem asks for given LTL specification $\spec$ and soft LTL specifications 
$\softSpec_1,\ldots,\softSpec_n$ with given $\Relax(\softSpec_j) = (\psi_{j,0},\ldots,\psi_{j,m})$, to determine whether there exists a transition system $\trans$ such that $\trans\models\spec$, and if the answer is positive, to construct a transition system $\trans^*$ such that $\trans^* \models \spec$, and for every $\trans$ with $\trans\models\spec$ it holds that $\val\trans{\softSpec_1 \wedge \ldots \wedge \softSpec_n} \leq \val{\trans^*}{\softSpec_1 \wedge \ldots \wedge \softSpec_n}$.
The bounded maximum realizability problem is defined in the obvious way.

We can adapt the MaxSAT approach from Section~\ref{sec:maxsat} to solve the bounded maximum realizability problem in this setting as follows. 

First, for each $\psi_{j,k}$ in $\Relax(\softSpec_j)$, we construct a universal co-B\"uchi automaton $\autA_{j,k} = (Q_{j,k},q_0^{j,k},\delta_{j,k},F_{j,k})$ such that $\trans \in \lang{\autA_{j,k}}$ if and only if $\trans \models \psi_{j,k}$.
In the MaxSAT encoding, the hard constraints for the annotation $\anot_{j,k}$  are
\begin{align*}
C_{j,k}\defeq\bigwedge_{q,q' \in Q_{j,k}}\bigwedge_{s,s' \in S}\bigwedge_{\inpval \in \ialphabet}
\Bigg( &
\big(
\anotbjk_{s,q} \wedge
\delta^{j,k}_{s,q,\inpval,q'}\wedge 
\tau_{s,\inpval,s'}
\big) \rightarrow 
\succa_{\anot}^{j,k}(s,q,s',q',\inpval)
\Bigg).
\end{align*}
Generalizing the encoding, for each $j \in \{1,\ldots,n\}$ and $k \in \{0,\ldots,m\}$ we now have one soft constraint
$\soft_{j,k}\defeq  \bigvee_{l=0}^k \anotbjl_{s_0,q^{j,l}}$ with weight $n^k$.

\smallskip
\noindent 
{\bf Maximum Realizability with Priorities.}
In the definitions in Section~\ref{sec:max-realizability} and the paragraph above, all soft specifications have the same priority. Now, we extend the maximum realizability setting with priorities for the soft specifications given as part of the input to the problem.

\smallskip
\noindent
{\it Soft specifications with priority ordering.} We begin with a simple setting where soft specifications are simply ordered in decreasing priority, without assigning any numerical weight for each formula's preference. More specifically, we assume that the soft specifications $\softSpec_1,\ldots,\softSpec_n$ are ordered such that, for every $i \in \{1,\ldots,n\}$, we have that $\softSpec_i$ has higher priority than $\softSpec_j$ for all $j > i$. 

Now, given a vector $\Relax(\softSpec_j) = (\psi_{j,0},\ldots,\psi_{j,m})$ for $\softSpec_j$  we define the value of $\softSpec_j$ in a transition system $\trans$ to be the number of specifications in $\Relax(\softSpec_j)$ satisfied by $\trans$, i.e., $\val\trans{\softSpec_j} = | \{k \in \{0,\ldots,m\} \mid \trans\models \psi_{j,k}\}|$. The value of $\softSpec_1\wedge\ldots\wedge\softSpec_n$ is then defined as $\val\trans{\softSpec_1 \wedge \ldots \wedge \softSpec_n} = (\val\trans{\softSpec_1},\ldots,\val\trans{\softSpec_n})$. The values of transition systems are compared according to the lexicographic ordering of vectors in $\{0,\ldots,m+1\}^n$, giving priority of $\softSpec_i$ over $\softSpec_j$ for $i < j$.

The MaxSAT approach can be adapted for this value function in the same way as above. The difference is in the weights of the soft constraints for the annotations $\anot_{j,k}$: for each
$j \in \{1,\ldots, n\}$ and $k \in \{1,\ldots,m\}$ we have a soft constraint  $\soft_{j,k} \; \defeq \;  \bigvee_{l=0}^k \anotbjl_{s_0,q^{j,l}}$ with weight $w_{j,k}$, where 
$w_{j,k} = 1 $ if $j=n$ or $k < m$, and $w_{j,k} = \sum_{j' = j+1}^n \sum_{k = 1}^m w_{j',k} + 1$ otherwise.

\smallskip
\noindent
{\it Soft specifications with given weights.}
We also consider the weighted maximum realizability problem, in which, together with $\Relax(\softSpec)$ for each soft specification $\softSpec$, the user also provides numerical weights for the formulas in $\Relax(\softSpec)$. That is, for each $j \in \{1,\ldots,n\}$ and $k \in \{1,\ldots,m\}$ we are given a weight $w_{j,k}$ for $\psi_{j,k}$. These weights specify the priority of each of the soft specifications.

The MaxSAT formulation is then adapted to incorporate the given weights, by using them for the corresponding soft constraints. Namely, for each $j$ and $k$, the corresponding soft constraint $\soft_{j,k}  \; \defeq \;  \bigvee_{l=0}^k \anotbjl_{s_0,q^{j,l}}$ has weight $w_{j,k}$.

\comment{
\begin{theorem}\label{thm:optimal-bound-general}
Given an LTL specification $\spec$ and a soft specification $\gphi_1 \wedge\ldots \wedge\gphi_n$ together with a vector of formulas $\Relax(\softSpec_j) = (\psi_{j,0},\ldots,\psi_{j,m})$ for each $\softSpec_j$,
if there is a transition system $\trans$ with  $\trans \models \spec$, then there exists $\trans^*$ such that:
\begin{itemize}
\item $\val\trans{\softSpec_1 \wedge \ldots \wedge \softSpec_n} \leq \val{\trans^*}{\softSpec_1 \wedge \ldots \wedge \softSpec_n}$ for all $\trans$ with $\trans \models \spec$,
\item $\trans^* \models \spec$ and $|\trans^*| \leq (2^{b+\log b})!^2$, where
\end{itemize}
$b = \max\{|\subf{\spec\wedge\softSpec_1'\wedge\ldots\wedge\softSpec_n'}| \mid \softSpec_i' \in \Relax(\softSpec_i) \text{ for }i=1,\ldots,n\}$.
\end{theorem}
}

\begin{appxthm}\label{thm:optimal-bound-general-appx}
Given an LTL specification $\spec$ and a soft specifications $\gphi_1,\ldots,\gphi_n$ together with a vector of formulas $\Relax(\softSpec_j) = (\psi_{j,0},\ldots,\psi_{j,m})$ for each $\softSpec_j$,
if there is a transition system $\trans$ with  $\trans \models \spec$, then there exists $\trans^*$ such that:
\begin{itemize}
\item $\val\trans{\softSpec_1 \wedge \ldots \wedge \softSpec_n} \leq \val{\trans^*}{\softSpec_1 \wedge \ldots \wedge \softSpec_n}$ for all $\trans$ with $\trans \models \spec$, and
\item $\trans^* \models \spec$ and $|\trans^*| \leq (2^{b+\log b})!^2$,
\end{itemize}
where $b = \max\{|\subf{\spec\wedge\softSpec_1'\wedge\ldots\wedge\softSpec_n'}| \mid \softSpec_i' \in \Relax(\softSpec_i) \text{ for }i=1,\ldots,n\}$.
\end{appxthm}
\begin{proof}
The proof is a generalization of the proof of Theorem~\ref{thm:optimal-bound-safety}. First, we need to establish the analogue of Lemma~\ref{lem:value-as-ltl} for the general case. 

\begin{appxlemma}\label{lem:value-as-ltl-general-appx}
For every transition system $\trans$, soft specifications $\gphi_1,\ldots,\gphi_n$, and vector of formulas $\Relax(\softSpec_j) = (\psi_{j,0},\ldots,\psi_{j,m})$ for each $\softSpec_j$, if $\val\trans{\gphi_1 \wedge \ldots \wedge \gphi_n} = v$, then there exists an LTL formula $\psi_v$ such that $\trans \models \psi_v$ and the following hold:
\begin{itemize}
\item[(1)] $\psi_v = \softSpec_1'\wedge\ldots\wedge\softSpec_n'$, where $\softSpec_i' \in\Relax(\softSpec_i)  \text{ for }i=1,\ldots,n$, 
\item[(2)] for every $\trans'$, if $\trans' \models \psi_v$, then $\val{\trans'}{\gphi_1 \wedge \ldots \wedge \gphi_n} \geq v$.
\end{itemize}
\end{appxlemma}
The proof of Lemma~\ref{lem:value-as-ltl-general-appx} is analogous to the proof of Lemma~\ref{lem:value-as-ltl-appx}. Then, with the help of Lemma~\ref{lem:value-as-ltl-general-appx} we can establish the theorem in the same way as Theorem~\ref{thm:optimal-bound-safety}. \qed
\end{proof}


\section{Introduction}\label{sec:intro}
\input{intro.tex}

\section{Maximum Realizability Problem}\label{sec:problem}
\input{problem.tex}



\section{Preliminaries}
\input{prelim.tex}


\section{From Maximum Realizability to MaxSAT}\label{sec:maxsat-encoding}
\input{maxsat.tex}


\section{Experimental Evaluation}\label{sec:experiments}
\input{experiments.tex}


\newpage
\bibliographystyle{plain}

\subsection{Bounded Maximum Realizability}
To establish an upper bound on the minimal (in terms of size) optimal implementation, we make use of an important property of the function $\mathit{val}$ defined in Section~\ref{sec:quantitative-semantics}. Namely, the property that for each of the possible values of $\gphi_1 \wedge\ldots \wedge\gphi_n$  there is a corresponding LTL formula that encodes this value in the classical LTL semantics, as we formally state in the next lemma.

\begin{lemma}\label{lem:value-as-ltl}
For every transition system $\trans$ and soft safety specifications $\gphi_1,\ldots,$ $\gphi_n$, if $\val\trans{\gphi_1 \wedge \ldots \wedge \gphi_n} = v$, then there exists an LTL formula $\psi_v$ such that $\trans \models \psi_v$ and the following conditions hold
\begin{itemize}
\item[(1)] $\psi_v = \softSpec_1'\wedge\ldots\wedge\softSpec_n'$, where $\softSpec_i' \in\{\gphi_i,\fgphi_i,\gfphi_i,\true\} \text{ for }i=1,\ldots,n$, 
\item[(2)] for every $\trans'$, if $\trans' \models \psi_v$, then $\val{\trans'}{\gphi_1 \wedge \ldots \wedge \gphi_n} \geq v$.
\end{itemize}
\end{lemma}

The following theorem is a consequence of Lemma~\ref{lem:value-as-ltl}. 
\begin{theorem}\label{thm:optimal-bound-safety}
Given an LTL specification $\spec$ and soft safety specifications $\gphi_1,\ldots,$ $\gphi_n$,  
if there exists a transition system $\trans \models \spec$, then there exists  $\trans^*$ such that
\begin{itemize}
\item [(1)] $\val\trans{\gphi_1 \wedge \ldots \wedge \gphi_n} \leq \val{\trans^*}{\gphi_1 \wedge \ldots \wedge \gphi_n}$ for all $\trans$ with $\trans \models \spec$,
\item[(2)] $\trans^* \models \spec$ and $|\trans^*| \leq \left((2^{(b+\log b)})!\right)^2$,
\end{itemize}
 where $b = \max\{|\subf{\spec\wedge\softSpec_1'\wedge\ldots\wedge\softSpec_n'}| \mid \forall i:\ \softSpec_i' \in\{\gphi_i,\fgphi_i,\gfphi_i\}\}$.
\end{theorem}

The bound above is estimated based on the size of the specifications, using a worst-case bound on the size of the corresponding automata. Given automata for all the specifications $\gphi_i,\fgphi_i$ and $\gfphi_i$, a potentially better bound can be estimated based on the size of these automata.

Lemma~\ref{lem:value-as-ltl} immediately provides a naive synthesis procedure, which searches for an optimal implementation by enumerating possible $\psi_v$ formulas and solving the corresponding realizability questions. The total number of these formulas is $4^n$, where $n$ is the number of soft specifications. The approach that we propose avoids this rapid growth, by reducing the optimization problem to a single MaxSAT instance, and thus it also makes use of  the power of MaxSAT solvers.

\subsection{Automata and Annotations for Soft Safety Specifications}\label{sec:automata-safety}
Let $\gphi$ be an LTL formula, where $\varphi$ is a syntactically safe LTL formula.

The first step in the MaxSAT reduction is the construction of a universal B\"uchi automaton for each soft safety specification $\gphi$ and its modification to incorporate the relaxation of $\gphi$ to $\fgphi$, as we now describe.

\begin{proposition}\label{prop:aut-globally}
Given an LTL formula $\gphi$ where $\varphi$ is syntactically safe, we can construct a universal B\"uchi automaton  $\autB_{\scriptsize \gphi} = (Q_{\scriptsize \gphi},q_0^{\scriptsize \gphi},\delta_{\scriptsize \gphi},F_{\scriptsize \gphi})$ such that 
 $\lang{\autB_{\scriptsize \gphi}} = \{\trans \mid \trans \models \gphi\}$, and $\autB_{\scriptsize \gphi}$ has a unique non-accepting sink state, that is, there exists a unique state $\rej_\varphi \in Q_{\scriptsize \gphi}$ such that 
$F_{\scriptsize \gphi} = Q_{\scriptsize \gphi} \setminus \{\rej_\varphi\}$, and for every $\sigma \in \Sigma$ it holds that $\{q \in Q_{\scriptsize \gphi} \mid (\rej_\varphi,\sigma,q) \in \delta_{\scriptsize \gphi}\}  = \{\rej_\varphi\}$.
\end{proposition}

From $\autB_{\scriptsize \gphi}$, which has at most $2^{\mathcal{O}(|\varphi|)}$ states, we obtain a universal automaton $\relaxfg(\gphi)$ constructed by redirecting all the transitions leading  to $\rej_\varphi$ to the initial state $q_0^{\scriptsize \gphi}$. Formally, 
$\relaxfg(\gphi) = (Q,q_0,\delta,F)$, where $Q = Q_{\scriptsize \gphi} \setminus \{\rej_\varphi\}$, $q_0 = q_0^{\scriptsize \gphi}$, $F = F_{\scriptsize \gphi}$ and the transition relation is defined as
\[\delta = \left(\delta_{\scriptsize \gphi} \setminus \{(q,\sigma,q') \in \delta_{\scriptsize \gphi}\mid q' = \rej_\varphi\}\right) \cup \{(q,\sigma,q_0) \mid (q,\sigma,\rej_\varphi)\in \delta_{\scriptsize \gphi}\}.\]

\noindent
Let $\Rej(\relaxfg(\gphi)) = \{(q,\sigma,q_0) \in \delta \mid (q,\sigma,\rej_\varphi) \in \delta_{\scriptsize \gphi}\}$ be the set of transitions in $\relaxfg(\gphi)$ that correspond to transitions in $\autB_{\scriptsize \gphi}$ leading to $\rej_\varphi$. 

The next proposition formalizes the property that a transition system $\trans$ is accepted by $\autB_{\scriptsize \gphi}$ iff the run graph of $\relaxfg(\gphi)$ on $\trans$ does not contain an edge corresponding to a transition in $\Rej(\relaxfg(\gphi))$. 
\begin{proposition}\label{prop:rej-trans}
Let $\trans$ be a transition system and let $G = (V,E)$ be the run graph of $\relaxfg(\gphi)$ on $\trans$. Then, $\trans \in\lang{\autB_{\scriptsize \gphi}}$ iff for every  $((s,q),\sigma,(s',q')) \in E$ with $(q,\sigma,q') \in  \Rej(\relaxfg(\gphi))$, $(s,q)$ is not reachable from $(s_0,q_0)$ in $G$.
\end{proposition}

We define an annotation function $\anotfg : S \times Q \to \natsbot$ for a transition system $\trans = (S,s_0,\tau)$ and the automaton $\relaxfg(\gphi) = (Q,q_0,\delta,F)$. The value of $\anotfg$ for the initial node of the run graph determines whether $\trans$ satisfies $\gphi$ or $\fgphi$.
A function $\anotfg : S \times Q \to \natsbot$ is \emph{\fgvalid}\ annotation if it is such that
\begin{itemize}
\item[\emph{(1)}] $\anotfg(s_0,q_0) \neq \bot$, i.e., the pair of initial states is labelled with a number, and 
\item[\emph{(2)}] if $\anotfg(s,q) \neq \bot$, then for every edge $((s,q),\sigma,(s',q'))$ in the run graph of $\relaxfg(\gphi)$ on $\trans$ we have that $\anotfg(s',q') \neq \bot$, and
\begin{itemize}
\item if $(q,\sigma,q') \in\Rej(\relaxfg(\gphi))$, then $\anotfg(s',q') >  \anotfg(s,q)$, and 
\item if $(q,\sigma,q') \not\in\Rej(\relaxfg(\gphi))$, then $\anotfg(s',q') \geq  \anotfg(s,q)$.
\end{itemize}
\end{itemize}

This definition  guarantees that if $\anotfg$ is a bounded \fgvalid\ annotation for $\trans$ and $\relaxfg(\gphi)$, then the number of rejecting edges in each path in the run graph of $\relaxfg(\gphi)$ on $\trans$ is finite, which implies $\trans \models \fgphi$ as stated below.\looseness=-1

\begin{proposition}\label{prop:anotfg}
Let $\trans = (S,s_0,\tau)$ be a finite-state transition system, and $G = (V,E)$ be the run graph of  $\relaxfg(\gphi)$ on $\trans$. Then, $\trans \models \fgphi$ if and only if there exists a \fgvalid\ $|\trans|$-bounded annotation for $\trans$ and $\relaxfg(\gphi)$. 
\end{proposition}

If the run graph of $\relaxfg(\gphi)$ on $\trans$ contains a reachable edge which belongs to $\relaxfg(\gphi)$, then we can conclude that $\trans\not\models\gphi$. However, if each infinite path in the run graph contains only a finite number of occurrences of edges in $\relaxfg(\gphi)$, then $\trans\models\fgphi$. In particular, we have that if $\anotfg(s_0,q_0) \in \nats$, then $\trans \models \fgphi$, and if $\anotfg$ is $c$-bounded and $\anotfg(s_0,q_0) = c$, then $\trans \models \gphi$.

This property of $\anotfg$ allows us to capture the satisfaction of $\gphi$ and of $\fgphi$ with soft clauses for the same annotation function in the MaxSAT formulation.

\subsection{MaxSAT Encoding of Bounded Maximum Realizability}\label{sec:maxsat}

Let $\autA = (Q,q_0,\delta,F)$ be a universal co-B\"uchi automaton for the LTL formula $\spec$.

For each syntactically safe formula $\gphij$, $j \in\{1,\ldots,n\}$, we consider two universal automata:
the universal automaton $\autB_j = \relaxfg(\gphi_j)= (Q_j,q_0^j,\delta_j,F_j)$ constructed as described in Section~\ref{sec:automata-safety} and 
a universal co-B\"uchi automaton $\autA_j = (\widehat Q_j,\widehat q_0^j,\widehat\delta_j,\widehat F_j)$ for the formula $\gfphi_j$. 
Given a bound $b$ on the size of the sought transition system, we encode the bounded maximum realizability problem as a MaxSAT problem with the following sets of variables and constraints.

{\bf Variables:} The MaxSAT formulation includes the variables from the SAT formulation of the bounded synthesis problem, which represent the sought transition system $\trans$ and the sought valid annotation of the run graph of $\autA$ on $\trans$. Additionally, it includes variables for representing the annotations $\anotfg_j$ and $\anot_j$ for $\autB_j$ and $\autA_j$ respectively, similarly to $\anot$ in the SAT encoding. More precisely, the annotations for $\anotfg_j$ and $\anot_j$ are represented respectively by variables $\anotfgbj_{s,q}$ and $\anotfgnj_{s,q}$  where $s\in S$ and $q \in Q_j$, and $\anotbj_{s,q}$ and $\anotnj_{s,q}$ where $s\in S$ and $q \in \widehat Q_j$.

The set of constraints includes $C_\tau$ and $C_\anot$ from the SAT formulation as hard constraints, as well as the following constraints for the new annotations.

{\bf Hard constraints for valid annotations:}
For each $j=1,\ldots,n$, let
\begin{align*}
C_\anotfg^{j}\defeq\bigwedge_{q,q' \in Q_j}\bigwedge_{s,s' \in S}\bigwedge_{\inpval \in \ialphabet}
\Big( &
\big(
\anotfgbj_{s,q} \wedge
\delta^j_{s,q,\inpval,q'}\wedge 
\tau_{s,\inpval,s'}
\big) \rightarrow 
\succa_{\anotfg}^j(s,q,s',q',\inpval) 
\Big),
\\
C_\anot^{j}\defeq\bigwedge_{q,q' \in \widehat Q_j}\bigwedge_{s,s' \in S}\bigwedge_{\inpval \in \ialphabet}
\Big( &
\big(
\anotbj_{s,q} \wedge
\widehat\delta^j_{s,q,\inpval,q'}\wedge 
\tau_{s,\inpval,s'}
\big) \rightarrow 
\succa_{\anot}^j(s,q,s',q',\inpval)
\Big),
\end{align*}
\begin{align*}
\text{where }\succa_\anotfg^j(s,q,s',q',\inpval) \defeq \anotfgbj_{s',q'} \wedge &
\big(\rej^j(s,q,q',\inpval) \rightarrow \anotfgnj_{s',q'} > \anotfgnj_{s,q}\big) \wedge
\\&
\big(\neg\rej^j(s,q,q',\inpval) \rightarrow \anotfgnj_{s',q'} \geq \anotfgnj_{s,q}\big)
,
 \end{align*}
and $\rej^j(s,q,q',\inpval)$ is a formula over $o_{s,\inpval}$ obtained from $\Rej(\autB_j)$.
The formula $\succa_{\anot}^j(s,\widehat q,s',\widehat q',\inpval)$ is analogous to 
$\succa_{\anot}(s,q,s',q',\inpval)$ defined in Section~\ref{sec:bounded-synthesis}.

{\bf Soft constraints for valid annotations:}
For each $j=1,\ldots,n$ we define
\[
\begin{array}{lllll}
\soft_{\tiny\LTLglobally}^{j} & \quad \defeq \quad &  \anotfgb_{s_0,q_0^j} \wedge (\anotfgn_{s_0,q_0^j} = b) & \qquad & \text{with weight }1,\\
\soft_{\tiny\LTLfinally\LTLglobally}^{j} & \quad \defeq \quad & \anotfgb_{s_0,q_0^j} & \quad & \text{with weight }n, \text{ and }\\
\soft_{\tiny\LTLglobally\LTLfinally}^{j} & \quad \defeq \quad & \anotfgb_{s_0,q_0^j} \vee \anotb_{s_0,\widehat  q_0^j} & \quad & \text{with weight }n^2,\\
\end{array}
\]
where $b \in \nats$ is the bound on the size of the transition system.

The definition of the soft constraints guarantees that $\trans \models \gphi_j$ if and only if there exist corresponding annotations that satisfy all three of the soft constraints for $\gphi_j$. Similarly, if $\trans \models \fgphi_j$, then $\soft_{\tiny\LTLfinally\LTLglobally}^{j}$ and $\soft_{\tiny\LTLglobally\LTLfinally}^{j}$ can be satisfied.

The weights are selected in a way that reflects the ordering of transition systems with respect to their satisfaction of $\gphi_1 \wedge \ldots \wedge \gphi_n$, as stated below.

\begin{lemma}\label{lem:encoding-weights}
Let $\trans'$ and $\trans''$ be transition systems such that $\trans' \models \spec$ and $\trans'' \models \spec$. Let $a'$ and $a''$ be variable assignments satisfying the constraint system, such that $a'$ is an optimal assignment consistent with $\trans'$, and $a''$ is an optimal assignment consistent with $\trans''$. Furthermore, let $w'$ and $w''$ be the sums of the weights of the soft clauses satisfied in $a'$ and $a''$ respectively. Then, it holds that
$\val{\trans'}{\gphi_1 \wedge \ldots \wedge \gphi_n} < \val{\trans''}{\gphi_1 \wedge \ldots \wedge \gphi_n} \text{ iff } w' < w''.$
\end{lemma}

The next results establish the size and correctness of the encoding.

\begin{theorem}\label{thm:encoding-correctness}
Let $\autA$ be a given co-B\"uchi automaton for $\varphi$, and for each $j \in \{1,\ldots,n\}$, let $\autB_j = \relaxfg(\gphi_j)$ be the universal automaton for $\gphi_j$ constructed as in Section~\ref{sec:automata-safety}, and let $\autA_j$ be a universal co-B\"uchi automaton for $\gfphi_j$. 
The constraint system for bound $b \in \nats$ is satisfiable if and only if there exists an implementation $\trans$ with $|\trans| \leq b$  such that $\trans \models \varphi$. Furthermore, from the optimal satisfying assignment to the variables $\tau_{s,\inpval,s'}$ and $o_{s,\inpval}$, one can extract a transition system $\trans^*$ such that for every transition system $\trans$ with $|\trans| \leq b$ and $\trans \models \varphi$ it holds that $\val\trans{\gphi_1 \wedge \ldots \wedge \gphi_n} \leq \val{\trans^*}{\gphi_1 \wedge \ldots \wedge \gphi_n}$.
\end{theorem}

\begin{proposition}\label{prop:encoding-size}
Let $\autA$ be a given co-B\"uchi automaton for $\varphi$, and for each $j \in \{1,\ldots,n\}$, let $\autB_j = \relaxfg(\gphi_j)$ be the universal B\"uchi automaton for $\gphi_j$ constructed as in Section~\ref{sec:automata-safety}, and let $\autA_j$ be a universal co-B\"uchi automaton for $\gfphi$. 
The constraint system for bound $b \in \nats$ has weights in $\mathcal{O}(n^2)$,
\[
\begin{array}{l}
\mathcal{O}\Big(
(b^2 + b \cdot |\outv|)\cdot 2^{|\inpv|} +  
b \cdot |Q|\cdot (1+ \log(b \cdot |Q|)) +\\ 
\phantom{\mathcal{O}(}\sum_{j=1}^n\big(b \cdot |Q_j| (1 + \log(b\cdot |Q_j|))\big)
+ \sum_{j=1}^n\big(b \cdot |\widehat Q_j| (1 + \log(b\cdot |\widehat Q_j|))\big)
\Big)
\end{array}\]
variables, and its size (before conversion to CNF) is
\[
\begin{array}{l}
\mathcal{O}\Big(
|Q|^2 \cdot b^2 \cdot 2^{|\inpv|} \cdot (d + \log(b\cdot |Q|)) + \\
\phantom{\mathcal{O}(}\sum_{j=1}^n\big(|Q_j|^2 \cdot b^2 \cdot 2^{|\inpv|} \cdot (d_j + r_j + \log(b\cdot |Q_j|))\big) +
\\
\phantom{\mathcal{O}(}\sum_{j=1}^n\big(|\widehat Q_j|^2 \cdot b^2 \cdot 2^{|\inpv|} \cdot (\widehat d_j + \log(b\cdot |\widehat Q_j|))\big)
\Big), 
\end{array}\]
\[
\begin{array}{lllllll}
\text{ where} &d &=& \max_{s,q,\inpval,q'}|\delta_{s,q,\inpval,q'}|,&
d_j &=& \max_{s,q,\inpval,q'}|\delta_{s,q,\inpval,q'}^j|,\\
&\widehat d_j &=& \max_{s,q,\inpval,q'}|\widehat \delta_{s,q,\inpval,q'}^j|, \text{ and } &
r_j &=& \max_{s,q,\inpval,q'}|\rej^j(s,q,q',\inpval)|.
\end{array}
\]
\end{proposition}
\subsection{Bounded Synthesis}\label{sec:bounded-synthesis}

A \emph{B\"uchi automaton} over a finite alphabet $\alphabet$ is a tuple $\autA = (Q,q_0,\delta,F)$, where $Q$ is a finite set of states, $q_0$ is the initial state, $\delta \subseteq Q \times \alphabet \times Q$ is the transition relation, and $F \subseteq Q$ is a subset of the set of states. A run of $\autA$ on an infinite word $w=\sigma_0\sigma_1\ldots \in \alphabet^\omega$ is an infinite sequence $q_0,q_1,\ldots$ of states, where $q_0$ is the initial state and for every $i \geq 0$ it holds that $(q_i,\sigma_i,q_{i+1}) \in \delta$. 

A run of a B\"uchi automaton is accepting if it contains infinitely many occurrences of states in $F$. A \emph{co-B\"uchi automaton} $\autA = (Q,q_0,\delta,F)$ differs from a B\"uchi automaton in the accepting condition: a run of a co-B\"uchi automaton is accepting if it contains only \emph{finitely many} occurrences of states in $F$. For a B\"uchi automaton the states in $F$ are called \emph{accepting states}, while for a co-B\"uchi automaton they are called \emph{rejecting states}.
A \emph{nondeterministic} automaton $\autA$ accepts a word $w \in \alphabet^\omega$ if \emph{some} run of $\autA$ on $w$ is accepting.
A \emph{universal} automaton $\autA$ accepts a word $w \in \alphabet^\omega$ if \emph{every} run of $\autA$ on $w$ is accepting.

The \emph{run graph} of a universal automaton $\autA = (Q,q_0,\delta,F)$ on a transition system $\trans = (S,s_0,\tau)$ is the unique graph $G = (V,E)$ with set of nodes $V = S \times Q$ and set of labelled edges $E \subseteq V \times \alphabet \times V$ such that $((s,q),\sigma,(s',q')) \in E$ iff $(q,\sigma,q') \in \delta$ and $\tau(s,\sigma\cap \inpv) = (s',\sigma\cap \outv)$.
That is, $G$ is the product of $\autA$ and $\trans$.

A run graph of a universal B\"uchi (resp.\ co-B\"uchi) automaton is accepting if every infinite path $(s_0,q_0),(s_1,q_1), \ldots$ contains infinitely many (resp. finitely) many occurrences of states $q_i$ in $F$. A transition system $\trans$ is accepted by a universal automaton $\autA$ if the unique run graph of $\autA$ on $\trans$ is accepting. We denote with  $\lang\autA$ the set of transition systems accepted by $\autA$.

The bounded synthesis approach is based on the following property.
\begin{lemma}[\cite{KupfermanV05}]\label{lem:ltl-ucba}
For every LTL formula $\varphi$ we can construct a universal co-B\"uchi automaton $\autA_\varphi$ that has at most $2^{O(|\varphi|)}$ states and is such that for every transition system $\trans$ it holds that $\trans \in \lang{\autA_\varphi}$ if and only if $\trans \models \varphi$.
\end{lemma}

An \emph{annotation} of a transition system $\trans = (S,s_0,\tau)$  with respect to a universal co-B\"uchi automaton $\autA = (Q,q_0,\delta,F)$ is a function $\anot : S \times Q \to \natsbot$ that maps nodes of the run graph of $\autA$ on $\trans$ to the set $\natsbot$. Intuitively, such an annotation is valid if every node $(s,q)$ that is reachable from the node $(s_0,q_0)$ is annotated with a natural number, which is an upper bound on the number of rejecting states on any path from $(s_0,q_0)$ to $(s,q)$. 

Formally, an annotation $\anot : S \times Q \to \natsbot$ is \emph{valid} if
\begin{itemize}
\item $\anot(s_0,q_0) \neq \bot$, i.e., the pair of initial states is labelled with a number, and 
\item whenever $\anot(s,q) \neq \bot$, then for every edge $((s,q),\sigma,(s',q'))$ in the run graph of $\autA$ on $\trans$ we have that $(s',q')$ is annotated with a number (i.e., $\anot(s',q')\neq \bot$), such that
$\anot(s',q') \geq  \anot(s,q)$, and if $q' \in F$, then $\anot(s',q') >  \anot(s,q)$.
\end{itemize}

Valid annotations of finite-state systems correspond to accepting run graphs. An annotation $\anot$ is $c$-bounded if $\anot(s,q) \in \{0,\ldots,c\}\cup\{\bot\}$ for all $s \in S$ and $q \in Q$.\looseness=-1

The synthesis method proposed in \cite{ScheweF07a,FinkbeinerS13} employs the following result in order to 
reduce the bounded synthesis problem to checking the satisfiability of propositional formulas. A transition system $\trans$ is accepted by a universal co-B\"uchi automaton $\autA = (Q,q_0,\delta,F)$ iff there exists a $(|\trans|\cdot|F|)$-bounded valid annotation for $\trans$ and $\autA$. One can estimate a bound on the size of the transition system, which allows to reduce the synthesis problem to its bounded version. Namely, if there exists a transition system that satisfies an LTL formula $\varphi$, then there exists a transition system  satisfying $\varphi$ with  at most $\big(2^{(|\subf\varphi| +\log |\varphi|)}\big)!^2$ states.
\looseness=-1

Let $\autA = (Q,q_0,\delta,F)$ be a universal co-B\"uchi automaton for the LTL formula $\spec$.
Given a bound $b$ on the size of the sought transition system $\trans$, the bounded synthesis problem can be encoded as a satisfiability problem with the following sets of propositional variables and constraints.

{\bf Variables:} The variables represent the sought transition system $\trans$, and the sought valid annotation $\anot$ of the  run graph of $\autA$ on $\trans$. A transition system with $b$ states $S = \{1,\ldots,b\}$ is represented by  Boolean variables $\tau_{s,\inpval,s'}$ and $o_{s,\inpval}$ for every $s, s' \in S$, $\inpval \in \ialphabet$, and output proposition $o \in \outv$. The variable $\tau_{s,\inpval,s'}$ encodes the existence of transition from $s$ to $s'$ on input $\inpval$, and the variable $o_{s,\inpval}$ encodes $o$ being true in the output from state $s$ on input $\inpval$.

The annotation $\anot$ is  represented by the following variables. For each $s\in S$ and $q \in Q$, the annotation is represented by a Boolean variable $\anotb_{s,q}$ and a vector $\anotn_{s,q}$ of $\log(b\cdot |F|)$ Boolean variables: the variable $\anotb_{s,q}$ encodes the reachability of $(s,q)$ from the initial node in the corresponding run graph, and the vector of variables $\anotn_{s,q}$ represents the bound for the node $(s,q)$. 

{\bf Constraints for input-enabled $\trans$}:
$C_\tau \defeq\bigwedge_{s \in S}\bigwedge_{\inpval \in \ialphabet}\bigvee_{s' \in S} \tau_{s,\inpval,s'}$.

{\bf Constraints for valid annotation:}\\
$
\begin{array}{lll}
C_\anot & \defeq & 
\anotb_{s_0,q_0} \wedge\\&& 
\bigwedge_{q,q' \in Q}\bigwedge_{s,s' \in S}\bigwedge_{\inpval \in \ialphabet}
\Big( 
\big(
\anotb_{s,q} \wedge 
\delta_{s,q,\inpval,q'} \wedge 
\tau_{s,\inpval,s'}
\big) \rightarrow 
\succa_\anot(s,q,s',q')
\Big),
\end{array}
$\\
where $\delta_{s,q,\inpval,q'}$ is a formula over the variables $o_{s,\inpval}$ that characterizes the transitions in $\autA$ between  $q$ and $q'$ on labels consistent with $\inpval$, and
$\succa_\anot(s,q,s',q')$ is a formula  over the annotation variables such that
$\succa_\anot(s,q,s',q') \defeq (\anotb_{s',q'} \wedge (\anotn_{s',q'} > \anotn_{s,q}))$ if $q' \in F$, and
$\succa_\anot(s,q,s',q') \defeq (\anotb_{s',q'} \wedge (\anotn_{s',q'} \geq \anotn_{s,q}))$ if $q' \not\in F$.

\subsection{Maximum Satisfiability (MaxSAT)}\label{sec:prelim-maxsat}
While the bounded synthesis problem can be encoded into SAT, for the synthesis of a transition system that satisfies a set of soft specifications as well as possible, we need to solve an optimization problem. In the next section we will reduce the bounded maximum realizability problem to a \emph{partial weighted MaxSAT problem}.

\emph{MaxSAT} is a Boolean optimization problem. Similarly to SAT, instances of MaxSAT are given as propositional formulas in conjunctive normal form (CNF). That is, a MaxSAT instance is a conjunction of clauses, each of which is a disjunction of literals, where a literal is a Boolean variable or its negation. The objective in MaxSAT is to compute a variable assignment that maximizes the number of satisfied clauses. In \emph{weighted MaxSAT}, each clause is associated with a positive numerical weight and the objective is now to maximize the sum of the weights of the satisfied clauses. Finally, in \emph{partial weighted MaxSAT}, there are two types of clauses, namely \emph{hard} and \emph{soft} clauses, where only the soft clauses are associated with weights. In order to be a solution to a partial weighted MaxSAT formula, a variable assignment must satisfy all the hard clauses. An optimal solution additionally maximizes the sum of the weights of the soft clauses.
 
In the encoding in the next section we use hard clauses for the hard specification, and soft clauses to capture the soft specifications in the maximum realizability problem. The weights for the soft clauses  will encode the lexicographic ordering  on values of conjunctions of soft specifications. 
\subsection{Specifications, Transition Systems, and the Synthesis Problem}\label{sec:basic-definitions}


Linear-time temporal logic (LTL) is a standard specification language for formalizing requirements on the behaviour of reactive systems. Given a finite set $\props$ of atomic propositions, the set of LTL formulas is generated by the grammar
$\varphi := p \mid \true \mid \false \mid \neg \varphi \mid \varphi_1 \wedge \varphi_2 \mid \varphi_1 \vee \varphi_2 \mid \LTLnext  \varphi  \mid \varphi_1 \LTLuntil \varphi_2 \mid \varphi_1 \LTLrelease \varphi_2,$
where $p \in \props$  is an atomic proposition, $\LTLnext$ is the \emph{next} operator, $\LTLuntil$ is the \emph{until} operator, and $\LTLrelease$ is the \emph{release} operator. As usual, we  define the derived operators 
\emph{finally}: $\LTLfinally \varphi = \true \LTLuntil \varphi$ and 
\emph{globally}: $\LTLglobally \varphi = \false \LTLrelease \varphi$. An LTL formula $\varphi$ is in negation normal form (NNF) if all the negations appear only in front of atomic propositions. Since every LTL formula can be converted to an equivalent one in NNF, we consider only formulas in NNF.
A \emph{syntactically safe} LTL formula is an LTL formula which contains no occurrences of the $\LTLuntil$ operator in its NNF. 

Let $\Sigma = 2^{\props}$ be the finite alphabet consisting of the valuations of the propositions $\props$. A letter $\sigma \in \Sigma$ is interpreted as the valuation that assigns value $\trueval$ to all $p \in \sigma$ and $\falseval$ to all $p \in \props \setminus \sigma$. LTL formulas are interpreted over infinite words $w \in\alphabet^\omega$. If a word $w \in \alphabet^\omega$ satisfies an LTL formula $\varphi$, we write $w \models \varphi$. The definition of the semantics of LTL can be found for instance in~\cite{BaierKatoen08}. 
We denote with $|\varphi|$ the length of $\varphi$, and with $\subf\varphi$ the set of its subformulas.

In the rest of the paper we assume that the set $\props$ of atomic propositions is partitioned into disjoint sets of \emph{input} propositions $\inpv$ and \emph{output} propositions $\outv$.

A \emph{transition system} over a set of input propositions $\inpv$ and a set of output propositions $\outv$ is a tuple $\trans = (S,s_0,\tau)$, where $S$ is a set of states, $s_0$ is the initial state, and the transition function $\tau : S \times \ialphabet \to S \times \oalphabet$ maps a state $s$ and a valuation $\inpval \in \ialphabet$ of the input propositions  to a successor state $s'$ and a valuation $\outval \in \oalphabet$ to the output propositions. 
Let $\props = \inpv \cup \outv$ be the set of all propositions. For $\sigma \in \Sigma = 2^{\props}$ we denote $\sigma \cap \inpv$ by $\inpval$, and $\sigma \cap \outv$ by $\outval$.

If the set $S$ is finite, then $\trans$ is a finite-state transition system. In this case we define the size $|\trans|$ of $\trans$ to be the number of its states, i.e.,  $|\trans| \defeq |S|$.

An \emph{execution} of $\trans$ is an infinite sequence $s_0, (\inpval_0 \cup \outval_0), s_1, (\inpval_1 \cup \outval_1), s_2\ldots$ such that $s_0$ is the initial state, and $(s_{i+1},\outval_i) = \tau(s_i,\inpval_i)$ for every $i \geq 0$. The corresponding sequence $(\inpval_0 \cup \outval_0),(\inpval_1 \cup \outval_1),\ldots \in \alphabet^\omega$ is called a trace. We denote with $\Traces(\trans)$ the set of all traces of a transition system $\trans$. 

We say that a transition system $\trans$ satisfies an LTL formula $\varphi$ over atomic propositions $\props = \inpv \cup \outv$, denoted $\trans \models \varphi$, if $w \models \varphi$ for every $w \in \Traces(\trans)$.

The \emph{realizability problem for LTL} is to determine whether for a given LTL formula $\varphi$ there exists a transition system $\trans$ that satisfies $\varphi$. The \emph{LTL synthesis problem} asks to construct such a transition system if one exists.

Often, the specification  is a combination of multiple requirements,  which might not be realizable in conjunction. In such a case, in addition to reporting the unrealizability to the system designer, we would like the synthesis procedure to construct an implementation that satisfies the specification ``as much as possible''. Such implementation is particularly useful in the case where some of the requirements  describe desirable but not necessarily essential properties of the system. To determine what ``as much as possible'' formally means, a quantitative semantics of the specification language is necessary. In the next subsection we provide such semantics for a fragment of LTL. The quantitative interpretation is based on the semantics of LTL formulas of the form $\gphi$.

\subsection{Quantitative Semantics of Soft Safety Specifications}\label{sec:quantitative-semantics}
Let $\gphi_1,\ldots,\gphi_n$ be LTL specifications, where each $\softSpec_i$ is a syntactically safe LTL formula. In order to formalize the maximal satisfaction of $\gphi_1\wedge\ldots\wedge\gphi_n$, we first give a quantitative semantics of formulas of the form $\gphi$.

\vspace{-.3cm}
\paragraph{Quantitative semantics of safety specifications.} 
For an LTL formula of the form $\gphi$ and a transition system $\trans$, we define \emph{the value $\val\trans{\gphi}$ of $\gphi$ in $\trans$} as
\[
\val\trans\gphi \defeq
\begin{cases}
(1,1,1) & \text{if } \trans\models\LTLglobally\varphi,\\
(0,1,1) & \text{if } \trans\not\models\LTLglobally\varphi \text{ and } \trans\models\LTLfinally\LTLglobally\varphi,\\
(0,0,1) & \text{if } \trans\not\models\LTLglobally\varphi \text{ and } \trans\not\models\LTLfinally\LTLglobally\varphi, \text{ and }\trans\models\LTLglobally\LTLfinally\varphi,\\
(0,0,0) & \text{if } \trans\not\models\LTLglobally\varphi, \text{ and } \trans\not\models\LTLfinally\LTLglobally\varphi, \text{ and }\trans\not\models\LTLglobally\LTLfinally\varphi.\\
\end{cases}
\]

Thus, the value of $\gphi$ in a transition system $\trans$ is a vector $(v_1,v_2,v_3) \in \{0,1\}^3$, where the value $(1,1,1)$ corresponds to the $\true$ value in the classical semantics of LTL. When $\trans\not\models\gphi$, the values $(0,1,1)$, $(0,0,1)$ and $(0,0,0)$ capture the extent to which $\varphi$ holds or not along the traces of $\trans$. For example, if $\val\trans\gphi =(0,0,1)$, then $\varphi$ holds infinitely often on each trace of $\trans$, but there exists a trace of $\trans$ on which $\varphi$ is violated infinitely often. When $\val\trans\gphi =(0,0,0)$, then on some trace of $\trans$, $\varphi$ holds for at most finitely many positions.

Note that by the definition of $\mathit{val}$, if $\val\trans\gphi = (v_1,v_2,v_3)$, then
\emph{(1)} $v_1=1$ iff $\trans\models \gphi$,
\emph{(2)} $v_2=1$ iff $\trans\models \fgphi$, and
\emph{(3)} $v_3=1$ iff $\trans\models \gfphi$.
Thus, the lexicographic ordering on $\{0,1\}^3$ captures the preference of one transition system over another with respect to the  quantitative satisfaction of $\gphi$.

\begin{example}\label{ex:one-safety}
Consider a robot working as a museum guide. We want to synthesize a transition system representing a navigation strategy for the robot. One of the requirements is that its tour should visit the special exhibition infinitely often, formalized in LTL as $\LTLglobally\LTLfinally \specex$. We also desire that the robot never enters the staff's office, formalized as $\LTLglobally\neg\office$. Now, suppose that initially the key for the special exhibition is in the office. Thus, in order to satisfy $\LTLglobally\LTLfinally \specex$, the robot must violate $\LTLglobally\neg\office$. In any case, a strategy in which the office is entered only once, which satisfies $\fg \neg\office$ is preferable to one which enters the office over and over again, and only satisfies $\gf\neg\office$.
Thus, we want to synthesize a strategy $\trans$ with maximal value $\val\trans{\LTLglobally\neg\office}$.
\end{example}

\vspace{-.2cm}
In order to compare implementations with respect to their satisfaction of a conjunction $\gphi_1 \wedge \ldots \wedge \gphi_n$ of several safety specifications, we will extend the above definition. We consider the case when the specifier has not expressed any preference for the individual conjuncts. Consider the following example.

\vspace{-.2cm}
\begin{example}\label{ex:two-safety} We consider again the museum guide robot, now with two soft safety specifications. The specification $\LTLglobally (\occupied \rightarrow \neg \enter\_{\passage})$ requires that the robot does not enter the narrow passage if it is occupied. The second one, $\LTLglobally \neg\enter\_\library$, requires that the robot never enters the library. Passing through the library is an alternative to using the passage. Now, unless these specifications are given priorities, it is preferable to satisfy each of $(\occupied \rightarrow \neg \enter\_{\passage})$ and $\neg\enter\_\library$ infinitely often, rather than avoid entering the library by going through a occupied passage every time, or vice versa. 
\end{example}

\vspace{-.3cm}
\paragraph{Quantitative semantics of conjunctions.} 
To capture the idea illustrated in Example~\ref{ex:two-safety}, we define a value function, which intuitively 
gives higher values to transition systems in which a fewer number of soft specifications have low values. Formally, let \emph{the value of $\gphi_1 \wedge \ldots \wedge \gphi_n$ in $\trans$} be
\[\val\trans{\gphi_1 \wedge \ldots \wedge \gphi_n} \defeq \big(
\sum_{i=1}^n v_{i,3},
\sum_{i=1}^n v_{i,2},
\sum_{i=1}^n v_{i,1}
\big),\] 
where
$\val\trans{\gphi_i} = (v_{i,1},v_{i,2},v_{i,3})$ for $i \in \{1,\ldots,n\}$. To compare transition systems according to these values, we use lexicographic ordering on $\{0,\ldots,n\}^3$.

\begin{example}\label{ex:two-safety-val}  For the specifications in Example~\ref{ex:two-safety}, the value function defined above assigns value $(2,0,0)$ to a  system that satisfies  $\gf (\occupied \rightarrow \neg \enter\_{\passage})$ and $\gf\neg\enter\_\library$, but satisfies neither of $\fg (\occupied \rightarrow \neg \enter\_{\passage})$ and $\fg\neg\enter\_\library$. It assigns the smaller value $(1,1,1)$
to an implementation that satisfies $\LTLglobally (\occupied \rightarrow \neg \enter_{\passage})$, but not $\gf\neg\enter\_\library$.
\end{example}

Note that in the definition above we have reversed the order of the sums of the values $v_1, v_2$ and $v_3$, with the sum over  $v_3$ being the first, and the sum over $v_1$ being last. In this way, a transition system that satisfies all soft requirements to some extent is considered better in the lexicographic ordering than a transition system that satisfies one of them and violates all the others. We could instead consider the inverse lexicographic ordering, thus giving preference to satisfying some soft specification, over having some lower level of satisfaction over all of them. The next example illustrates the differences between these two variations.

\begin{example}\label{ex:ordering}
For the two soft specifications from Example~\ref{ex:two-safety}, reversing the order of the sums in the definition of $\val\trans{\gphi_1 \wedge \ldots \wedge \gphi_n}$ results in giving the higher value $(1,1,1)$ to a transition system that satisfies $\LTLglobally (\occupied \rightarrow \neg \enter\_{\passage})$ but not $\gf\neg\enter\_\library$, and the lower value $(0,0,2)$ to the one that guarantees only $\gf (\occupied \rightarrow \neg \enter\_{\passage})$ and $\gf\neg\enter\_\library$. The most suitable ordering usually depends on the specific application. 
\end{example}

In Appendix~\ref{sec:generalizations} we discuss generalizations of the framework, where
the user provides a set of relaxations for each of the soft specifications, and possibly a priority ordering among the soft specifications, or numerical weights.

\vspace{-.3cm}
\subsection{Maximum realizability}\label{sec:max-realizability}
Using the definition of quantitative satisfaction of soft safety specifications, we now define the maximum realizability problem, which asks to synthesize a transition system that satisfies a given \emph{hard} LTL specification, and is optimal with respect to the satisfaction of a conjunction of \emph{soft} safety specifications.

{\bf Maximum realizability problem:} Given an LTL formula $\spec$ and formulas $\gphi_1,\ldots,\gphi_n$, where each $\softSpec_i$ is a syntactically safe LTL formula, the maximum realizability problem asks to determine if there exists a transition system $\trans$ such that $\trans \models \spec$, and if the answer is positive, to synthesize a transition system $\trans$ such that $\trans \models \spec$, and such that for every transition system $\trans'$ with $\trans'\models \spec$ it holds that $\val\trans{\gphi_1 \wedge \ldots \wedge \gphi_n} \geq \val{\trans'}{\gphi_1 \wedge \ldots \wedge \gphi_n}$.

{\bf Bounded maximum realizability problem:} Given an LTL formula $\spec$ and formulas $\gphi_1,\ldots,\gphi_n$, where each $\softSpec_i$ is a syntactically safe LTL formula, and a bound $b$, the bounded maximum realizability problem asks to determine if there exists a transition system $\trans$ with $|\trans| \leq b$ such that $\trans \models \spec$, and if the answer is positive, to synthesize a transition system $\trans$ such that $\trans \models \spec$, $|\trans| \leq b$ and such that for every transition system $\trans'$ with $\trans'\models \spec$ and $|\trans'| \leq b$, it holds that $\val\trans{\gphi_1 \wedge \ldots \wedge \gphi_n} \geq \val{\trans'}{\gphi_1 \wedge \ldots \wedge \gphi_n}$.

