DCSYNTH: Guided Reactive Synthesis with Soft Requirements

TL;DR

This paper introduces DCSYNTH, a framework and tool for guided reactive controller synthesis using soft and hard requirements expressed in QDDC logic, enabling the creation of high-quality controllers that satisfy complex specifications.

Contribution

It presents a novel method for synthesizing controllers guided by soft requirements in QDDC logic, handling conflicting specifications and optimizing controller quality.

Findings

Effective synthesis of controllers satisfying hard and soft requirements.

Ability to handle conflicting and unrealizable specifications.

Demonstrated high-quality controllers through case studies.

Abstract

In reactive controller synthesis, a number of implementations (controllers) are possible for a given specification because of the incomplete nature of specification. To choose the most desirable one from the various options, we need to specify additional properties which can guide the synthesis. In this paper, We propose a technique for guided controller synthesis from regular requirements which are specified using an interval temporal logic QDDC. We find that QDDC is well suited for guided synthesis due to its superiority in dealing with both qualitative and quantitative specifications. Our framework allows specification consisting of both hard and soft requirements as QDDC formulas. We have also developed a method and a tool DCSynth, which computes a controller that invariantly satisfies the hard requirement and it optimally meets the soft requirement. The proposed technique is also useful in dealing with conflicting i.e., unrealizable requirements, by making some of them as soft requirements. Case studies are carried out to demonstrate the effectiveness of the soft requirement guided synthesis in obtaining high-quality controllers. The quality of the synthesized controllers is compared using metrics measuring both the guaranteed and the expected case behaviour of the controlled system. Tool DCSynth facilitates such comparison.

Figures

Tables

Table 1. Table 1: Synthesis from Mine-pump(8,2,6,2) and Arb(5,3,2) specifications in DCSynth. The last column gives the expected value of commitment in long run on random inputs.

	DCSynth Specification		Synthesis (States/Time)
Sr	Controller	Output	MPS	MPHOS	Controller	Expected
No	type	Ordering	Stats	Stats	Stats	Value
$\mathrm{𝐌𝐢𝐧𝐞}-\mathrm{𝐩𝐮𝐦𝐩}(\mathrm{𝟖},\mathrm{𝟐},\mathrm{𝟔},\mathrm{𝟐})$
1	$Type0$	-	Unrealizable
2	$Type1$	$PUMPON$	70/0.00045	70/0.00254	21/0.00220	0.0
3	$Type2$	$PUMPON$	1/0.00004	10/0.00545	10/0.00033	0.99805
4	$Type3$	$PUMPON$	70/0.00045	75/0.044216	73/0.00081	0.99805
5	$Type1$	$!\left(PUMPON\right)$	70/0.00045	70/0.00254	47/0.00230	0.0
6	$Type2$	$!\left(PUMPON\right)$	1/0.00004	10/0.00545	10/0.00019	0.99805
7	$Type3$	$!\left(PUMPON\right)$	70/0.00045	75/0.044216	73/0.00082	0.99805
$\mathrm{𝐀𝐫𝐛}(\mathrm{𝟓},\mathrm{𝟑},\mathrm{𝟐})$
1	$Type0$	-	Unrealizable
2	$Type1$	$ArbDef$	13/0.000226	13/0.004794	11/0.007048	0.0
3	$Type2$	$ArbDef$	1/0.00001	207/1.864346	201/0.058423	0.9930985
4	$Type3$	$ArbDef$	13/0.000213	207/1.897907	201/0.057062	0.9930985

Table 2. Table 2: Automatic Ring-Back Sequence for Alarm Annunciation

Input	Lamp Output	Audio Output
Normal to Alarm	Fast Flashing	Normal Alarm Hooter On
Acknowledged	Lamp On	Normal Alarm Hooter Off
Alarm to Normal	Slow Flashing	Ringback Hooter On
Reset	Lamp Off	Ringback Hooter Off

Table 3. Table 3: MPS Synthesis: Enumeration vs symbolic method (time in seconds). For 𝒜 ​ ( D h ) 𝒜 superscript 𝐷 ℎ \mathcal{A}(D^{h}) we give number of states and time to compute it from the Q ​ D ​ D ​ C 𝑄 𝐷 𝐷 𝐶 QDDC hard requirement formula. For M ​ P ​ S ​ ( D h ) 𝑀 𝑃 𝑆 superscript 𝐷 ℎ MPS(D^{h}) we give its number of states and time to compute it using the two methods. S t subscript 𝑆 𝑡 S_{t} , T s subscript 𝑇 𝑠 T_{s} , E ​ n 𝐸 𝑛 En and S ​ y 𝑆 𝑦 Sy represent total no. of states, time in seconds, enumerative method and symbolic method respectively. The Example A ​ r ​ b h ​ a ​ r ​ d ​ ( n , k ) 𝐴 𝑟 superscript 𝑏 ℎ 𝑎 𝑟 𝑑 𝑛 𝑘 Arb^{hard}(n,k) represents the specification T ​ y ​ p ​ e ​ 0 ​ ( A ​ r ​ b ​ ( n , k , n ) ) 𝑇 𝑦 𝑝 𝑒 0 𝐴 𝑟 𝑏 𝑛 𝑘 𝑛 Type0(Arb(n,k,n)) and A ​ r ​ b s ​ o ​ f ​ t ​ ( n , k ) 𝐴 𝑟 superscript 𝑏 𝑠 𝑜 𝑓 𝑡 𝑛 𝑘 Arb^{soft}(n,k) represents the example T ​ y ​ p ​ e ​ 2 ​ ( A ​ r ​ b ​ ( n , k , n ) ) 𝑇 𝑦 𝑝 𝑒 2 𝐴 𝑟 𝑏 𝑛 𝑘 𝑛 Type2(Arb(n,k,n)) .

Example	Hard Requirement	$𝒜\left(D^h\right)$		$MPS\left(D^h\right)$
		$S_t$	$T_s$	$S_t$	$T_s$	$T_s$
					($En$)	($Sm$)
$Ar{b}^{hard}(4,4)$	$ARBHARD(4,4)$	177	0.04	126	0.025563	0.002033
$Ar{b}^{hard}(5,5)$	$ARBHARD(5,5)$	2103	0.43	1297	0.59	0.04
$Ar{b}^{hard}(6,6)$	$ARBHARD(6,6)$	31033	9.22	16808	42.75	0.91
$Ar{b}^{soft}(4,2)$	$ARBINV\left(4\right)$	3	0.016	2	6.2E-4	7.6E-5
$Ar{b}^{soft}(5,3)$	$ARBINV\left(5\right)$	3	0.020	2	1.9E-3	1.2E-4
$Minepump(8,2,10,1)$	$MineAssume(2,10,1)$	271	0.08	211	1.4E-2	5.8E-3
	$\Rightarrow ArbCommit\left(8\right)$

Table 4. Table 4: Comparison of Synthesis in Acacia+, BoSy and DCSynth, in terms of controller computation time and memory and number of states of the controller automaton. M ​ i ​ n ​ e ​ p ​ u ​ m ​ p 𝑀 𝑖 𝑛 𝑒 𝑝 𝑢 𝑚 𝑝 Minepump as well as A ​ r ​ b t ​ o ​ k ​ ( n ) 𝐴 𝑟 superscript 𝑏 𝑡 𝑜 𝑘 𝑛 Arb^{tok}(n) specifications can be found in Appendix 0.A.1 .

	Acacia+		BoSy		DCSynth
Hard Requirement	time(Sec)	Memory /	time(Sec)	Memory /	time(Sec)	Memory /
		States		States		States
$Ar{b}^{hard}(4,4)$	0.4	29.8/ 55	0.75	-/4	0.08	9.1/ 50
$Ar{b}^{hard}(5,5)$	11.4	71.9/ 293	14.5	-/8	5.03	28.1/ 432
$Ar{b}^{hard}(6,6)$	TO555TO=timeout(DCSynth and Acacia+ 3600secs, BoSy 600secs)	-	TO	-	80	1053.0/ 4802
$Ar{b}^{tok}\left(7\right)$	9.65	39.1/ 57	TO	-	0.3	7.3/ 7
$Ar{b}^{tok}\left(8\right)$	46.44	77.9/ 73	-	-	2.2	16.2/ 8
$Ar{b}^{tok}\left(10\right)$	NC666NC=synthesis inconclusive	-	-	-	152	82.0/ 10
Mine-pump	NC	-	TO	-	0.06	50/ 32

Table 5. Table 5: Worst Case Response Time Analysis using CTLDC using Response Formula MAXLEN([[ r ​ e ​ q i 𝑟 𝑒 subscript 𝑞 𝑖 req_{i} && ! a ​ c ​ k i 𝑎 𝑐 subscript 𝑘 𝑖 ack_{i} ]]) computation. The value of H 𝐻 H is specified only for A ​ r ​ b s ​ o ​ f ​ t 𝐴 𝑟 superscript 𝑏 𝑠 𝑜 𝑓 𝑡 Arb^{soft}

Sr.No	Arbiter Variant	Horizon (H)	Computed Response
			Response for $i^{th}$ cell	Value (in cycles)
1	$Ar{b}^{hard}(5,5)$	-	$1\le i\le 5$	5
2	$Ar{b}^{hardAssume}(5,3,2)$	-	i = 1	2
3			$2\le i\le 5$	3
4	$Ar{b}^{soft}(5,3)$	(H = 1)	$1\le i\le 4$	$\infty$
5			i = 5	3
6	$Ar{b}^{soft}(5,3)$	(H = 2)	$1\le i\le 3$	$\infty$
7			$4\le i\le 5$	3
8	$Ar{b}^{soft}(5,3)$	(H $>=$ 3)	$1\le i\le 2$	$\infty$
9			$3\le i\le 5$	3

Equations

$$\phi :=false|true|p\in PV|!\phi |\phi \&\&\phi |\phi ||\phi$$

$$\begin{array}[]{lc}D:=&\langle\varphi\rangle\ |\ [\varphi]\ |\ [[\varphi]]\ |\ D\ \verb|^|\ D\ |\ !D\ |\ D~{}||~{}D\ |\ D~{}\&\&~{}D\\ &ex~{}p.\ D\ |\ all~{}p.\ D\ |\ slen\bowtie c\ |\ scount\ \varphi\bowtie c\ |\ sdur\ \varphi\bowtie c\end{array}$$

$$\begin{array}[]{lcl}\sigma,[b,e]\models\langle\varphi\rangle&\mathrm{\ iff\ }&b=e\mbox{ and }\sigma,b\models\varphi,\\ \sigma,[b,e]\models[\varphi]&\mathrm{\ iff\ }&b<e\mbox{ and }\forall b\leq i<e:\sigma,i\models\varphi,\\ \sigma,[b,e]\models[[\varphi]]&\mathrm{\ iff\ }&\forall b\leq i\leq e:\sigma,i\models\varphi,\\ \sigma,[b,e]\models\{\{\varphi\}\}&\mathrm{\ iff\ }&e=b+1\mbox{ and }\sigma,b\models\varphi,\\ \sigma,[b,e]\models D_{1}\verb|^|D_{2}&\mathrm{\ iff\ }&\exists b\leq i\leq e:\sigma,[b,i]\models D_{1}\mbox{ and }\sigma,[i,e]\models D_{2},\\ \end{array}$$

$$Ind(D,w)=pref(EP(w)\iff D)$$

$$\begin{array}[]{l}ValAvgMax(s)~{}=~{}\mathbb{E}_{ii\in(2^{I})^{H}}~{}VMAX(s,ii)\\ ValAvgMin^{\pi}(s)~{}=~{}\mathbb{E}_{ii\in(2^{I})^{H}}~{}VMIN^{\pi}(s,ii)\end{array}$$

$$\begin{array}[]{l}Val(s,0)=0\\ Val(s,p+1)=\mathbb{E}_{i\in 2^{I}}~{}~{}max_{o\in 2^{(O\cup\{w\})}~{}:~{}\delta(s,(i,o))\neq r}{}\\ \hskip 113.81102pt\{wt(o)~{}+~{}Val(\delta(s,(i,o)),p)\}\end{array}$$

$$\begin{array}[]{l}F^{*}(s,i)=argmax_{o\in 2^{O}}\{wt(o)~{}+~{}Val(s,H)\\ \hskip 56.9055pt~{}\mid~{}\delta_{\mathcal{A}^{Arena}}(s,(i,o))=s^{\prime}\land s^{\prime}\not=r\}\end{array}$$

$$\begin{array}[]{l}Mutex(n)=true\textrm{\textasciicircum}\langle~{}\land_{i\neq j}~{}\neg(a_{i}\land a_{j})~{}\rangle,~{}1\leq i\leq n\\ NoLoss(n)=true\textrm{\textasciicircum}\langle~{}~{}(\lor_{i}r_{i})\Rightarrow(\lor_{j}a_{j})~{}\rangle,~{}1\leq i\leq n\\ NoSpurious(n)=true\textrm{\textasciicircum}\langle~{}~{}\land_{i}~{}(a_{i}\Rightarrow r_{i})~{}~{}\rangle,~{}1\leq i\leq n\\ ARBINV(n)=Mutex(n)\land NoLoss(n)\land NoSpurious(n).\end{array}$$

$$\begin{array}[]{l}Resp(r,a,k)=true\textrm{\textasciicircum}(([[r]]\ \&\&\ (slen=(k-1)))~{}\Rightarrow\\ \hskip 56.9055pttrue\textrm{\textasciicircum}(scount\ a>0\ \&\&\ (slen=(k-1)))\\ ArbResp(n,k)=(\land_{1\leq i\leq n}~{}(Resp(r_{i},a_{i},k))\\ ArbCommit(n,k)=ARBINV(n)\land ArbResp(n,k)\end{array}$$

$$Ar{b}^{hard}(n,k)=(\{r_1,\dots ,r_n\},\{a_1,\dots ,a_n\},ArbCommit(n,k),⟨⟩)$$

$$Arb^{hardAssume}(n,k,i)=\begin{array}[t]{l}(\{r_{1},\ldots,r_{n}\},\{a_{1},\ldots,a_{n}\},\\ \mathit{pref}(ArbAssume(n,i))\Rightarrow EP(ArbCommit(n,k)),\\ ~{}~{}\langle ArbCommit(n,k)\rangle~{})\end{array}$$

$$Arb^{soft}(n,k)=\begin{array}[t]{l}(\{r_{1},\ldots,r_{n}\},\{a_{1},\ldots,a_{n}\},ARBINV(n),\\ ~{}~{}\langle Resp(r_{n},a_{n},k):2^{n},\ldots,Resp(r_{1},a_{1},k):2^{1}\rangle~{})\end{array}$$

$$\begin{array}[]{l}TokInit(n)=<tok_{1}\ \&\&\ (\land_{2\leq i\leq n}!tok_{i})>\textrm{\textasciicircum}\ true\\ TokCirculate(n)=[](\land_{1\leq i\leq n}({{tok_{i}}}\ \textrm{\textasciicircum}\ (slen=1)<=>\\ \hskip 170.71652pt(slen=1)\ \textrm{\textasciicircum}\ {{tok_{i\%n+1}}}))\\ TokResp(n)=\land_{1\leq i\leq n}[[(r_{i}\ \&\&\ tok_{i})=>a_{i}]]\\ Token(n)=TokInit(n)\land TokCirculate(n)\land TokResp(n).\\ \end{array}$$

$$Ar{b}^{tok}(n)=(\{r_1,\dots ,r_n\},\{a_1,\dots ,a_n\},ARBTOKEN(n),⟨⟩,⟨⟩)$$

$${\models }_{qddc}\forall I(\left[\forall O.D(S_1)\wedge C)\right]\Rightarrow \left[\forall O.(D(S_1)\wedge C)\right])$$

Full text

We have also developed a method and a tool DCSynth, which computes a controller that invariantly satisfies the hard requirement and it optimally meets the soft requirement. The proposed technique is also useful in dealing with conflicting i.e., unrealizable requirements, by making some of the them as soft requirements. Case studies are carried out to demonstrate the effectiveness of the soft requirement guided synthesis in obtaining high quality controllers. The quality of the synthesized controllers is compared using metrics measuring both the guaranteed and the expected case behaviour of the controlled system. Tool DCSynth facilitates such comparison.

1 Introduction

Reactive synthesis aims at constructing a controller (say a Mealy Machine) algorithmically from a given temporal logic specification of its desired behaviour. Considerable amount of research has gone into the area of reactive synthesis and several tools are available for experimenting with reactive synthesis[13]. However, existing tools do not have the capability to guide the synthesis towards the most desirable controller. In practice, user specification may be incomplete and it may contain certain requirements, which are not mandatory, but desirable. We term the desirable properties as soft requirements.

In this work, we propose a specification consisting of hard requirement which are mandatory and needs to be satisfied invariantly, and the soft requirement which are desirable and should be satisfied at as many points in the execution as possible. We choose to specify the hard and soft requirements as regular properties in logic Quantified Discrete Duration Calculus(QDDC)[20, 21]. QDDC is the discrete time variant of Duration Calculus proposed by Zhou et.al. [8, 33].

Regular properties can conceptually be specified by a deterministic finite state automaton (DFA). At any point in the execution, a regular property holds provided the past behaviour upto the point is accepted by its DFA. The study of synthesis of controllers for such properties was pioneered by Ramadge and Wonham [25, 26, 18]. QDDC is an interval temporal logic, which has the expressive power of regular languages. Section 2 presents the syntax and semantics of this logic. Prior work [17, 21, 20] shows that any formula in QDDC can be effectively translated into a language equivalent DFA over finite words. Logic QDDC’s bounded counting features, interval based modalities and regular expression like primitives allow complex qualitative and quantitative properties (such as latency, resource constraints) to be specified succinctly and modularly (see the example below). With illustrations, papers [19, 21, 22] show how quantitative and qualitative regular properties can be succinctly specified in QDDC. Paper [19] also gives a comparison with other logics such as LTL and PSL. It should be noted that QDDC does not allow specification of general liveness properties, however, time bounded liveness can be specified. The following example motivates need for soft requirement guided synthesis.

Example 1 (Arbiter for Mutually Exclusive Shared Resource)

The arbiter has an input $r_{i}$ (denoting request for access) and an output $a_{i}$ (denoting acknowledgement for access) for each client $1\leq i\leq n$. The specification consists of the following two properties, given as QDDC formulas together with their intuitive explanation. Section 2 gives the formal syntax and semantics of QDDC.

$-$Mutual Exclusion Requirement $R_{1}$: $[[~{}\land_{i\neq j}~{}\neg(a_{i}\land a_{j})~{}]]$, states that at every point, the access to the shared resource should be mutually exclusive.

$-$k-cycle Response Requirement $R_{2}$: $[](\land_{i}~{}(([[r_{i}]]~{}\&\&\ (slen>=(k-1)))~{}\Rightarrow(scount~{}a_{i}>0))$ , states that in any observation interval spanning $k$ cycles if request from $i^{th}$ client ($r_{i}$) is continuously high during the interval, then that client should get at least one access ($a_{i}$) within the observation interval. Modality $[]D$ states that sub-formula $D$ should hold for all observation intervals. Term $slen$ gives the length of the observation interval and the term $(scount~{}P)$ counts the number of occurrences of proposition $P$ within the observation interval. The property $R2$ is asserted for each client $1\leq i\leq n$.

When $k<n$ no controller can satisfy both requirements (their conjunction is unrealizable); consider the case where all clients request all the time. We may want to opt for an implementation, which mandatorily satisfies $R1$ and it tries to meet the $R2$ “as much as possible”. This can be specified in our framework, by making requirement $R2$ as a soft requirement. One possible controller in such a case will make $a_{i}$ true in a round-robin manner for all the requesting clients. Let $r$ denote the number of clients requesting simultaneously. The round-robin policy will mandatorily satisfy $R2$ under the assumption that invariantly $r\leq k$. But when $r>k$ (overload condition), this controller will be able to meet the response time requirement $R2$ for only $k$ out of $n$ clients. Using the soft requirement, we can also given priority to the clients which meet response time requirements under overload condition. Thus, soft requirements allow us to choose the preferred one from several candidate controllers. ∎

This paper introduces a tool DCSynth which allows synthesis of controllers from regular properties (QDDC formulas). The specification in DCSynth is a tuple $(I,O,D^{h},D^{s})$, where $D^{h}$ and $D^{s}$ are QDDC formulas over a set of input and output propositions $(I,O)$. Here, $D^{h}$ and $D^{s}$ are the hard and the soft requirement, respectively111The tool supports more general lexicographically ordered list of soft requirements. However, we omit the general case for brevity. We use the term supervisor for a non-blocking Mealy machine which may non-deterministically produce one or more outputs for each input. A supervisor may be refined to a sub-supervisor by resolving (pruning) the non-determinstic choice of outputs (the sub-supervisor may use additional memory for making the choice.) We define a determinism ordering on supervisors in the paper. A controller is a deterministic supervisor. Ramadge and Wonham [25, 26] investigated the synthesis of the maximally permissive supervisor for a regular specification. The maximally permissive supervisor is a unique supervisor, which encompasses all the behaviors invariantly satisfying the specified regular property (See Definition 6). The well known safety synthesis algorithm applied to the DFA for $D^{h}$ gives us the maximally permissive supervisor $MPS(D^{h})$ [10]. If no such supervisor exists, the specification is reported as unrealizable.

Any controller obtained by arbitrarily resolving the nondeterministic choices for outputs in $MPS(D^{h})$ is correct-by-construction. This results in several controllers with distinct behaviours (as shown by previous example). Thus, only correct-by-construction synthesis is not sufficient [3]. Some form of guidance must be provided to the synthesis method to choose among the possible controllers. We use the soft requirements to provide such guidance. Our synthesis method tries to choose a controller, which satisfies the soft requirements ($D^{s}$) “as much as possible”. Soft requirement can also specify the desirable requirements, which cannot be met invariantly. For example, in a Mine-pump controller, as soft requirement “keep the pump off unless mandated by the hard requirement” specifies an energy efficient controller. Specification of scheduling, performance and quality constraints are often such desirable properties. Moreover, a specification may consist of a conjunction of conflicting requirements. In this case, all the requirements cannot be invariantly met simultaneously. User may resolve the conflict(s) by making some of these requirements as soft. Therefore, soft requirements give us a capability to synthesize meaningful and practical controllers.

In DCSynth, we formalize the notion of a controller meeting the soft requirement $D^{s}$ “as much as possible”, by synthesizing a sub-supervisor of $MPS(D^{h})$ (guaranteeing invariance of $D^{h}$), which maximizes the expected value of count of $D^{s}$ in next $H$ moves when averaged over all the inputs. The classical value iteration algorithm due to Bellman [2] allows us to compute this $H$-optimal sub-supervisor. This can be further refined to a controller as desired. Thus, our synthesis method gives a controller which, (a) invariantly satisfies $D^{h}$ and (b) it is $H$-optimal for $D^{s}$ amongst all controllers meeting condition (a).

The above synthesis method is implemented in tool DCSynth. An efficient representation of DFA using BDDs, originally introduced by the tool MONA [15], is used for representing both automata and supervisors. We adapt the safety synthesis algorithm and the value iteration algorithm so that they work symbolically over this MONA DFA representation.

We illustrate our specification method and synthesis tool with the help of two case studies222DCSynth can be downloaded at [31] along with the specification files for experiments.. We define metrics to compare the controllers for their guaranteed and expected behaviour. The tool DCSynth facilitates measurement of both these metrics. The main contributions of this paper are as follows:

• •

We develop a technique for the synthesis of controllers from QDDC requirements. This extends the past work on model checking interval temporal logic QDDC [21, 20, 7, 29, 17] with synthesis abilities.

• •

We propose a method for guided synthesis of controllers based on soft requirements which are met in a $H$-optimal fashion. Conceptually, this enhances the Ramadge-Wonham framework for optimal controller synthesis.

• •

We present a tool DCSynth for guided synthesis, which

• –

represents and manipulates automata/supervisors using BDD-based semi-symbolic DFA. It uses eager minimization for efficient synthesis, and

• –

provides facility to compare both the guaranteed and expected case behaviours of the candidate controllers.

• •

We analyse the impact of soft requirements on the quality of the synthesized controllers experimentally using case studies.

The rest of the paper is arranged as follows. Section 2 describes the syntax and semantics of QDDC. Important definitions are presented in Section 3. Syntax of DCSynth specification and the controller synthesis method are presented in Section 4. Section 5 discusses case studies and experimental results. The paper is concluded with a discussion and related work in Sections 6 and 7.

2 Quantified Discrete Duration Calculus (QDDC) Logic

Let $PV$ be a finite non-empty set of propositional variables. Let $\sigma$ a non-empty finite word over the alphabet $2^{PV}$. It has the form $\sigma=P_{0}\cdots P_{n}$ where $P_{i}\subseteq PV$ for each $i\in\{0,\ldots,n\}$. Let $len(\sigma)=n+1$, $dom(\sigma)=\{0,\ldots,n\}$, $\sigma[i,j]=P_{i}\cdots P_{j}$ and $\sigma[i]=P_{i}$.

The syntax of a propositional formula over variables $PV$ is given by:

[TABLE]

with $\&\&,||,!$ denoting conjunction, dis-junction and negation, respectively. Operators such as $\Rightarrow$ and $\Leftrightarrow$ are defined as usual. Let $\Omega(PV)$ be the set of all propositional formulas over variables $PV$. Let $i\in dom(\sigma)$. Then the satisfaction of propositional formula $\varphi$ at point $i$, denoted $\sigma,i\models\varphi$ is defined as usual and omitted here for brevity.

The syntax of a QDDC formula over variables $PV$ is given by:

[TABLE]

where $\varphi\in\Omega(PV)$, $p\in PV$, $c~{}\in\mathbb{N}$ and $\bowtie\in\{<,\leq,=,\geq,>\}$.

An interval over a word $\sigma$ is of the form $[b,e]$ where $b,e\in dom(\sigma)$ and $b\leq e$. Let $Intv(\sigma)$ be the set of all intervals over $\sigma$. Let $\sigma$ be a word over $2^{PV}$ and let $[b,e]\in Intv(\sigma)$ be an interval. Then the satisfaction relation of a QDDC formula $D$ over $\Sigma$ and interval $[b,e]$ written as $\sigma,[b,e]\models D$, is defined inductively as follows:

[TABLE]

with Boolean combinations $!D$, $D_{1}~{}||~{}D_{2}$ and $D_{1}~{}\&\&~{}D_{2}$ defined in the expected way. We call word $\sigma^{\prime}$ a $p$-variant, $p\in PV$, of a word $\sigma$ if $\forall i\in dom(\sigma),\forall q\neq p:q\in\sigma^{\prime}[i]\Leftrightarrow q\in\sigma[i]$. Then $\sigma,[b,e]\models ex~{}p.~{}D\Leftrightarrow\sigma^{\prime},[b,e]\models D$ for some $p$-variant $\sigma^{\prime}$ of $\sigma$ and $(all~{}p.~{}D)\Leftrightarrow(!ex~{}p.~{}!D)$.

Entities $slen$ , $scount$ and $sdur$ are called terms. The term $slen$ gives the length of the interval in which it is measured, $scount\ \varphi$ where $\varphi\in\Omega(PV)$, counts the number of positions including the last point in the interval under consideration where $\varphi$ holds, and $sdur\ \varphi$ gives the number of positions excluding the last point in the interval where $\varphi$ holds. Formally, for $\varphi\in\Omega(PV)$ we have $slen(\sigma,[b,e])=e-b$, scount(\sigma,\varphi,[b,e])=\sum_{i=b}^{i=e}\left\{\begin{array}[]{ll}1,&\mbox{if }\sigma,i\models\varphi,\\ 0,&\mbox{otherwise.}\end{array}\right\} and sdur(\sigma,\varphi,[b,e])=\sum_{i=b}^{i=e-1}\left\{\begin{array}[]{ll}1,&\mbox{if }\sigma,i\models\varphi,\\ 0,&\mbox{otherwise.}\end{array}\right\}

We also define the following derived constructs: $pt=\langle true\rangle$, $ext=!pt$, $\mathbf{\langle\rangle D}=true\verb|^|D\verb|^|true$, $[]D=(!\langle\rangle!D)$ and $\mathbf{pref(D)}=!((!D)\verb|^|true)$. Thus, $\sigma,[b,e]\models[]D$ iff $\sigma,[b^{\prime},e^{\prime}]\models D$ for all sub-intervals $b\leq b^{\prime}\leq e^{\prime}\leq e$ and $\sigma,[b,e]\models\mathit{pref}(D)$ iff $\sigma,[b,e^{\prime}]\models D$ for all prefix intervals $b\leq e^{\prime}\leq e$.

Definition 1 (Language of a formula)

Let $\sigma,i\models D$ iff $\sigma,[0,i]\models D$, and $\sigma\models D$ iff $\sigma,len(\sigma)-1\models D$. We define $L(D)=\{\sigma\mid\sigma\models D\}$, the set of behaviours accepted by $D$. Formula $D$ is called valid, denoted $\models_{dc}D$, iff $L(D)=(2^{PV})^{+}$. ∎

Thus, a formula $D$ holds at a point $i$ in a behaviour provided the past of the point $i$ satisfies $D$.

Theorem 2.1

[21]** For every formula $D$ over variables $PV$ we can construct a Deterministic Finite Automaton (DFA) $\mathcal{A}(D)$ over alphabet $2^{PV}$ such that $L(\mathcal{A}(D))=L(D)$. We call $\mathcal{A}(D)$ a formula automaton for $D$ or the monitor automaton for $D$. ∎

A tool DCVALID implements this formula automaton construction in an efficient manner by internally using the tool MONA [15]. It gives minimal, deterministic automaton (DFA) for the formula $D$.

We omit the details here. The reader may refer to several papers on QDDC for detailed description and examples of QDDC specifications as well as its model checking tool DCVALID [21, 19, 20, 7, 29].

3 Supervisor and Controller

In this section we present QDDC formulas and automata where variables $PV=I\cup O$ are partitioned into disjoint sets of input variables $I$ and output variables $O$. It is known that supervisors and controllers can be expressed as Mealy machines with special properties. Here we show how Mealy machines can be represented as special form of Deterministic finite automata (DFA). This representation allows us to use the MONA DFA library [15] to compute supervisors and controllers efficiently using our tool DCSynth.

Definition 2 (Output-nondeterministic Mealy Machine)

A total and Deterministic Finite Automaton (DFA) over input-output alphabet $\Sigma=2^{I}\times 2^{O}$ is a tuple $A=(Q,\Sigma,s,\delta,F)$ having conventional meaning, where $\delta:Q\times 2^{I}\times 2^{O}\rightarrow Q$. An output-nondeterministic Mealy machine is a DFA with a unique reject (or non-final) state $r$ which is a sink state i.e., $F=Q-\{r\}$ and $\delta(r,i,o)=r$ for all $i\in 2^{I}$, $o\in 2^{O}$. ∎

The intuition behind this definition is that the transitions from $q\in F$ to $r$ are forbidden (and kept only for making the DFA total). The language of any such Mealy machine is prefix-closed. Recall that for a Mealy machine, $F=Q-\{r\}$. A Mealy machine is deterministic if $\forall s\in F$, $\forall i\in 2^{I}$, $\exists$ at most one $o\in 2^{O}$ such that $\delta(s,i,o)\not=r$.

Definition 3 (Non-blocking Mealy Machine)

An output-nondeterministic Mealy machine is called non-blocking if $\forall s\in F$, $\forall i\in 2^{I}$ $\exists o\in 2^{O}$ such that $\delta(s,i,o)\in F$. It follows that for all input sequences a non-blocking Mealy machine can produce one or more output sequence without ever getting into the reject state. ∎

For a Mealy machine $M$ over variables $(I,O)$, its language $L(M)\subseteq(2^{I}\times 2^{O})^{*}$. A word $\sigma\in L(M)$ can also be represented as pair $(ii,oo)\in((2^{I})^{*},(2^{O})^{*})$ such that $\sigma[k]=ii[k]\cup oo[k],\forall k\in dom(\sigma)$. Here $\sigma,ii,oo$ must have the same length. Note that in the rest of this paper, we do not distinguish between $\sigma$ and $(ii,oo)$. Also, for any input sequence $ii\in(2^{I})^{*}$, we define $M[ii]=\{oo~{}\mid~{}(ii,oo)\in L(M)\}$.

Definition 4 (Controllers and Supervisors)

An output-nondeterministic Mealy machine which is non-blocking is called a supervisor. An deterministic supervisor is called a controller. ∎

The non-deterministic choice of outputs in a supervisor denotes unresolved decision. The determinism ordering defined below allows supervisors to be refined into controllers.

Definition 5 (Determinism Order and Sub-supervisor)

Given two supervisors $S_{1}$ and $S_{2}$, we say $S_{1}\leq_{det}S_{2}$ ($S_{2}$ is more deterministic than $S_{1}$), iff $L(S_{2})\subseteq L(S_{1})$. We call $S_{2}$ to be a sub-supervisor of $S_{1}$. ∎

Note that being supervisors, they are both non-blocking and hence $\emptyset\subset S_{2}[ii]\subseteq S_{1}[ii]$ for any $ii\in(2^{I})^{*}$. The supervisor $S_{2}$ may make use of additional memory for resolving and pruning the non-determinism in $S_{1}$.

For technical convenience, we define a notion of indicator variable for a QDDC formula (regular property). The idea behind this is that the indicator variable $w$ witnesses the truth of a formula $D$ at any point in execution. Thus,

[TABLE]

Here, $\mathbf{EP(w)}=(true\verb#^#\langle w\rangle)$, i.e. $EP(w)$ holds at a point $i$, if variable $w$ is true at that point $i$. Hence, $w$ will be $true$ exactly on those points where $D$ is $true$. The formula automaton $\mathcal{A}(Ind(D,w))$ gives us a controller with input-output alphabet $(I\cup O,w)$ such that it outputs $w=1$ on a transition iff the past satisfies $D$. Since our formula automata are minimal DFA, $\mathcal{A}(Ind(D,w))$ characterizes the least memory needed to track the truth of formula $D$.

4 DCSynth Specification and Controller Synthesis

This section defines the DCSynth specification and presents the algorithm used in our tool DCSynth for soft requirement guided controller synthesis from a DCSynth specification. The process of synthesizing a controller as discussed in Section 4.4 uses three main algorithms given in Sections 4.1-4.3.

4.1 Invariance Properties and Maximally Permissive Supervisor

A QDDC formula $D$ specifies a regular property which may hold intermittently during a behaviour (see Definition 1). An important class of properties, denoted by $\mbox{\bf inv\/}~{}D$, states that $D$ must hold invariantly during the system behaviour.

Definition 6

Let ${\mathbf{S}}~{}\mathbf{realizes}\mathbf{~{}\mbox{\bf inv\/}~{}D}$ denote that a supervisor $S$ realizes invariance of QDDC formula $D$ over variables $(I,O)$. Define ${\mathbf{S}}~{}\mathbf{realizes}\mathbf{~{}\mbox{\bf inv\/}~{}D}$ provided $L(S)\subseteq L(D)$. Recall that, by the definition of supervisors, $S$ must be non-blocking. A supervisor $S$ for a formula $D$ is called maximally permissive $\mathit{iff}$ $S\leq_{det}S^{\prime}$ holds for any supervisor $S^{\prime}$ such that $S^{\prime}~{}\mbox{{realizes}}~{}\mbox{\bf inv\/}~{}D$. This $S$ (when it exists) is unique upto language equivalence of automata, and the minimum state maximally permissive supervisor is denoted as $\textbf{MPS}(D)$. ∎

Now, we discuss how $MPS(D)$ for a given QDDC formula $D$ is computed.

Language equivalent DFA $\mathcal{A}(D)=\langle S,2^{I\cup O},\delta,F\rangle$ is constructed for formula $D$ (Theorem 2.1). The standard safety synthesis algorithm [12] over $\mathcal{A}(D)$ gives us the desired $MPS(D)$ as outlined in the following steps. 2. 2.

We first compute the largest set of winning states $G\subseteq F$ with the following property: $s\in G$ iff $\forall i\exists o:\delta(s,(i,o))\in G$. Let $Cpre(\mathcal{A}(D),X)=\{s~{}\mid~{}\forall i\exists o:\delta(s,(i,o))\in X\}$. Then we iteratively compute $G$ as follows:

     G=F;

     do

         G1=G;

         G=Cpre($\mathcal{A}(D)$,G1);

     while (G != G1); 3. 3.

If initial state $s\notin G$, then the specification is unrealizable. Otherwise, $MPS(D)$ is obtained by declaring $G$ as the set of final states and retaining all the transitions in $\mathcal{A}(D)$ between states in $G$ and redirecting the remaining transitions of $\mathcal{A}(D)$ to a unique reject state $r$ which is made a sink state.

Proposition 1

For a given QDDC formula $D$ the above algorithm computes the maximally permissive supervisor $MPS(D)$. ∎

The proposition follows straightforwardly by combining Theorem 2.1 with the correctness of standard safety synthesis algorithm [12]. We omit a detailed proof.

4.2 Maximally Permissive $H$-Optimal Supervisor (MPHOS)

Given a supervisor $S$ and a desired QDDC formula $D$ which should hold “as much as possible” (both are over input-output variables $(I,O)$), we give a method for constructing an “optimal” sub-supervisor of $S$, which maximizes the expected value of count of $D$ holding in next H moves when averaged over all the inputs.

First consider $\mathcal{A}^{Arena}=S\times\mathcal{A}(Ind(D,w))$ which is a supervisor over input-output variables $(I,O\cup\{w\})$. It augments $S$ by producing an additional output $w$ which witnesses the truth of $D$. It has the property: $L(\mathcal{A}^{Arena})\downarrow(I\cup O)=L(S)$. Also for $\sigma\in L(\mathcal{A}^{Arena})$ and $i\in dom(\sigma)$ we have $w\in\sigma[i]$ iff $\sigma[0:i]\models D$. Thus, every transition of $\mathcal{A}^{Arena}$ is labelled with $w$ iff $D$ holds on taking the transition. Let the weight of transitions labelled with $w$ be 1 and 0 otherwise. Thus, for $o\in 2^{(O\cup\{w\})}$ let $wt(o)=1$ if $w\in o$ and [math] otherwise. Technically, this makes $\mathcal{A}^{Arena}$ a weighted automaton.

In the supervisor $\mathcal{A}^{Arena}=(Q,\Sigma,s,\delta,Q-\{r\})$, where $r$ is the unique reject state, we define for $(q\in Q)\not=r$ and $i\in 2^{I}$, set $LegalOutputs(q,i)=\{o~{}\mid~{}\delta(q,i)\not=r\}$. We also define a deterministic selection rule as function $f$ s.t.  $f(q,i)\in LegalOutputs(q,i)$ and a non-deterministic selection rule $F$ as function $F$ s.t.$F(q,i)\in\{O\subseteq LegalOutputs(q,i)~{}\mid~{}O\neq\emptyset\}$. Let $H$ be a natural number. Then $H$-horizon policy $\pi$ is a sequence $F_{1},F_{2},\ldots,F_{H}$ of non-deterministic selection rules. A deterministic policy will use only deterministic selection rules. A policy is stationary (memory-less) if each $F_{i}$ is the same independently of $i$.

Given a state $s$, a policy $\pi$ and an input sequence $ii\in(2^{I})^{H}$ (of length $H$), we define $L(\mathcal{A}^{Arena},ii,s)$ as all runs of $\mathcal{A}^{Arena}$ over the input $ii$ starting from state $s$ and $L^{\pi}(\mathcal{A}^{Arena},ii,s)$ as all runs over input $ii$ starting from $s$ and following the selection rule $F_{i}$ at step $i$. Each run has the form $(ii,oo)$. Let $Value(ii,oo)=\Sigma_{1\leq i\leq\#ii}~{}~{}wt(oo[i]))$. Thus, $Value(ii,oo)$ gives the count of $D$ holding during behaviour fragment $(ii,oo)$. Then, we define $VMIN^{\pi}(s,ii)=min\{Value(ii,oo)~{}\mid~{}(ii,oo)\in L^{\pi}(\mathcal{A}^{Arena},ii,s)\}$, which gives the minimum possible count of $D$ among all the runs of $S$ under policy $\pi$ on input $ii$, starting with state $s$. We also define, $VMAX(s,ii)=max\{Value(ii,oo)~{}\mid~{}(ii,oo)\in L(\mathcal{A}^{Arena},ii,s)\}$, which gives the maximum achievable count. Note that $VMAX$ is independent of any policy.

Given a horizon value (natural number) $H$, $\mathcal{A}^{Arena}$ and a non-deterministic $H$-horizon policy $\pi$, we define utility values $ValAvgMin^{\pi}(s)$ and $ValAvgMax(s)$ for each state $s$ of $\mathcal{A}^{Arena}$ as follows.

[TABLE]

Thus, intuitively, $ValAvgMax(s)$ gives the maximal achievable count of $D$ from state $s$, when averaged over all inputs of length $H$. Similarly, $ValAvgMin^{\pi}(s)$ gives the minimal such count for $D$ under policy $\pi$, when averaged over all inputs of length $H$. Our aim is to construct a horizon-$H$ policy $\pi^{*}=argmax_{\pi}~{}~{}ValAvgMin^{\pi}(s)$. This will turn out to be a stationary policy given by a selection rule $F^{*}$. This rule can be implemented as a supervisor denoted by $MPHOS(\mathcal{A}^{Arena},H)$. We now give its construction.

The well known value iteration algorithm allows us to efficiently compute $ValAvgMax(s)$ as recursive function $Val(s,H)$ below.

[TABLE]

We omit the straightforward proof that $Val(s,H)=ValAvgMax(s)$ (see [24]).

Having computed this, the optimal selection rule $F^{*}$ giving stationary policy $\pi^{*}$ is given as follows: For each state $s\in\mathcal{A}^{Arena}$ and each input $i\in 2^{I}$,

[TABLE]

Note that $F^{*}(s,i)$ is non-deterministic as more than one output $o$ may satisfy the $argmax$ condition. The following well-known lemma states that stationary policy $\pi^{*}$ using the selection rule $F^{*}$ is $H$-optimal.

Lemma 1

For all states $s$ of $\mathcal{A}^{Arena}$, $ValAvgMin^{\pi^{*}}(s)=ValAvgMax(s)$ always holds. Therefore, for all states $s$ of $\mathcal{A}^{Arena}$ and for any $H$-horizon policy $\pi$, $ValAvgMin^{\pi}_{H}(s)\leq ValAvgMin^{\pi^{*}}(s)$ also holds. ∎

We omit the proof of these well known properties from optimal control of Markov Decision Processes (see [24]).

Supervisor $\mathcal{A}^{Arena}$ is pruned to retain only the transitions with the outputs in set $F^{*}(s,i)$ (as these are all equally optimal). This gives us Maximally permissive $H$-Optimal sub-supervisor of $\mathcal{A}^{Arena}$ w.r.t. $D$. This supervisor is denoted by $MPHOS(\mathcal{A}^{Arena},H)$ or equivalently $MPHOS(S,D,H)$. The following proposition follows immediately from the construction of $MPHOS(S,D,H)$ and Lemma 1.

Proposition 2

$S\leq_{det}MPHOS(S,D,H)$, for all $H$. 2. 2.

$MPHOS(S,D,H)$* is maximally permissive $H$-optimal sub-supervisor of $S$.* 3. 3.

If $MPHOS(S,D,H)\leq_{det}S^{\prime}$ then $S^{\prime}$ is $H$-Optimal. ∎

4.3 From Supervisor to Controller

A controller $Cnt$ can be obtained from a supervisor $S$ by resolving output non-determinism in $S$. We give a rather straightforward mechanism for this. We allow the user to specify an ordering $Ord$ on the set of output variables $2^{O}$. A given supervisor $S$ is determinized by retaining only the highest ordered output among those permitted by $S$. This is denoted $Det_{Ord}(S)$. The output ordering is specified by giving a lexicographically ordered list of output variable literals. This facility is used to determinize $MPHOS$ and $MPS$ supervisors as required.

Example 2

For a supervisor $S$ over variables $(I,\{o_{1},o_{2}\})$, an example output order can be given as lexicographically ordered list ($o_{1}>~{}!o_{2}$). Then, for any transition the determinization step will try to select the highest ordered output (which is allowed by $S$) from the list {($o_{1}=true,o_{2}=false$), ($o_{1}=true,o_{2}=true$), ($o_{1}=false,o_{2}=false$), ($o_{1}=false,o_{2}=true$)}. ∎

4.4 DCSynth Specification and Controller Synthesis

A DCSynth specification is a tuple $(I,O,D^{h},D^{s})$, where $I$ and $O$ are the set of input and output variables, respectively. Formula $D^{h}$ called the hard requirement and formula $D^{s}$ called the soft requirement are QDDC formulas over the set of propositions $PV=I\cup O$. Let $H$ be a natural number called Horizon. The objective in DCSynth is to synthesize a deterministic controller which (a) invariantly satisfies the hard requirement $D^{h}$, and (b) it is $H$ Optimal w.r.t. $D^{s}$ amongst all the controllers satisfying (a).

Given a specification $(I,O,D^{h},D^{s})$, a horizon value $H$ (a natural number) and a total ordering $Ord$ on the set of outputs $2^{O}$, the controller synthesis in DCSynth can be given as Algorithm 1.

Algorithm 1

**ControllerSynthesis

Input: $S=(I,O,D^{h},D^{s})$. Horizon $H$, Output ordering $Ord$

Output: Controller Cnt for S.

1. $\mathcal{A}^{mps}$ = $MPS(D^{h})$

2. $\mathcal{A}^{mphos}$ = $MPHOS(\mathcal{A}^{mps},D^{s},H)$

3. $Cnt$ = $Det_{ord}(\mathcal{A}^{mphos})$.

4. Encode the automaton $Cnt$ in an implementation language.**

Step 1 uses the MPS construction given in Section 4.1. Step 2 uses the MPHOS construction given in Section 4.2 whereas Step 3 uses the determinization method of Section 4.3.

Proposition 3

The controller $Cnt$ output by Algorithm 1 invariantly satisfies $D^{h}$, and it intermittently, but $H$-optimally, satisfies $D^{s}$.

Proof

By Proposition 1, $\mathcal{A}^{mps}$ realizes $\mbox{\bf inv\/}~{}D^{h}$. Then, by Proposition 2, $\mathcal{A}^{mphos}$ and $Cnt$ are sub-supervisors of $\mathcal{A}^{mps}$ and hence they also realize $\mbox{\bf inv\/}~{}D^{h}$. Moreover, by Lemma 1, we get that $\mathcal{A}^{mphos}$ is $H$-optimal w.r.t. $D^{s}$. Hence, by Proposition 2, we get that $Cnt$ which is a sub-supervisor of $\mathcal{A}^{mphos}$ is also $H$-Optimal with respect to $D^{s}$. ∎

At all stages of above synthesis, the automata/supervisors $\mathcal{A}(D^{h})$, $\mathcal{A}(D^{s})$, $A^{mps}$ and $A^{mphos}$ and $Cnt$ are all represented as semi-symbolic automata (SSDFA) using the MONA [15] DFA data structure. In this representation, the transition function is represented as a multi-terminal BDD. MONA DFA library provides a rich set of automata operations including product, projection, determinization and minimization over the SSDFA. The algorithms discussed in Sections 4.1, 4.2 and 4.3 are implemented over SSDFA. Moreover, these algorithms are adapted to work without actually expanding the specification automata into game graph. At each stage of computation, the automata and supervisors are aggressively minimized, which leads to significant improvement in the scalability and computation time of the tool. Appendix 0.D gives the details of SSDFA data structure and its use in symbolic computation of supervisors in efficient manner.

5 Case Studies and Experiments

For a DCSynth specification, $D^{h}$ and $D^{s}$ can be any QDDC formulas. While invariance of $D^{h}$ is guaranteed by the synthesis algorithm, the quality of the controller is controlled by optimizing the outputs for which the soft requirement $D^{s}$ holds. For example, $D^{s}$ may specify outputs which save energy, giving an energy efficient controller. The soft requirement can also be used to improve the robustness [3] of the controller (see [30]). Below, we consider specifications structured as assumptions and commitments, and their optimized robustness using our soft requirement guided synthesis.

5.1 Types of Controller Specification

For many examples, the controller specification can be given as a pair $(A,C)$ of QDDC formulas over input-output variables $(I,O)$. Here, commitment $C$ is a formula specifying the desired behaviour which must ideally hold invariantly. But this may be unrealizable, and a suitable assumption $A$ on the behaviour of environment may have to be made for $C$ to hold. In case the assumption $A$ does not hold, it is still desirable that controller satisfies $C$, intermittently but “as much as possible”. Given this assumption-commitment pair $(A,C)$, we specify four types of derived controller specifications $(I,O,D^{h},D^{s})$ as follows.

[TABLE]

Type0 controller gives the best guarantee but it may be unrealizable. Type1 controller provides a firm but conditional guarantee. Type2 controller tries to achieve $C$ in $H$-optimal fashion irrespective of any assumption and Type3 Controller provides firm conditional guarantee and it also tries to satisfy $C$ in $H$-optimal fashion even when the assumption does not hold.

5.2 Performance Metrics: Measuring quality of controllers

For the same assumption commitment pair $(A,C)$, we can synthesize diverse controllers using different specification types, horizon values and output orderings. In order to compare the performance of these different controllers, we define two metrics – i) Expected Case Performance measure to compare average case behaviour, and ii) Must Dominance to compare the guaranteed behaviour.

i) Expected Case Performance:

Given a controller $Cnt$ over input-output alphabet $(I,O)$ and a QDDC formula (regular property) $C$ over variables $I\cup O$, we can construct a Discrete Time Markov Chain (DTMC), denoted $M_{unif}(Cnt,C)$, whose analysis allows us to measure the probability of $C$ holding in long runs (steady state) of $Cnt$ under random independent and identically distributed(iid) inputs. This value is designated as $\mathbb{E}_{unif}(Cnt,C)$. The construction of the desired DTMC is as follows. The product $Cnt\times\mathcal{A}(C)$ gives a finite state automaton with the same behaviours as $Cnt$. Moreover, it is in accepting state exactly when $C$ holds for the past behaviour. (Here $\mathcal{A}(C)$ works as a total deterministic monitor automaton for $C$ without restricting $Cnt$). By assigning uniform discrete probabilities to all the inputs from any state, we obtain the DTMC $M_{unif}(Cnt,C)$ along with a designated set of accepting states, such that the DTMC is in accepting state precisely when $C$ holds. Standard techniques from Markov chain analysis allow us to compute the probability (Expected value) of being in the set of accepting states on long runs (steady state) of the DTMC. This gives us the desired value $\mathbb{E}_{unif}(Cnt,C)$. A leading probabilistic model checking tool MRMC implements this computation [14]. In DCSynth, we provide a facility to compute $M_{unif}(Cnt,C)$ in a format accepted by the tool MRMC. Hence, using DCSynth and MRMC, we are able to compute $\mathbb{E}_{unif}(Cnt,C)$.

ii) Guaranteed Performance as Must-Dominance:

Consider two supervisors $S_{1}$, $S_{2}$ and a regular property $C$. Define that $S_{i}$ guarantees $C$ for an input sequence $ii$, provided for every output sequence $oo\in S_{i}[ii]$ produced by $S_{i}$ on $ii$ we have that $(ii,oo)$ satisfies $C$. We say that $S_{2}$ must dominance $S_{1}$ with respect to the property $C$ provided for every input sequence $ii$, if $S_{1}$ guarantees $C$ then $S_{2}$ also guarantees $C$. Thus, $S_{2}$ provides a superior must guarantee of $C$ than $S_{1}$.

Definition 7 (Must Dominance)

Given two supervisors $S_{1},S_{2}$ and a property (formula) $C$ over input-output alphabet $(I,O)$, the must dominance of $S_{2}$ over $S_{1}$ is defined as $S_{1}\leq_{dom}^{C}S_{2}\quad\mbox{iff}\quad$ $MustInp(S_{1},C)~{}\subseteq~{}MustInp(S_{2},C)$, where $MustInp(S_{i},C)=\{ii\in(2^{I})^{+}\mid\forall oo\in(2^{O})^{+}.((ii,oo)\in L(S_{i})\Rightarrow(ii,oo)\models C\}$. ∎

We establish must dominance relations among MPHOS supervisors of various types of specifications discussed in Section 5.1.

Lemma 2

For any QDDC formulas $A$ and $C$, and any horizon $H$, the following must dominance relations will hold (for any given $H$)

$MPHOS_{1}(A,C))$* $\leq_{dom}^{C}MPHOS_{3}(A,C))\leq_{dom}^{C}MPHOS_{0}(A,C))$* 2. 2.

$MPHOS_{2}(A,C))\leq_{dom}^{C}MPHOS_{0}(A,C))$*

---

where, $MPHOS_{i}(A,C)$ denote the maximally permissive $H$-optimal supervisor $\mathcal{A}^{MPHOS}$ of Algorithm 1 for the specification $Type_{i}(A,C)$.

Proof

By definition, $MPHOS_{0}(A,C)$ invariantly satisfies $C$ for all input sequences. Hence, $MustInp(MPHOS_{0}(A,C),C)=(2^{I})^{*}$, which immediately gives us that $S\leq_{dom}^{C}MPHOS_{0}(A,C))$ for any supervisor $S$.

Now we prove the remaining relation $MPHOS_{1}(A,C))$ $\leq_{dom}^{C}MPHOS_{3}(A,C))$. Let $S=MPS(A\Rightarrow C)$. Then, $MPHOS_{1}(A,C))=MPHOS(S,true,H)=S$. The second equality holds as soft requirement $true$ does not cause any pruning of outputs in $H$-optimal computation. By definition $MPHOS_{3}(A,C)=MPHOS(S,C,H)$. By Proposition 2, $S\leq_{det}MPHOS(S,C,H)$ which gives us the required result. ∎

Note that in general, $MPHOS_{2}(A,C)$ is theoretically incomparable with $MPHOS_{1}(A,C)$ and $MPHOS_{3}(A,C)$, as $MPHOS_{2}(A,C)$ is a supervisor that does not have to meet any hard requirement, but it optimally meets the soft requirements irrespective of the assumption. However, for specific $(A,C)$ instances, some additional must-dominance relations may hold between $MPHOS_{2}(A,C)$ and the other supervisors.

5.3 Case Studies: Mine-pump and Arbiter Specifications

We have carried out experiments with i) the Mine-pump specification presented in this section, and ii) an Arbiter specification given in Appendix 0.A.1.

Mine-pump: The Mine-pump controller (see [21]) has two input sensors: high water level sensor $\mathit{HH2O}$ and methane leakage sensor $\mathit{HCH4}$; and one output, $\mathit{PUMPON}$ to keep the pump on. The objective of the controller is to safely operate the pump in such a way that the water level never remains high continuously for more that $w$ cycles. Thus, Mine-pump controller specification has input and output variables $(\{HH2O,HCH4\},\{PUMPON\})$.

We have following assumptions on the mine and the pump. Their conjunction is denote $MineAssume(\epsilon,\zeta,\kappa)$ with integer parameters $\epsilon,\zeta,\kappa$. Being of the form $[]D$ each formula states that the property $D$ (described in text) holds for all observation intervals in past.

Pump capacity: $([]!(slen=\epsilon~{}\&\&~{}([[PUMPON~{}\&\&~{}HH2O]]$^$\langle HH2O\rangle)))$. If the pump is continuously on for $\mathit{\epsilon}$ cycles with water level also continuously high, then water level will not be high at the $\mathit{\epsilon+1}$ cycle.

• -

Methane release: $[](([HCH4]$^$[!HCH4]$^$\langle HCH4\rangle)\Rightarrow(slen>\zeta))$ and $[]([[HCH4]]\Rightarrow slen<\kappa)$. The minimum separation between the two leaks of methane is $\mathit{\zeta}$ cycles and the methane leak cannot persist for more than $\mathit{\kappa}$ cycles.

The commitments are as follows. The conjunction of commitments is denoted by $MineCommit(w)$ and they hold intermittently in absence of assumption.

Safety conditions: $true$^$\langle((HCH4~{}||~{}!HH2O)\Rightarrow~{}!PUMPON))\rangle$ states that if there is a methane leak or absence of high water in current cycle, then pump should be off in the current cycle. Formula $!(true$^$([[HH2O]]~{}\&\&~{}slen=w))$ states that the water level does not remain continuously high in last $w+1$ cycles.

The Mine-Pump specification denoted by $MinePump(w,\epsilon,\zeta,\kappa)$ is given by the assumption-commitment pair $(MineAssume(\epsilon,\zeta,\kappa),MineCommit(w))$. The four types of DCSynth specifications of Section 5.1 can be derived from this. Figure 3 in Appendix 0.B gives the textual source of $Type3(MinePump(8,2,6,2))$ specification used by the DCSynth tool.

Arbiter: Due to space limitations, the detailed specification of the arbiter, briefly discussed as Example 1 in Section 1, is given in Appendix 0.A.1. The arbiter is denoted as $Arb(n,k,r)$, where $n$ denotes the number of clients, $k$ is the response time (time for which a client should keep the request high continuously to get the guaranteed access) and $r$ is the maximum number of request that can be true simultaneously.

5.4 Experimental Evaluation

Given an assumption-commitment pair $(A,C)$ the four types of DCSynth specifications can be derived as given in Section 5.1. Given any such specification, a horizon value $H$, and an ordering of outputs, a controller can be synthesized using our tool DCSynth as described in Section 4.4.

For the Mine-pump instance $MinePump(8,2,6,2)$, we synthesized controllers for all the four derived specification types with horizon value $H=50$ and output ordering $PUMPON$. These controllers choose to get rid of water aggressively by keeping the pump on whenever possible. Similarly, controllers were also synthesized with the output ordering $!PUMPON$. These controllers save energy by keeping the pump off whenever possible. Note that, in our synthesis method, hard and soft requirements are fulfilled before applying the output orderings.

For the Arbiter instance $Arb(5,3,2)$ also, controllers were synthesized for all the four derived specification types with horizon value $H=50$ and output ordering $ArbDef=(a_{1}>a_{2}>a_{3}>a_{4}>a_{5})$. This ordering tries to give acknowledgment such that client $i$ has priority higher than client $j$ for all $i<j$.

In Table 1 we give the performance of the of tool DCSynth in synthesizing these controllers. The table gives the time taken at each stage of the synthesis algorithm, and the sizes of the computed supervisors/controllers. The experiments were conducted on Linux (Ubuntu 16.04) system with Intel i5 64 bit, 2.5 GHz processor and 4 GB memory.

Experimental Evaluation of Expected Case Performance: The last column of Table 1 gives the expected value of commitment holding in long run for the controllers of various types for both Mine-pump and Arbiter instances. This value is computed as outlined in Section 5.2. The results are quite encouraging.

It can be observed from Table 1 that in both the examples, the controllers for Type1 (i.e., when soft-requirements are not used) specifications have [math] expected value of commitment $C$. This is because of the strong assumptions used in guaranteeing $C$, which themselves have expected value [math]. In such a case, whenever the assumption fails, the synthesis algorithm has no incentive to try to meet $C$.

On the other hand, with soft requirement $C$ in Type2 and Type3 specifications, the $H$-optimal controllers have the expected value of $C$ above $99\%$. This remarkable increase in the expected value of Commitment shows that $H$-optimal synthesis is very effective in figuring out controllers which meet the desirable property $C$ as much as possible, irrespective of the assumption.

Experimental Evaluation of Must-Dominance:

Given supervisors $S_{1},S_{2}$ for an assumption-commitment pair $(A,C)$, since both $S_{1},S_{2}$ are finite state Mealy machines and $C$ is a regular property, an automata theoretic technique can automatically check whether $S_{1}\leq_{dom}^{C}S_{2}$. We omit the details of this technique here, which is presented in Appendix 0.C Proposition 4. This technique is implemented in our tool DCSynth. In case $S_{1}\leq_{dom}^{C}S_{2}$ does not hold, the tool provides a counter example.

For our case studies, we experimentally compare must dominance of supervisors $MPHOS_{i}(A,C)$ as defined in Lemma 2. Recall that $MPHOS_{i}(A,C)$ denotes the maximally permissive $H$-optimal supervisor for the specification $Type_{i}(A,C)$. The results obtained (with $H=50$) are as follows.

Mine-pump instance $Minepump(8,2,6,2)$ denoted by $MP(8,2,6,2)$):

• $MPHOS_{1}(MP(8,2,6,2))~{}<_{dom}^{C}~{}MPHOS_{3}(MP(8,2,6,2))~{}=_{dom}^{C}~{}MPHOS_{2}(MP(8,2,6,2))$

Arbiter instance $Arb(5,3,2)$:

• $MPHOS_{1}(Arb(5,3,2))~{}<_{dom}^{C}~{}MPHOS_{2}(Arb(5,3,2))~{}=_{dom}^{C}~{}MPHOS_{3}(Arb(5,3,2))$

$MPHOS_{3}$ must dominates $MPHOS_{1}$ as expected, as $MPHOS_{3}$ is a sub-supervisor of $MPHOS_{1}$. What is interesting and surprising is that in both the case studies Arbiter and Mine-pump, the $MPHOS_{2}$ and $MPHOS_{3}$ supervisors are found to be syntactically identical. This is not theoretically guaranteed, as $Type2$ and $Type3$ supervisors are must-incomparable in general. Thus, in these examples, the $H$-optimal $MPHOS_{2}$ already provides all the must-guarantees of the hand-crafted $MPHOS_{3}$ hard requirements. The $H$-optimization of $C$ seems to exhibit startling ability to guarantees $C$ without human intervention. It will be our attempt to validate this with more examples in future. So far we have considered commitment as soft requirement. In general, the soft requirement can be used to optimize MPS w.r.t. any regular property of interest, where as the hard requirements gives the necessary must guarantees. Such soft requirements may embody performance and quality goals. Hence, it is advisable to use the combination of hard and soft requirement based on the criticality of each requirement.

6 Discussion along with Related Work

Reactive synthesis from Linear Temporal Logic (LTL) specification is a widely studied area[3] and a considerable number of tools [5, 11] supported by theoretical foundations are available. The leading tools such as Acacia+[5] and BoSy[11] mainly focus on the future fragment of LTL. In contrast, this paper focuses on invariance of complex regular properties, denoted by $\mbox{\bf inv\/}~{}D^{h}$ where $D^{h}$ is a QDDC formula. For such a property, a maximally permissive supervisor ($MPS$) can be synthesized. Formally, logics LTL and QDDC have incomparable expressive power. There is increasing evidence that regular properties form an important class of requirements [9, 18, 19]. The IEEE standard PSL extends LTL with regular properties [1]. Wonham and Ramadge in their seminal work [25, 26] first studied the synthesis of maximally permissive supervisors from regular properties. In their supervisory control theory, $MPS$ can in fact be synthesized for a richer property class $AGEF~{}D^{h}$ [10]. Tool DCSynth can be easily extended to support such properties too. Riedweg et al [28] give some sub-classes of Quantified Mu-Calculus for which $MPS$ can be computed. However, none of these works address soft requirement guided synthesis.

Most of the reactive synthesis tools focus on correct-by-construction synthesis from hard requirements. For example, none of the tools in recent competition on reactive synthesis, SYNTCOMP17 [13], address the issue of guided synthesis which is our main focus. In our approach, we refine the MPS (for hard requirements) to a sub-supervisor optimally satisfying the soft requirements too. Since LTL does not admit MPS, it is unclear how our approach can extend to it.

In quantitative synthesis, a weighted arena is assumed to be available, and algorithms for optimal controller synthesis for diverse objectives such as Mean-payoff [4] or energy [6] have been investigated. In our case, we first synthesize the weighted arena from given hard and soft requirements. Moreover, we use $H$-optimality as the synthesis criterion. This criterion has been widely used in reinforcement learning as well as optimal control of MDPs [24, 2]. In other related work, techniques for optimal controller synthesis are discussed by Ding et al [9], Wongpiromsarn et al [32] and Raman et al [27], where they have explored the use of receding horizon model predictive control along with temporal logic properties.

Since our focus is on the quality of the controllers, we have also defined metrics and measurement techniques for comparing the controllers for their guaranteed (based on must dominance) and expected case performance. For the expected case measurement, we have assumed that inputs are $iid$. However, the method can easily accommodate a finite state Markov model governing the occurrences of inputs.

DCSynth uses an efficient BDD-based symbolic representation, inherited from tool MONA [15] for storing automata, supervisors and controllers. The use of eager minimization (see Appendix 0.D for implementation details) allows us to handle much more complex properties (see Appendix 0.E).

7 Conclusions

We have presented a technique for guided synthesis of controllers from hard and soft requirements specified in logic QDDC. This technique is also implemented in our tool DCSynth. Case studies show that combination of hard and soft requirements provides us with a capability to deal with unrealizable (but desirable), conflicting and default requirements. In context of assumption-commitment based specification, we have shown with case studies that soft requirements improve the expected case performance, where as hard requirements provide certain (but typically conditional) guarantees on the synthesized controller. Hence, the combination of hard and soft requirements as formulated in $Type3$ specifications offers a superior choice of controller specification. This is confirmed by theoetical analysis as well as experimental results.

In the paper, we have also explored the experimental ability to compare the controller performance using expected value and must dominance metrics. This helps us in designing better performing controllers.

Appendix 0.A Other Case Studies

In this section we present 3 more case studies:

$n$-client shared resource arbiter (several different specifications), 2. 2.

alarm annunciation system.

0.A.1 Arbiter

An $n$-client resource (e.g. bus) arbiter is a circuit with $r_{1},\ldots,r_{n}$ as inputs ($r_{i}$ high indicates $i^{th}$ client request access to resource) and $ack_{1},\ldots,ack_{n}$ ($a_{i}$ indicates arbiter has granted the $i^{th}$ client access to the resource) as the corresponding outputs. Arbiter arbitrates among a subset of requests at each cycle by setting one of the acknowledgments ($a_{i}$’s) true. Hard requirements on the arbiter include the following three invariant properties.

[TABLE]

Thus, $Mutex$ gives mutual exclusion of acknowledgments, $NoLoss$ states that if there is at least one request then there must be an acknowledgment and $Nospurious$ states that acknowledgment is only given to a requesting cell.

In the literature various arbitration schemes for the arbiter have been proposed, here we consider the following schemes.

• •

$k$-cycle response time: let $Resp(r,a,k)$ denote that if request has been high for last $k$ cycles there must have been at least one acknowledgment in the last $k$ cycles. Let $ArbResp(n,k)$ state that for each cell $i$ and for all observation intervals the formula $Resp(r_{i},a_{i},k)$ holds.

[TABLE]

Based on $k$-cycle response we can define various arbiter specification with different properties as follows:

• –

Then specification $Arb^{hard}(n,k)$ is the following $k$-cycle response time DCSynth specification.

[TABLE]

• –

The specification $Arb^{hard}$ above, invariantly satisfy $ArbCommit(n,k)$ if $n\leq k$. Tool DCSynth gives us a concrete controller for the instance ($D^{h}=ArbCommit(6,6)$, $D^{s}=true$). It is easy to see that there is no controller which can invariantly satisfy $ArbCommit(n,k)$ if $k<n$. Consider the case when all requests $r_{i}$ are continuously true. Then, it is not possible to give response to every cell in less than $n$ cycles due to mutual exclusion of acknowledgment $a_{i}$.

To handle such desirable but unrealizable requirement we make an assumption. Let the proposition $Atmost(n,i)$ be defined as

$\forall S\subseteq\{1\ldots n\},|S|\leq i.~{}~{}\land_{j\notin S}\neg r_{j}$.

It states that at most $i$ requests are true simultaneously. Then, the arbiter assumption is the formula $ArbAssume(n,i)$ = [[ Atmost(n,i)]], which states that $Atmost(n,i)$ holds invariantly in past.

The synchronous arbiter specification $Arb(n,k,i)$ is the assumption-commitment pair $(ArbAssume(n,i),ArbCommit(n,k))$. The four types of controller specifications can be derived from this pair. Figure 4 in Appendix 0.C gives, in textual syntax of the specification for $Type3(Arb(5,3,2))$, in tool DCSynth. The DCSynth specification for $Type3(Arb(n,k,i))$ is denoted by $Arb^{hardAssume}$ given as follows:

[TABLE]

• –

$k$-cycle response time as soft requirement: we specify the requirement of response in $k$ cycles as a soft requirement 333Note that soft requirement in this example is a lexicographical list of several QDDC formulas. The tool DCSynth implements a MPHOS computation using weighted requirements (See 0.D.2 for details) as below.

[TABLE]

• •

Token ring arbitration: a token is circulated among the masters in a round robin fashion. The token is modeled using the variables $tok_{i}$’s ($1\leq i\leq n$). Exactly one of $tok_{i}$’s will hold at any time and if $tok_{i}$ is true then we mean that $master_{i}$ holds the token. The arbiter asserts acknowledgement $a_{i}$ whenever request $r_{i}$ and $tok_{i}$ are true, i. e. priority is accorded to the request of the master which holds the token.

[TABLE]

Let $ARBTOKEN(n)=ARBINV(n)\land Token(n)$. Then $Arb^{tok}(n)$ is the following DCSynth specification.

[TABLE]

0.A.2 Alarm Annunciation System

The next case study is Alarm Annunciation System(AAS) used in a process control system for annunciation for various alarms in the control room. The Alarm Annunciation involves the standard Automatic Ring-Back Sequence for all the digital inputs meant for alarm annunciation and provide the necessary outputs. The specification of Automatic Ring-Back Sequence is given in Table 2. All digital inputs representing alarm conditions are scanned periodically.

As shown in the Table 2 that Automatic Ring-Back Sequence specification takes the alarm signal as input. The high value of signal represents the alarm state, otherwise the signal is said to be in normal state. Other inputs are Acknowledgment, Reset and Silence inputs, which are controller by the operator. There are three output elements: Lamp, Normal Hooter and Ringback Hooter. There is a Lamp corresponding to each alarm signal, whereas Hooters are common to all alarm signals. Lamp can either be Fast Flashing, Slow Flashing, Steady On or Off states. We have encoded the requirements in DCSynth to synthesize the controller. The Silence input can be used by the operator to switch off Hooters.

0.A.2.1 Result of Synthesis

: As discussed in the previous case study soft requirements helped in specification of requirements concisely. The controller synthesized has 8 states. We could simulate the controller and verified the correctness.

0.A.3 Synthesis of 2 client arbiter

Fig. 1 gives the monitor automaton for 2-client arbiter (See section 0.A.1) for n-cell arbiter specification. Each transition is labeled by 4 bit vector giving values of $r_{1},r_{2},a_{1},a_{2}$.

Fig. 2 gives the MPS automaton for the 2-cell arbiter computed from the safety monitor automaton of Fig. 1. (There is an additional reject state. All missing transitions are directed to it. These are omitted from the diagram for simplicity.) Note that this is a DFA whose transitions are labelled by 4-bit vectors representing alphabet $2^{\{r_{1},r_{2},a_{1},a_{2}\}}$. As defined in Definition 2, the DFA also denotes an output-nondeterministic Mealy machine with input variables $(r_{1},r_{2})$ and output variables $(a_{1},a_{2})$. The automaton is nondeterministic in output as from state $1$, on input $(1,1)$ it can move to state $2$ with output $(1,0)$, or to state $3$ with output $(0,1)$. The reader can verify that the automaton is non-blocking and hence a controller.

In 2-cell arbiter example, with soft requirements $\langle ack1,ack2\rangle$ which give $ack1$ priority over $ack2$, we obtain the MPHOS controller automaton of Fig. 2(b) from the MPS of Fig. 2(a). Note that we minimize the automaton at each step.

Appendix 0.B Specification of Mine-pump and Arbiter example in DCSynth

The specification of Arbiter(5,3,2) and MinePump(8,2,6,2) is DCSynth syntax is given is Figure 3 and 4 respectively.

Appendix 0.C DCSynth Tool Usage and performance evaluation

The tool DCSynth uses a specification for Arbiter Arbiter.qsf shown in Figure 4. This file contains the set of input and output alphabets in interface section. The definitions/macros required for specifying hard and soft requirements are contained in definitions section. This is followed by a section called indefinitions, to specify the required indicating monitor for a given formula (or corresponding automaton). Finally the section called hardreq and softreq define the hard and soft requirements respectively using the definitions and indicating monitors. The steps to synthesize a controller from the specification file is as follows.

• •

First we generate the DFAs for $D^{h}$, $D^{s}$ and the required input/output partitioning file using qsf command, e.g. for Arbiter example, we use qsf Arbiter.qsf to generate files named Arbiter.hardreq.dfa, Arbiter.softreq.dfa and Arbiter.io as per step 1 of synthesis method in section 4.

• •

We then use the command synth2 Arbiter.hardreq.dfa Arbiter.softreq.dfa Arbiter.io synth.config to synthesize the supervisors as per step 2 and 3 of synthesis method in section 4. The file synth.config is used to provide the configuration parameters like the number of iterations for H-optimal supervisor. The command produces the supervisors MPS.dfa and MPHOS.dfa.

• •

We then determinize the MPHOS.dfa using default values with command synth_deterministic MPHOS.dfa default.io to get a controller called Controller.dfa. The file default.io contains the ordered list of output literals e.g. if we have two outputs o1 and o2, then the list {!o1,o2} says that try to determinize the MPHOS.dfa with following priority for the output {!o1,o2}$>>${!o1,!o2}$>>${o1,o2}$>>${o1,!o2}.

• •

To measure the expected value of the soft requirement being satisfied, the command aut2mrmc Controller.dfa default.io index is used. The index parameter is the index of indicator variable (for the soft requirement) in the Controller.dfa. The command produces Controller.tra and Controller.lab files which can be imported in tool MRMC to compute the expected value.

• •

Apart from expected case performance, the tool also facilitates the method for checking must dominance between two given supervisors $S_{1}$ and $S_{2}$. As supervisors are finite state mealy machines and a commitment $C$ is a regular property, we can use validity checking of QDDC to check whether $S_{1}\leq_{dom}^{C}S_{2}$ as formulated in the following proposition. In tool DCSynth, we provide a facility to decide must-dominance between two supervisors. The tool also gives a counter example if must-dominance fails.

Proposition 4

Let $\mathcal{D}(S_{i})$ denote QDDC formulas with same language as the supervisors $S_{i}$ and let $C$ be regular property over input-output alphabet $(I,O)$. Then, $S_{1}\leq_{dom}^{C}S_{2}$ iff

[TABLE]

We use this facility to compare supervisors obtained from different types of specifications discussed in Section 5.1

Appendix 0.D Synthesis with Semi-Symbolic DFA

An interesting representation for total and deterministic finite state automata was introduced and implemented by Klarlund et al in the tool MONA[15]. It was used to efficiently compute formula automaton for MSO over finite words. We denote this representation as Semi-Symbolic DFA (SSDFA). In this representation, the transition function is encoded as multi-terminal BDD (MTBDD). The reader may refer to original papers [15, 16] for further details of MTBDD and the MONA DFA library.

Here, we briefly describe the SSDFA representation, and then consider controller synthesis on SSDFA. Figure 5(a) gives an explicit DFA. Its alphabet $\Sigma$ is 4-bit vectors giving value of propositions $(r_{1},r_{2},a_{1},a_{2})$ and set of states $S=\{1,2,3,4\}$. This automaton has a unique reject state 4 and all the missing transitions are directed to it. (State 4 and transitions to it are omitted in Figure 5(a) for brevity.)

Figure 5(b) gives the SSDFA for the above automaton. Note that states are explicitly listed in the array at top and final states are marked as $1$ and non-final states marked as $-1$. (For technical reasons there is an additional state [math] which may be ignored here and state 1 may be treated as the initial state). Each state $s$ points to shared MTBDD node encoding the transition function $\delta(s):\Sigma\rightarrow S$ with each path ending in the next state. Each circular node of MTBDD represents a decision node with indices $0,1,2,3$ denoting variables $r_{1},r_{2},a_{1},a_{2}$. Solid edges lead to true co-factors and dotted edges to false co-factors.

MONA provides a DFA library implementing automata operations including product, complement, projection and minimization on SSDFA. Moreover, automata may be constructed from scratch by giving list of states and adding transitions one at a time. A default transition must be given to make the automaton total. Tools MONA and DCVALID use eager minimization while converting formula into SSDFA.

Remark 1: DFA in Figure 5 also denotes a Output-nondeterministic Mealy machine with input alphabet $(r_{1},r_{2})$ and output alphabet $(a_{1},a_{2})$. Automaton is nondeterministic in its output as $\delta(1,(1,1,1,0))$ $=2$ and $\delta(1,(1,1,0,1))=3$.

We use SSDFA to efficiently synthesize the MPS and MPHOS for the DCSynth specification $(I,O,D^{h},D^{s})$, without actually expanding the specification automata into game graph. The use of SSDFA leads to significant improvement in the scalability and computation time of the tool.

0.D.1 Computing Maximally Permissive Supervisor (MPS)

Recall the synthesis method in Section 4. Let the hard requirement automaton be $A(D^{h})=\langle S,2^{I\cup O},\delta,F\rangle$. We construct the maximally permissive supervisor by iteratively applying $Cpre(A(D^{h}),X)$ to compute set of winning states $G$, as outlined section 4.1. This requires efficient implementation of $\mathit{Cpre(A(D^{h}),X)}$ over SSDFA $A(D^{h})$. The symbolic algorithm for $\mathit{Cpre}$ marks, (a) each leaf node representing state $s$ by truth value of $s\in X$, (b) each decision node associated with an input variable with $AND$ of its children’s value, and (c) each decision node associated with output variable with $OR$ of its children’s value. The computation is carried out bottom up on MTBDD and takes time $|MTBDD|$, where $|MTBDD|$ is the number of BDD nodes in it. In contrast the enumerative method for implementation of $Cpre$ would have taken time of the order of $2^{|I\cup O|}$.

Next we compute the automaton $MPS(D^{h})=\langle G\cup\{r\},2^{I\cup O},G,\delta^{\prime}\rangle$ by only retaining transitions between the winning states $G$. Here $r$ is the unique reject state introduced to make the automaton total. We consider the following two methods.

• •

Enumerative method: $MPS(D^{h})$ is constructed from $\mathcal{A}(D^{h})$ by adding a transition at a time as follows: for any $s\in G$ if $\delta(s,(i,o))\in G$ then $(s,(i,o),\delta(s,$ $(i,o))\in\delta^{\prime}$. Clearly, this algorithm has time complexity $|S|\times 2^{|I\cup O|}$. Finally, we make $A^{mps}$ total by adding all the unaccounted transitions from any state to the reject state $r$.

• •

Symbolic method: in this method, the MTBDD of $\mathcal{A}(D^{h})$ is modified so that each edge pointing to a state in $S-G$ is changed to go to the reject state $r$. Note that this makes states in $S-(G\cup\{r\})$ inaccessible. Now this modified SSDFA is minimized to get rid of inaccessible states and to get smaller MPS. The time complexity of this computation is $O(|MTBDD|)$ for modifying the links and $N.t.log(N)$ for minimization where $N$ is number of states and $t$ is the size of alphabet in $A(D^{h})$.

In Table 3 we give experimental results comparing the computation of $MPS(D^{h})$ using the two algorithms. It can be seen that the symbolic algorithm can be faster by several orders of magnitude. This is because we do not construct the MPS from scratch; instead we only redirect some links in MTBDD of $A(D^{h})$ which is already computed. The Mine-pump specification used in the Table 3 is given in Section 5.3.

0.D.2 Computing $H$-Optimal Supervisor (MPHOS)

In this step we compute the MPHOS from MPS. For a given maximally permissive supervisor MPS, a QDDC formula $D$ and an integer parameter H. We get the H-optimal sub-supervisor of MPS called MPHOS by iteratively computing $Val(s,p+1)$ from $Val(s,p)$ for $0\leq p<H$ as outlined in Section 4.2 444Note that the tool DCSynth in general allows a lexicographical list of soft requirement, it is basically a lexicographical list of several QDDC formulas. The tool DCSynth implements a MPHOS computation based on this lexicographical (or with explicit weight to each soft requirement) list by using the weight for each transition as the sum of weights of all the soft requirement being satisfied on that transition. The tool also allows the discounting factor $\gamma$ which is used to give higher weight to the requirements being satisfied in near future. This step can be denoted by $\mathit{VALPre(\mathcal{A}^{Arena})}$.

Remark 2: For $\mathcal{A}^{Arena}$ a transition has the form $\delta(s,(i,o,v))$ with $i\in 2^{I},o\in 2^{O},v\in 2^{\{w\}}$. However, from the definition of $Ind(D^{s},w)$, the value of $w$ is uniquely determined by $(s,(i,o))$ in the corresponding automaton $\mathcal{A}(Ind(D^{s},w))$. Hence we can abbreviate the transition as $\delta(s,(i,o))$. ∎

Now to compute $MPHOS$ we again have two methods: one is enumerative and other is symbolic method. We give the algorithm and associated complexity results for one value iteration (i.e. for $\mathit{VALpre}$ followed by $O_{max}$ computation. Let $Q$ be the set of states of $\mathcal{A}^{Arena}$.

• •

Enumerative Method: As given in Step (3) of synthesis method, for each state $s$ we need to enumerate all paths starting from $s$ to get $Val(s,p+1)$ from $Val(s,p)$, which will take time of the order of $2^{|I\cup O|}\times k$, where $k$ is the number of soft requirements (In this paper $k$ is assumed to be 1). Similar complexity will be required to get the list of transitions with maximum values denoted as $o_{max}$ (Note that there can be multiple transitions with same $o_{m}ax$, all such transitions will be included in MPHOS). Hence, As the algorithm terminates after $H$ iterations the total time complexity of entire algorithm for $H$ iteration is $|Q|\times 2^{|I\cup O|}\times H$ (for $k=1$).

• •

Symbolic method: For this optimization to be applicable we assume that in MTBDD representation of $A^{Arena}$, all the input variables occur before the output variables $O$ and the indicating variable $w$ (in general it can be a set if $k>1$). A node in MTBDD is called a frontier node if it is labelled with an output or a witness variable, and all its ancestors are labelled with input variables. For example, in Figure 5(b), these are nodes labelled 2 (they happen to occur at same level in this example). For each frontier node enumerate each path $\pi$ within the MTBDD below the frontier node (this fixes values of $(o,w)\in 2^{O}\times 2^{W}$ occurring on $\pi$ as well as next state $s^{\prime}$). Update the optimal $o_{max}$ as well as next state $s_{o}$ based on $wt(o,v)$ for paths seen so far. This takes time $O(d_{f}\times k)$ where $d_{f}$ is the number of paths in $MTBDD$ below the frontier node $f$. This optimal output $o_{max}(f)$ as well as next state $s_{o}$ for each value iteration is stored in each frontier node $f$. The total time taken is $O(d_{output}\times H)$ where $d_{output}=\Sigma_{f\in Fr}~{}d_{f}$ and $Fr$ is the set of all frontier nodes. $H$ is the number of steps in value iterations.

In second step, for each state $s\in Q$, enumerate each path from state $s$ to a frontier node $f$. This fixes the valuation of input $x$. Insert a transition $\delta_{mphos}(s,(x,o_{max}))=s_{o}$ to $\mathcal{A}^{mphos}$. Let the total number of paths up to frontier nodes be $d_{input}$. Then the second step takes time $O(d_{input}+|Q|)$ where time taken to insert a transition in $\mathcal{A}^{mphos}$ is assumed to be constant. Hence total time for entire algorithm is $\mathcal{A}^{mphos}$ is $O(d+|Q|)\times H$ where $d$ is total number of paths in MTBDD of $\mathcal{A}^{Arena}$ (here $k$ is assumed to be 1).

It may also be noted that in worst case, the total number of MTBDD paths $d$ is of size $O(2^{|I\cup O|})$ and two algorithms have comparable complexity. But in most cases, the total number of MTBDD paths $d\ll 2^{|I\cup O|}$ and the symbolic algorithm turns out to be more efficient.

0.D.3 Computing a Controller using default value

The controller can be computed from MPHOS for a given default value order $ord$, using the similar algorithm as given for MPHOS computation. Here we assume that the default values provided are the soft requirements and $H$ is equal to 1. So the MPHOS computation algorithm will try to choose those transitions with outputs that locally satisfy the default values given in $ord$. As the $ord$ provides default values for every output variable, so there will always be a unique output that will maximally satisfy the default value. Hence, the output will always be a deterministic Mealy machine i.e., we will get a controller.

Appendix 0.E Comparison with Other tools

In Table 4 we have compared the performance of DCSynth with few leading tools for LTL synthesis. The examples in QDDC are manually translated into bounded LTL properties for giving them as input to Acacia+ [5] and BoSy [11]. We have only considered examples with hard requirements as these tools do not support soft requirements. The on-line version of BoSy tool was used which enforces a maximum timeout of 600 seconds. For other tools, a local installation on Linux (Ubuntu 16.04) system with Intel i5 64 bit, 2.5 GHz processor and 4 GB memory was used with a time out of 3600 seconds. In this comparison DCSynth was used with symbolic algorithm for both MPS and MPHOS computation. Note that for these examples the MPHOS algorithm will always terminate after 1 iteration only, as the examples do not have soft requirements, so DCSynth chooses one of the possible outputs from the MPS based on default output order. We have provided default output order for all types of arbiter example as $a_{1}>\ldots>a_{i}$ and for Mine-pump example it is $PumpOn$.

As the comparison table above shows, the DCSynth approach seems to outperform the state-of-the-art tools in scalability and controller computation time. This is largely due to the pragmatic design choices made in the logic QDDC and tool DCSynth.

It can also be seen that BoSy often results in controller with fewer states. BoSy is specifically optimized to resolve non-determinism to get fewer states. In our case, the tool is optimized to satisfy maximal number of soft requirements. It would be interesting to merge the two techniques for best results.

Appendix 0.F Measuring latency using Model Checking

Plethora of synthesis algorithms and optimizations give rise to diverse controllers for the same requirement. In comparing the quality of these different controllers, an important measure is their worst case latency. Latency can be defined as time (number of steps) taken to achieve some desired behaviour. In our framework, for latency specification, user must give a QDDC formula $D^{p}$ characterizing execution fragments of interest. For example the QDDC formula $D^{p}$ = [[req && !ack]] specifies fragments of execution with request continuously true but with no acknowledgment. Given a DFA (controller) $M$, the latency goal $MAXLEN(D^{p},M)$ computes $\sup\{e-b\mid\rho,[b,e]\models D^{p},\rho\in Exec(M)\}$, i. e. it computes the length of the longest interval satisfying $D^{p}$ across all the executions of $M$. Thus, it computes worst case latency for achieving behaviour $D^{p}$ in $M$. For example, given a synchronous bus arbiter controller $Arb$, goal $MAXLEN(\verb#[[req && !ack]]#,Arb)$ specifies the worst case response time of the arbiter $Arb$. Tool CTLDC, which like DCSynth and DCVALID is member of DCTOOLS suite of tools, provides efficient computation of $MAXLEN$ by symbolic search for longest paths as formulated in article [23]. This facility will be used subsequently in the paper to compare the worst case response times achieved by various controllers synthesized under different criteria.

Table. 5 gives worst case latency measurements carried out using tool CTLDC for various controllers synthesized using DCSynth. For Arbiter examples, worst case response time (maximum number of cycles a request remains true continuously, without an acknowledgment) is measured using a CTLDC formula MAXLEN([[$req_{i}$ && !$ack_{i}$]]), for each cell $i$ of various arbiters discussed in section 5. We use arbiter variants with 5 cells (i.e. $1\leq i\leq 5$) for our experiments.

• •

The specification $Arb^{hard}$ and $Arb^{hardAssume}$ do not have soft requirements, therefore guided synthesis will choose an arbitrary output from the constructed MPS, without any value iteration (i.e. H = 1). The results for these are described as follows

• –

$Arb^{hard}(5,5)$ has worst case response time for each cell as 5 cycles, this would happen when all the request lines are continuously $on$ and the controller gives acknowledgment to each cell in round robin fashion.

• –

$Arb^{hardAssume}(5,3,2)$ has worst case response for first cell is 2 cycles, whereas for all the other cells it is 3 cycles, provided the assumptions are met. If assumptions are not met, then 3 cycle response cannot be guaranteed (If request from all 5 cells is $on$ continuously). Assumption put a constraint that at most 2 requests can be $on$ at any point of time.

• •

For the specification $Arb^{soft}(5,3)$ the response requirement is that all the cell should get an acknowledgment within 3 cycles if the request is continuously true (it would be unrealizable if we use only hard requirement). However, a controller which satisfies these requirements as much as possible was generated using DCSynth.

• –

For example, $Arb^{soft}(5,3)$ “tries” to give acknowledgment within 3 cycles with higher priority assigned to higher numbered cell (see the description in Section 5). However, when all the requests are $on$ simultaneously then $req_{5}$ gets the highest priority and hence can always have worst case response time of 3 cycles, but $req_{1}$ given the lowest priority may end up with worst case response time of $\infty$ (when the request from higher number cell is always true).

• –

Another important observation is that DCSynth may generates different controllers for different horizons (value iterations) given for MPHOS computation. More intuitively, as the value of horizon tends to $\infty$, the controller produced reaches closer to the global optimality. This effect can be seen from row number 4–9, where the horizon moves from 1 to more than 2. For horizon $1$, DCSynth produces a locally optimal controller and hence the controller produced only guarantees the response time for the highest priority cell (i.e. cell no. 5, see row number 5). For all other cells the worst case response is $\infty$. When the horizon bound is increased to 2, the controller produced meets the response requirements for 2 cells (i.e. cell no. 4 and 5, see row number 7). Finally, when the bound is increase to 3 or more, the controller produced guarantees the worst case response for 3 cells (i.e. cell no. 3, 4 and 5 see row number 9). It can be seen that the maximum number of cells that can meet the 3 cycle response will be 3, in worst case. Therefore, increasing horizon beyond 3 does not change the result.