Practical Synthesis of Reactive Systems from LTL Specifications via Parity Games

TL;DR

This paper introduces an efficient, structured, and incremental automata-theoretic approach for synthesizing reactive systems from LTL specifications, implemented in the Strix tool, which outperforms other tools on benchmark sets.

Contribution

The paper presents a structured, forward, and incremental synthesis method with heuristics and symbolic representations, improving efficiency and scalability in LTL synthesis.

Findings

Strix outperforms other tools on Syntcomp benchmarks.

The approach reduces runtime and memory consumption.

Techniques for extracting implementations from automata are effective.

Abstract

The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption of the classic automata-theoretic approach to LTL synthesis, implemented in the tool Strix which has won the two last synthesis competitions (Syntcomp2018/2019). The presented approach is (1) structured, meaning that the states used in the construction have a semantic structure that is exploited in several ways, it performs a (2) forward exploration such that it often constructs only a small subset of the reachable states, and it is (3) incremental in the sense that it reuses results from previous inconclusive solution attempts. Further, we present and study different guiding heuristics that determine where to expand the on-demand constructed arena. Moreover, we show several techniques for extracting an implementation (Mealy machine or circuit) from the witness of the tree-automaton emptiness check. Lastly, the chosen constructions use a symbolic representation of the transition functions to reduce runtime and memory consumption. We evaluate the proposed techniques on the Syntcomp2019 benchmark set and show in more detail how the proposed techniques compare to the techniques implemented in other leading LTL synthesis tools.

Tables

Table 1. Table 1 : Overall results for Strix compared with its previous version, ltlsynt and BoSy . For Realisability and Synthesis , we give the number of solved instances (unique instances) and for Quality the total accumulated and the average points over solved synthesis instances.

		Strix	Strix	ltlsynt	BoSy
	max	(19.07)	(CAV’18)	(2.8.1)	(July ’19)
Realisability	434	415 (29)	374 (0)	353 (0)	344 (0)
Synthesis	337	304 (28)	264 (0)	254 (0)	234 (2)
Total Quality	674	571.66	425.17	242.82	416.94
Avg. Quality	2.00	1.88	1.61	0.96	1.78

Table 2. Table 2 : Time (s) to decide Realisability , comparing Strix with its previous version, ltlsynt and BoSy , both pairwise on the specifications with the 8 largest differences and on selected parameterised instances. We mark timeouts by time , memouts by mem , and errors by err .

				Strix	Strix	ltlsynt	BoSy
	Specification	$\left|{\mathrm{𝖠𝗉}}_{\text{in}}\right|$	$\left|{\mathrm{𝖠𝗉}}_{\text{out}}\right|$	(19.07)	(CAV’18)	(2.8.1)	(July ’19)
Strix (19.07) vs Strix (CAV’18)	simple_arbiter_10	10	10	2.4	1603.2	818.0	time
	detector_10	10	1	0.8	486.4	mem	506.0
	prioritized_arbiter_8	9	9	2.1	1048.6	2450.7	time
	ltl2dba_C2_10	10	1	1.1	457.2	mem	474.0
	detector_unreal_10	10	1	1.7	465.1	mem	13.1
	loadfull5	6	5	5.0	1253.9	3.5	10.9
	amba_decomposed_lock_8	17	1	1.8	301.0	18.4	2.5
	ltl2dba_theta_8	10	1	1.4	223.9	mem	96.5
Strix (19.07) vs ltlsynt (2.8.1)	ltl2dba_C2_8	8	1	1.2	17.8	3443.6	7.1
	detector_unreal_8	8	1	1.4	19.7	3320.2	1.5
	ltl2dpa22	6	3	1.2	time	2581.1	12.2
	prioritized_arbiter_8	9	9	2.1	1048.6	2450.7	time
	prioritized_..._unreal1_3_8	4	4	1.7	time	1686.7	time
	TorcsSteeringSmart	4	6	51.2	17.7	0.1	0.7
	torcs_steering_smart	4	6	49.4	16.9	0.1	0.6
	simple_arbiter_10	10	10	2.4	1603.2	818.0	time
Strix (19.07) vs BoSy (July ’19)	round_robin_arbiter_4	4	4	1.3	4.1	1.2	3178.3
	ltl2dba_Q_6	6	1	0.9	4.9	1.1	1539.9
	detector_10	10	1	0.8	486.4	mem	506.0
	ltl2dba_C2_10	10	1	1.1	457.2	mem	474.0
	SPIWriteManag	5	15	3.3	3.6	16.3	1076.3
	SPI	4	16	5.1	6.6	10.0	1341.1
	ltl2dba_R_6	6	1	4.8	time	mem	1167.0
	OneCounterGuiA6	9	9	2.9	7.3	79.0	464.7
selected parameterised instances	amba_..._arbiter_2	3	4	1.3	0.9	0.1	0.1
	amba_..._arbiter_4	5	6	1.7	1.4	1.0	4.8
	amba_..._arbiter_6	7	8	9.4	40.1	38.3	393.1
	amba_..._arbiter_8	9	10	177.7	1629.1	time	time
	full_arbiter_enc_6	3	3	11.7	2.0	17.2	200.0
	full_arbiter_enc_8	3	4	63.0	21.4	time	time
	full_arbiter_enc_10	4	4	337.8	303.7	time	time
	full_arbiter_enc_12	4	4	1274.5	time	time	time
	ltl2dba_beta_4	8	1	1.1	6.1	1.1	2.4
	ltl2dba_beta_6	12	1	1.5	237.0	72.5	152.5
	ltl2dba_beta_8	16	1	19.0	time	err	mem
	ltl2dba_beta_10	20	1	352.2	time	err	mem
	ltl2dba_Q_6	6	1	0.9	4.9	1.1	1539.9
	ltl2dba_Q_8	8	1	4.2	145.3	324.9	time
	ltl2dba_Q_10	10	1	47.5	time	time	time
	ltl2dba_Q_12	12	1	1042.4	time	time	time

Table 3. Table 3 : Size of AIG for Synthesis and Quality , comparing Strix with its previous version, ltlsynt and BoSy , pairwise on the specifications with the 8 largest differences. We mark timeouts by time , memouts by mem , and errors by err . The symbol ✓ denotes successful verification and 🕒 denotes a timeout during verification of the AIG.

				Strix		Strix		ltlsynt		BoSy
	Specification	$\left|{\mathrm{𝖠𝗉}}_{\text{in}}\right|$	$\left|{\mathrm{𝖠𝗉}}_{\text{out}}\right|$	(19.07)		(CAV’18)		(2.8.1)		(July ’19)
Strix (19.07) vs Strix (CAV’18)	tictactoe	9	9	0	✓	153	✓	time		time
	collector_v2_4	4	1	20	✓	2060	🕒	8292	✓	10	✓
	ltl2dba_Q_6	6	1	114	✓	9761	✓	16563	✓	48591	🕒
	collector_v4_7	7	1	57	✓	3547	🕒	time		time
	collector_v2_5	5	1	24	✓	1238	✓	time		time
	OneCounter	9	9	22	✓	870	✓	2534	✓	mem
	ltl2dba_C2_8	8	1	58	✓	2133	🕒	time		mem
	detector_8	8	1	58	✓	2133	🕒	time		440	✓
Strix (19.07) vs ltlsynt (2.8.1)	narylatch_10	11	10	186	🕒	time		6349541	🕒	time
	simple_arbiter_10	10	10	29	✓	mem		996921	🕒	time
	prioritized_arbiter_8	9	9	43	✓	mem		747766	🕒	mem
	ltl2dba_C2_6	6	1	31	✓	1071	✓	422872	🕒	468	✓
	detector_6	6	1	31	✓	1071	✓	422872	🕒	449	✓
	ltl2dba_E_10	10	1	29	✓	time		321799	🕒	time
	simple_arbiter_8	8	8	18	✓	mem		87834	🕒	21	✓
	narylatch_8	9	8	144	✓	mem		376661	🕒	time
Strix (19.07) vs BoSy (July ’19)	simple_arbiter_enc_6	3	3	751	✓	2699	🕒	5276	🕒	611824	🕒
	prioritized_arbiter_enc_6	3	3	1445	🕒	7938	🕒	66443	🕒	897716	🕒
	ltl2dba_Q_6	6	1	114	✓	9761	✓	16563	✓	48591	🕒
	full_arbiter_7	7	7	911	🕒	mem		112488	🕒	388240	🕒
	ltl2dba_E_6	6	1	17	✓	17	✓	3630	✓	5813	✓
	full_arbiter_6	6	6	373	✓	634	✓	28264	🕒	117163	🕒
	round_robin_arbiter_4	4	4	94	✓	239	✓	1928	✓	19738	✓
	full_arbiter_5	5	5	284	✓	351	✓	7039	✓	47570	🕒

Table 4. Table 4 : Cross-comparison of different tool. Each cell counts the number of instances where the result of the row tool is strictly better than the result of the column tool, comparing time for realisability and size of the AIG as the number of and gates plus number of latches. A time is only considered better if it is at least 5 seconds less than the other time.

	Time for realisability					Size of AIG
	Strix (19.07)	Strix (CAV’18)	ltlsynt (2.8.1)	BoSy (July ’19)		Strix (19.07)	Strix (CAV’18)	ltlsynt (2.8.1)	BoSy (July ’19)
Strix (19.07)	—	105	124	145		—	212	293	190
Strix (CAV’18)	25	—	80	98		31	—	242	125
ltlsynt (2.8.1)	22	34	—	77		0	23	—	82
BoSy (July ’19)	14	33	32	—		101	139	202	—

Table 5. Table 5 : Cross-comparison of different exploration strategies. Each cell counts the number of instances where the result of the row strategy is strictly better than the result of the column strategy. 𝒪 expl best superscript subscript 𝒪 expl best {\mathcal{O}}_{\textsf{expl}}^{\textsf{best}} is the best of the three other exploration strategies. A time is only considered better if it is at least 5 seconds less than the other time.

$\left|V_{\square }\right|$	${𝒪}_{\text{expl}}^{\text{bfs}}$	${𝒪}_{\text{expl}}^{\text{bfs+}}$	${𝒪}_{\text{expl}}^{\text{pq}}$	${𝒪}_{\text{expl}}^{\text{pq+}}$	${𝒪}_{\text{expl}}^{\text{best}}$
${𝒪}_{\text{expl}}^{\text{bfs}}$	—	10	45	36	5
${𝒪}_{\text{expl}}^{\text{bfs+}}$	30	—	50	37	11
${𝒪}_{\text{expl}}^{\text{pq}}$	31	28	—	6	5
${𝒪}_{\text{expl}}^{\text{pq+}}$	45	45	48	—	30

Table 6. Table 6 : Comparison of different exploration strategies for checking realisability.

	Explored states $\left|V_{\square }\right|$				Time for realisability (s)
Specification	${𝒪}_{\text{expl}}^{\text{bfs}}$	${𝒪}_{\text{expl}}^{\text{bfs+}}$	${𝒪}_{\text{expl}}^{\text{pq}}$	${𝒪}_{\text{expl}}^{\text{pq+}}$	${𝒪}_{\text{expl}}^{\text{bfs}}$	${𝒪}_{\text{expl}}^{\text{bfs+}}$	${𝒪}_{\text{expl}}^{\text{pq}}$	${𝒪}_{\text{expl}}^{\text{pq+}}$
amba_case_study_2	8187	3852	5598	2428	1008.9	451.4	707.3	306.8
collector_v3_5	78	73	148	54	2.3	2.3	4.3	2.6
collector_v3_6	148	147	206	32	6.5	6.0	13.0	4.6
collector_v3_7	306	305	386	22	42.2	39.9	94.0	18.2
detector_unreal_12	28	31	48	22	1.7	1.8	2.9	2.1
full_arbiter_unreal1_3_6	65536	65536	7475	6645	23.1	12.4	30.7	14.1
full_arbiter_unreal1_3_8	1685603	1678429	6576	6321	369.9	328.4	34.4	17.3
full_arbiter_unreal1_3_10	—	—	6812	6249	time	time	38.0	16.7
full_arbiter_unreal1_3_12	—	—	6899	6418	time	time	53.1	19.4
genbuf2	77479	61878	83025	35196	80.1	56.9	175.9	77.5
KitchenTimerV2	23	12	24	24	2.7	2.1	3.2	3.1
load_balancer_unreal1_2_10	2523	572	701	700	12.2	2.6	2.3	1.5
load_balancer_unreal1_2_12	10106	638	725	713	22.4	2.6	2.3	1.9
ltl2dba_R_6	162	80	29	14	4.7	4.0	3.8	3.0
ltl2dba_R_8	138	138	4	3	603.1	613.2	544.7	437.6
round_robin_[...]_unreal1_2_12	11703	16384	4096	4096	8.1	15.0	22.9	13.0
round_robin_[...]_unreal1_2_15	93623	93623	22509	21077	21.7	40.2	66.6	25.2
round_robin_[...]_unreal1_2_18	673158	669697	262144	45152	140.5	117.8	243.9	57.7
SliderDelayed	81	48	81	81	1.5	1.0	2.0	1.7
slider_delayed	50	81	81	81	1.3	1.4	2.2	1.4
TwoCounters3	11	11	99	99	9.1	8.2	44.5	40.4
TwoCountersInRangeM0	7	7	20	19	2.9	2.3	7.8	6.7
TwoCountersInRangeM1	7	7	24	23	2.7	2.4	9.1	7.9

Table 7. Table 7 : Cross-comparison of different minimisation strategies. Each cell counts the number of instances where the size of the AIG from the row strategy is strictly smaller than the result of the column strategy, and l best subscript 𝑙 best l_{\textsf{best}} gives the minimum over all three other strategies.

$\left|\text{AIG}\right|$	$l_{\text{unstr}}$	$l_{\text{unstr}}^{\text{min}}$	$l_{\text{struct}}$	$l_{\text{struct}}^{\text{min}}$	$l_{\text{best}}$
$l_{\text{unstr}}$	—	27	131	120	18
$l_{\text{unstr}}^{\text{min}}$	157	—	172	200	138
$l_{\text{struct}}$	80	61	—	71	29
$l_{\text{struct}}^{\text{min}}$	106	28	117	—	3

Table 8. Table 8 : Comparison for different minimisation strategies, giving the size of the AIG as the number of and gates plus number of latches. The symbol ✓ denotes successful verification and 🕒 denotes a timeout during verification of the AIG.

			${𝒪}_{\text{expl}}^{\text{bfs}}$	Size of AIG
Specification	$\left|{\mathrm{𝖠𝗉}}_{\text{in}}\right|$	$\left|{\mathrm{𝖠𝗉}}_{\text{out}}\right|$	$\left|V_{\square }\right|$	$l_{\text{unstr}}$		$l_{\text{unstr}}^{\text{min}}$		$l_{\text{struct}}$		$l_{\text{struct}}^{\text{min}}$
collector_v2_5	5	1	144	446	✓	24	✓	73	✓	35	✓
collector_v2_6	6	1	336	1610	✓	34	✓	101	✓	51	✓
collector_v2_7	7	1	607	3052	🕒	65	✓	113	✓	77	✓
collector_v4_6	6	1	184	772	✓	1216	✓	209	✓	2020	✓
collector_v4_7	7	1	375	1451	✓	57	✓	141	✓	173	✓
full_arbiter_6	6	6	645	373	✓	3865	🕒	758	✓	8469	🕒
full_arbiter_7	7	7	1422	911	🕒	10722	🕒	1080	✓	20349	🕒
full_arbiter_enc_8	3	4	15985	18533	🕒	11623	🕒	2904	🕒	31195	🕒
full_arbiter_enc_10	4	4	70662	time		147730	🕒	time		time
KitchenTimerV3	4	6	69	48	✓	1	✓	64	✓	14	✓
KitchenTimerV4	4	6	78	48	✓	1	✓	64	✓	14	✓
load_balancer_8	9	8	2250	12903	🕒	3751	✓	512	✓	4705	✓
ltl2dba_beta_6	12	1	49	1026	✓	1026	✓	90	✓	90	✓
ltl2dba_beta_8	16	1	81	1819	✓	1819	✓	151	✓	151	✓
ltl2dba_beta_10	20	1	121	2445	✓	2445	✓	156	✓	156	✓
ltl2dba_Q_6	6	1	170	3504	✓	3504	✓	114	✓	114	✓
ltl2dba_Q_8	8	1	986	31821	🕒	31821	🕒	187	✓	187	✓
ltl2dba_Q_10	10	1	5742	time		199301	🕒	243	✓	243	✓
ltl2dba_Q_12	12	1	33462	time		time		309	✓	time
prioritized_arbiter_enc_8	4	4	23554	57136	🕒	33762	🕒	3487	🕒	85101	🕒
prioritized_arbiter_enc_10	4	4	142337	time		time		6906	🕒	time
prioritized_arbiter_enc_12	4	4	593921	time		mem		12256	🕒	mem
round_robin_arbiter_7	7	7	9189	12119	🕒	843	✓	2535	✓	1183	✓
simple_arbiter_enc_8	3	4	10240	15906	🕒	11308	🕒	1317	🕒	24468	🕒
simple_arbiter_enc_10	4	4	65024	112422	🕒	62369	🕒	3356	🕒	time
TorcsSteeringSmart	4	6	421	4963	🕒	67	✓	5131	🕒	104	✓
torcs_steering_smart	4	6	421	5006	🕒	67	✓	5210	🕒	104	✓
Total solved and verified (unique)				292 (0)		299 (2)		300 (3)		298 (0)

Equations

$$\chi (q,a):=\{\begin{array}{ll}0& \text{if }(q,a,\delta (q,a))\in \alpha \\ 1& \text{otherwise}\end{array}$$

$$\chi (q,a):=\{\begin{array}{ll}0& \text{if }(q,a,\delta (q,a))\in \beta \\ 1& \text{otherwise}\end{array}$$

$$\chi (q,a):=\{\begin{array}{ll}p& \text{if δ(q,a)∈γ}\\ \overline{p}& \text{otherwise}\end{array}$$

$$\phi ::=$$

$$\psi ::=$$

$$\begin{array}[t]{lclclcl}w\models{\mathbf{tt}}\\ w\not\models{\mathbf{ff}}\\ w\models a&\mbox{ iff }&a\in w(0)\\ w\models\neg a&\mbox{ iff }&a\not\in w(0)\\ w\models\varphi\wedge\psi&\mbox{ iff }&w\models\varphi\text{ and }w\models\psi\\ w\models\varphi\vee\psi&\mbox{ iff }&w\models\varphi\text{ or }w\models\psi\\ w\models\varphi\leftrightarrow\psi&\mbox{ iff }&w\models\varphi\text{ if and only if }w\models\psi\\ w\models{\mathbf{X}}\varphi&\mbox{ iff }&w_{1}\models\varphi\\ w\models\varphi{\mathbf{U}}\psi&\mbox{ iff }&\exists k.\,w_{k}\models\psi\leavevmode\nobreak\ \text{ and }\leavevmode\nobreak\ \forall j<k.\,w_{j}\models\varphi\\ w\models\varphi{\mathbf{R}}\psi&\mbox{ iff }&\forall k.\,w_{k}\models\psi\leavevmode\nobreak\ \text{ or }\leavevmode\nobreak\ \exists k.\,w_{k}\models\varphi\leavevmode\nobreak\ \text{ and }\leavevmode\nobreak\ \forall j\leq k.\,w_{j}\models\psi\\ \end{array}$$

$$\varphi =\underset{{\psi }_0}{\underbrace{\mathbf{G}(\neg g_1\vee \neg g_2)}}\wedge \underset{{\psi }_1}{\underbrace{\mathbf{G}(r_1\to \mathbf{F}{g}_1)}}\wedge \underset{{\psi }_2}{\underbrace{\mathbf{G}(r_2\to \mathbf{F}{g}_2)}}$$

$$\begin{array}[]{lllllr}\alpha\Coloneqq&\phantom{\mid}\;\mathcal{B}_{\wedge}(\alpha,\alpha)&\mid\mathcal{C}_{\wedge}(\alpha,\alpha)&\mid\mathcal{P}_{\wedge}(\alpha,\alpha)&\mid\mathcal{W}_{\wedge}(\alpha,\alpha)&\\ &\mid\mathcal{B}_{\vee}(\alpha,\alpha)&\mid\mathcal{C}_{\vee}(\alpha,\alpha)&\mid\mathcal{P}_{\vee}(\alpha,\alpha)&\mid\mathcal{W}_{\vee}(\alpha,\alpha)&\\ &\mid\mathcal{B}_{\leftrightarrow}(\alpha,\alpha)&\mid\mathcal{C}_{\leftrightarrow}(\alpha,\alpha)&\mid\mathcal{P}_{\leftrightarrow}(\alpha,\alpha)&\mid\mathcal{W}_{\leftrightarrow}(\alpha,\alpha)&\\ &\mid\mathcal{B}(\varphi)&\mid\mathcal{C}(\varphi)&\mid\mathcal{P}(\varphi)&\mid\mathcal{W}(\varphi)&\text{ with }\varphi\in LTL\end{array}$$

$${\tau }_{\phi }=\{\begin{array}{ll}{\tau }_{{\psi }_1}\bigsqcup {\tau }_{{\psi }_2}& \text{if }\phi ={\psi }_{1}op{\psi }_2\text{ with }op\in \{\wedge ,\vee \}\\ \mathcal{W}& \text{if }\phi \in \mu LTL\cup \nu LTL\\ & \text{or if }\phi ={\psi }_1\leftrightarrow {\psi }_2\text{ and }\{{\tau }_{{\psi }_1},{\tau }_{{\psi }_2}\}=\{\mathcal{W}\}\\ \mathcal{B}& \text{if }\phi \in \mathbf{G}(\mu LTL)\\ \mathcal{C}& \text{if }\phi \in \mathbf{F}(\nu LTL)\\ \mathcal{P}& \text{otherwise}\end{array}$$

$${\mathcal{T}}_{\phi }=\{\begin{array}{ll}({\tau }_{\phi }{)}_{op}({\mathcal{T}}_{{\psi }_1},{\mathcal{T}}_{{\psi }_2})& \text{if }\phi ={\psi }_{1}op{\psi }_2\text{ with }op\in \{\wedge ,\vee ,\leftrightarrow \}\\ & \text{ and }\{{\tau }_{{\psi }_1},{\tau }_{{\psi }_2}\}\ne \{\mathcal{P}\}\\ {\tau }_{\phi }(\phi )& \text{otherwise}\end{array}$$

$$\alpha ::=$$

$$A({\mathcal{X}}_{\wedge }({\mathcal{W}}_1,{\mathcal{X}}_2))$$

$$\delta (q,a)$$

$$A({\mathcal{X}}_{\wedge }({\mathcal{C}}_1,{\mathcal{X}}_2))$$

$$\delta (q,a)$$

$$A({\mathcal{B}}_{\wedge }({\mathcal{B}}_1,\dots ,{\mathcal{B}}_n))$$

$$\delta ((q,r),a)$$

$$\chi ((q,r),a)$$

$$A({\mathcal{P}}_{\wedge }({\mathcal{B}}_1,{\mathcal{P}}_2))$$

$$\delta ((q,c),a)$$

$$\chi ((q,c),a)$$

$${\delta }^{\prime }(q,a)$$

$${\chi }^{\prime }(q,a)$$

$$A({\mathcal{W}}_{\leftrightarrow }({\mathcal{W}}_1,{\mathcal{W}}_2))$$

$$\delta (q,a)$$

$$A({\mathcal{P}}_{\leftrightarrow }({\mathcal{X}}_1,{\mathcal{X}}_2))$$

$$\delta ((q,c),a)$$

$$\chi (q,a)$$

$${\delta }^{\prime }(q,a)$$

$${\chi }^{\prime }(q,a)$$

$${\mathcal{O}}_{\text{expl}}^{\text{bfs}}(\alpha ,V_{\text{scalerel}\ast ◯\square },V_{\square },E,\chi ,B,q_0,p,\sigma ,\tau ):=\underset{b\in B}{\mathrm{argmin}}\text{dist}(V_{\text{scalerel}\ast ◯\square }\cup V_{\square },E,q_0,b)$$

$$\text{dist}(V,E,q_0,q):=\min \{\left|\pi \right|\mid \pi \text{ is a path from q0 to q in (V,E)}\}$$

$${\mathcal{O}}_{\text{expl}}^{\text{bfs+}}$$

$${\mathcal{O}}_{\text{expl}}^{\text{bfs}}(\alpha ,V_{\text{scalerel}\ast ◯\square },V_{\square },E,\chi ,\text{filter}(B),q_0,p,\sigma ,\tau )$$

Full text

††journal: Preprint

1 Introduction

Synthesis refers to the problem of finding for a formal specification of an input-output relation a matching implementation Pnueli:1989 , e.g. an (I/O)-transducer, a Mealy machine, a Moore machine or a circuit. In our case we focus on linear temporal logic (LTL) as the specification logic. While an asymptotically optimal synthesis algorithm has been given in Pnueli:1989 , this approach and other algorithms solving this task111See DBLP:reference/mc/BloemCJ18 for an introduction to reactive synthesis and related graph games. have not yet been successfully put into industrial practice. Tools able to deal with large specifications have been elusive and those that are available often produce subpar results compared to straight-forward manual implementations when successfully applied. DBLP:conf/sofsem/Kupferman12 identifies four challenges that hinder the practical impact of these synthesis algorithms: ‘algorithmic, methodological, scope, and qualitative’ DBLP:conf/sofsem/Kupferman12 . The first challenge is to find efficient synthesis algorithms. The second challenge is the discrepancy between the assumed synthesis setting and reality: a finished and complete specification is the exception and not the rule. Users often iterate specifications and thus this brings up the task of reusing and composing intermediate results. The third challenge is expressiveness and succinctness of input and output formats. Finally, the fourth challenge is not only to compute any valid solution, but to find implementations that have good quality. In this paper we primarily address the algorithmic and qualitative side of the synthesis problem, but also sketch ideas for the two other areas.

The classic automata-theoretic synthesis procedure using deterministic automata suffers from the ‘messy state space’ DBLP:conf/sofsem/Kupferman12 of Safra’s determinisation, which hinders efficient implementations that need to work on top of it. Moreover this automata-theoretic approach to synthesis requires the construction of a potentially double exponentially sized automaton (in the length of the specification) DBLP:conf/dagstuhl/2001automata . These two issues gave rise to ‘Safraless’ approaches DBLP:conf/cav/KupfermanPV06 ; DBLP:conf/cav/FaymonvilleFT17 ; DBLP:conf/cav/BohyBFJR12 ; DBLP:conf/cav/KhalimovJB13 ; DBLP:conf/tacas/Ehlers11 to avoid the complicated state structure and to alleviate the state space explosion problem. Further, bounded synthesis adds to the synthesis problem an additional size constraint on the matching implementation. This effectively turns the synthesis problem into a search problem.

We, on the other hand, address the ‘messy state space’ issue by employing a collection of ‘Safraless’ LTL to deterministic parity automaton (DPA) translations DBLP:conf/cav/SickertEJK16 ; DBLP:conf/tacas/EsparzaKRS17 ; DBLP:conf/lics/EsparzaKS18 in combination with a special product automaton construction that includes a latest appearance record (LAR) construction and a formula decomposition in the spirit of DBLP:journals/corr/abs-1006-1408 ; DBLP:journals/fmsd/FiliotJR11 ; DBLP:journals/fmsd/Ehlers12 ; DBLP:journals/corr/abs-1709-02102 . Our construction recovers the Boolean structure present in the input specification. The state explosion problem is tackled by exploring the on-demand constructed parity game using a forward search resembling the optimisation described in DBLP:journals/ijfcs/FriedmannL12 . This enables our customised strategy iteration DBLP:journals/corr/abs-0806-2923 to leave most of the arena (and thus of the automaton) unexplored. Further, the decomposition allows us to split-off formulas and use them to prune the search-space which is a generalisation of a central insight from DBLP:journals/sttt/SohailS13 .

Further, we propose two heuristics guiding the construction of the arena in directions of probably decisive regions and thus focussing on important states, while skipping irrelevant parts. One approach is agnostic about the internal structure of the parity game, while the other one extracts information from the special parity automaton construction. Lastly, since we use strategy iteration to compute winning strategies, we can reuse so-far constructed solution attempts after expanding the arena, thereby reducing the amount of iterations until stabilisation is reached. We believe that our approach could be adapted to cache intermediate results (constructed automata, partial strategies) when using LTL synthesis interactively to speed up synthesis, which addresses the second area.

Regarding the quality of the synthesised structures ‘there is no emphasize [sic] on constructing optimal or well-structured systems’ DBLP:conf/sofsem/Kupferman12 . While in this paper we do not look at general methods for producing qualitatively good solutions and do not support synthesis under a specific quality measure, we provide a set of best-effort heuristics to produce good solutions: we make use of a range of post-processing steps to ensure that the solution is as small as possible. We also provide a modular encoding of the product automata into circuits that retains the Boolean structure of the specification. This approach surprisingly yields on some of the specifications used in the experimental evaluation smaller circuits compared to extracting a circuit out of a minimised Mealy machine. This data suggests that minimisation of the implementation represented as a Mealy machine might be in some cases diametral to generating small circuits. It seems that this area has not been studied enough and we think enriching specifications with additional, explicit optimisation goals is worthwhile, but currently these ideas have not manifested in specifications such as the Syntcomp2019 benchmarks.

We implement and test the outlined ideas within Strix222https://strix.model.in.tum.de/ DBLP:conf/cav/MeyerSL18 , which relies on DBLP:conf/atva/KretinskyMS18 for automata translations and DBLP:conf/atva/MeyerL16 for parity game solving. An older version of Strix won in the TLSF/LTL track in all six categories of Syntcomp2018 against other mature tools such as ltlsynt DBLP:journals/corr/abs-1711-11439 , which also implements synthesis using parity games, and BoSy DBLP:conf/cav/FaymonvilleFT17 , which implements several bounded synthesis approaches. We further improve the prototype by representing the transition relation symbolically to address scalability issues for large alphabets and replace external tooling such as Speculoos with an internal implementation able to cope with larger systems. This newer version again won in all TLSF/LTL tracks of Syntcomp2019 against ltlsynt.

The rest of the paper is structured as follows: after introducing preliminaries, we give a high-level overview of the synthesis procedure and detail it in the following subsections. We then put our improvements to the test by evaluating them on the Syntcomp2019 benchmarks and comparing them with the old version, ltlsynt and BoSy. Each section, if appropriate, contains its specific discussion of related work.

Editorial Note.

This paper is an extended version of the preliminary report published in DBLP:conf/cav/MeyerSL18 . The synthesis approach is the same, but we give a much more detailed explanation of the techniques used, e.g., the decomposition and the product automaton construction. Further, we describe new extensions for different exploration strategies in Section 3.2.1 and different encoding strategies in Section 3.3.2. We also give an updated experimental evaluation on a larger set of benchmarks and a comprehensive comparison with the old version and other tools.

2 Preliminaries

2.1 $\omega$-Languages and $\omega$-Automata

Let $\Sigma$ be a finite alphabet. An $\omega$-word $w$ over $\Sigma$ is an infinite sequence of letters $a_{0}a_{1}a_{2}\dots$ with $a_{i}\in\Sigma$ for all $i\geq 0$ and an $\omega$-language is a set of $\omega$-words. The set of all $\omega$-words is denoted $\Sigma^{\omega}$. We denote the $i$-th letter of an $\omega$-word $w$ (starting at 0) by $w(i)$ and the infinite suffix $w(i)w(i+1)\dots$ by $w_{i}$.

In this paper we focus on deterministic $\omega$-automata with accepting conditions defined on transitions which is nowadays the preferred acceptance condition in implementations due to the succinctness and in-line with other recent papers and tools DBLP:conf/forte/GiannakopoulouL02 ; DBLP:conf/cav/BabiakBDKKM0S15 ; DBLP:conf/atva/Duret-LutzLFMRX16 ; DBLP:conf/atva/KretinskyMS18 . The discussed constructions can also be transferred to automata with acceptance defined on states with the folklore translation from transition acceptance to state acceptance.

A deterministic pre-automaton (DA) over $\Sigma$ is a tuple $(Q,\delta,q^{0})$ where $Q$ is a finite set of states, $\delta\colon Q\times\Sigma\rightarrow Q$ is a transition function, and $q^{0}$ is an initial state. A transition is a triple $(q,a,q^{\prime})$ such that $q^{\prime}=\delta(q,a)$.

A deterministic Parity automaton (DPA) is a deterministic pre-automaton automaton ${A}=(Q,\delta,q^{0},\chi,d,p)$ with the addition of the transition colouring $\chi\colon Q\times\Sigma\to\{0,1,\ldots,d\}$, $d\geq 1$ the maximal colour and $p\in\{0,1\}$ the parity that determines whether a run is accepting or not (as defined below). A run of $A$ on an $\omega$-word $w\colon{\mathbb{N}}_{0}\rightarrow\Sigma$ is an $\omega$-sequence of states $\rho\colon{\mathbb{N}}_{0}\rightarrow Q$ such that $\rho(0)=q^{0}$ and for all positions $i\in{\mathbb{N}}_{0}$, we have that $(\rho(i),w(i),\rho(i+1))\in\delta$. Given a run $\rho$ over a word $w$, the infinite sequence of colours traversed by the run $\rho$ is denoted by \chi(\rho)\coloneqq\bigl{(}\chi(\rho(i),w(i))\bigr{)}_{i\in{\mathbb{N}}_{0}}. The minimal colour appearing infinitely often along a run $\rho$ is $\liminf\chi(\rho)$. A run $\rho$ is accepting if $\liminf\chi(\rho)\equiv_{2}p$ (with $x\equiv_{2}y:\Leftrightarrow(x-y)\bmod{2}=0$). An $\omega$-word $w$ is in the language of ${A}$, denoted $w\in\mathcal{L}({A})$, iff the run for $w$ on ${A}$ is an accepting run.

For a parity $p\in\{0,1\}$, define $\overline{p}\coloneqq 1-p$ as the switched parity. Note that by changing the parity $p$ to $\overline{p}$, we obtain a complement automaton $\overline{{A}}\coloneqq(Q,\delta,q^{0},\chi,d,\overline{p})$ for which we have $\mathcal{L}(\overline{{A}})=\Sigma^{\omega}\setminus\mathcal{L}({A})$.

To change the parity $p$ to $\overline{p}$ while preserving the language, one can use ${A}^{\prime}\coloneqq(Q,\delta,q^{0},\chi^{\prime},d+1,\overline{p})$ with $\chi^{\prime}(q,a)\coloneqq\chi(q,a)+1$, which has one more colour and satisfies $\mathcal{L}({A}^{\prime})=\mathcal{L}({A})$.

A deterministic Büchi automaton (DBA) with the set of accepting transitions $\alpha$ is a DPA with colours $\{0,1\}$, parity [math] and $\chi$ defined as:

[TABLE]

A deterministic co-Büchi automaton (DCA) with the set of rejecting transitions $\beta$ is a DPA with colours $\{0,1\}$, parity $1$ and $\chi$ defined as:

[TABLE]

A deterministic weak automaton (DWA) with the set of accepting states $\gamma$ is a DPA with colours $\{0,1\}$ and parity [math] or $1$, where for each strongly connected component $S\subseteq Q$, either $S\subseteq\gamma$ or $S\cap\gamma=\emptyset$. Then $\chi$ is defined as:

[TABLE]

Note that for weak automata, we can switch between parity [math] and $1$ while preserving the language without increasing the number of colours.

A bottom state of a DPA is a special state $\bot\in Q$ such that $\delta(\bot,a)=\bot$ and $\chi(\bot,a)\equiv_{2}\overline{p}$ for each $a\in\Sigma$. A top state of a DPA is a special state $\top\in Q$ such that $\delta(\top,a)=\top$ and $\chi(\top,a)\equiv_{2}p$ for each $a\in\Sigma$.

2.2 Linear Temporal Logic

We present LTL DBLP:conf/focs/Pnueli77 with a larger than usual set of modal operators and Boolean connectives, instead of a minimalistic syntax often found in other publications. While a minimalistic syntax reduces the amount of cases, e.g., in an induction, we want to keep as much structure of the given formula as possible and thus add redundancy. In particular, we are going to present customised constructions in order to deal with the Boolean connective $\leftrightarrow$ that effectively reduces the size of the automaton that is constructed. We work with a syntax for LTL in which formulas within the scope of modal operators (${\mathbf{X}}$, ${\mathbf{U}}$) are written in negation-normal form, i.e., negations only occur in front of atomic propositions. Thus we need to introduce ${\mathbf{ff}}$, $\neg a$, $\vee$, and the temporal operator ${\mathbf{R}}$ (release) in order to remove $\neg$ from the syntax. It is easy to see that LTL formulas with the usual syntax can be translated to equivalent LTL formulas of the same size in our syntax. A formula of LTL over a set of atomic propositions ($\mathsf{Ap}$) is given by the following syntax:

Definition 1 (Syntax of LTL)

[TABLE]

We also define the usual abbreviations ${\mathbf{F}}\varphi\coloneqq{\mathbf{tt}}{\mathbf{U}}\varphi$ (eventually) and ${\mathbf{G}}\varphi\coloneqq{\mathbf{ff}}{\mathbf{R}}\varphi$ (always). The satisfaction relation $\models$ between $\omega$-words over the alphabet $\Sigma\coloneqq 2^{\mathsf{Ap}}$ and formulas is inductively defined as follows:

Definition 2 (Semantics of LTL)

[TABLE]

We denote by $\mathcal{L}(\varphi)$ the language of $\varphi$ defined as $\mathcal{L}(\varphi)\coloneqq\{w\in\Sigma^{\omega}\mid w\models\varphi\}$.

2.3 Notable Fragments of LTL

In the latter section we are going to consider the following four fragments of LTL:

• •

$\mu{LTL}$ and $\nu{LTL}$:

$\mu{LTL}$ is the fragment of LTL restricted to the temporal operator ${\mathbf{U}}$, the Boolean connectives $(\wedge,\vee)$, the literals $(a,\neg a)$, and the next operator $({\mathbf{X}})$. $\nu{LTL}$ is defined analogously, but with the operator ${\mathbf{R}}$ instead of ${\mathbf{U}}$. In the literature $\mu{LTL}$ is also called syntactic co-safety and $\nu{LTL}$ syntactic safety.

• •

${\mathbf{G}}(\mu{LTL})$ and ${\mathbf{F}}(\nu{LTL})$:

These fragments contain the formulas of the form ${\mathbf{G}}\varphi$, where $\varphi\in\mu{LTL}$, and ${\mathbf{F}}\varphi$, where $\varphi\in\nu{LTL}$.

The reason for the names $\mu{LTL}$ and $\nu{LTL}$ is that ${\mathbf{U}}$ is a least-fixed-point operator, in the sense that its semantic is naturally formulated by a least fixed point, e.g., in the $\mu$-calculus, while the semantics of ${\mathbf{R}}$ is naturally formulated by a greatest fixed point.

For all these fragments several translations to deterministic automata are known and we are going to use the constructions for $\mu{LTL}$, $\nu{LTL}$, ${\mathbf{G}}{\mathbf{F}}(\mu{LTL})$, and ${\mathbf{F}}{\mathbf{G}}(\nu{LTL})$ described in DBLP:conf/lics/EsparzaKS18 , for ${\mathbf{G}}(\mu{LTL})$ and ${\mathbf{F}}(\nu{LTL})$ the construction described in DBLP:conf/cav/SickertEJK16 , and for arbitrary LTL formulas the construction described in DBLP:conf/tacas/EsparzaKRS17 . It should be noted that of course these constructions can be swapped with other constructions, but some of the implemented heuristics rely on the specific state structure these constructions yield.

2.4 Synthesis Problem

Let $\varphi$ be a specification given as an LTL formula and let the atomic propositions $\mathsf{Ap}={\mathsf{Ap}_{\textsf{in}}}\uplus{\mathsf{Ap}_{\textsf{out}}}$ be partitioned into input symbols ${\mathsf{Ap}_{\textsf{in}}}$ and output symbols ${\mathsf{Ap}_{\textsf{out}}}$. We then define $\Sigma\coloneqq 2^{\mathsf{Ap}}$, $\Sigma_{\textsf{in}}\coloneqq 2^{\mathsf{Ap}_{\textsf{in}}}$, and $\Sigma_{\textsf{out}}\coloneqq 2^{\mathsf{Ap}_{\textsf{out}}}$.

Then the synthesis problem is to decide if a function $\sigma:\Sigma_{\textsf{in}}^{*}\to\Sigma_{\textsf{out}}$ exists such that for every $\omega$-word $v\in\Sigma_{\textsf{in}}^{\omega}$, the $\omega$-word $w\in\Sigma^{\omega}$ defined by $w(i)\coloneqq v(i)\cup\sigma(v(0)v(1)\ldots v(i))$ satisfies $w\in\mathcal{L}(\varphi)$. In the positive case, also a finite and executable representation of $\sigma$ in the form of a controller should be produced, e.g., a Mealy machine or a circuit.

3 Synthesis Procedure

We start with an overview on how Strix constructs parity games from specification formulas and solves them. For the controller extraction we refer the reader to Section 3.3. We illustrate the intuition of Algorithm 1 using a simple arbiter example and refer to functionality explained in subsequent sections via oracles: First, the formula is analysed with ${\mathcal{O}}_{\mathcal{T}}$ and a DPA is constructed on-the-fly via ${\mathcal{O}}_{q_{0}}$, ${\mathcal{O}}_{p}$, and ${\mathcal{O}}_{\delta}$. Second, the DPA is interpreted as a parity game and the game is solved via ${\mathcal{O}}_{\textsf{win}}$ computing the winning regions. Further an exploration heuristic (${\mathcal{O}}_{\textsf{expl}}$) guides which parts of the parity games are extended. To be more precise, we use the following oracles:

• •

${\mathcal{O}}_{\mathcal{T}}(\varphi)$: Given the formula $\varphi$, the oracle returns an annotated formula $\alpha$ that labels syntax nodes with a recommended automaton type to be used for this subformula for translation and how to compose a (product) DPA from these components.

• •

${\mathcal{O}}_{q_{0}}(\alpha)$: Given the annotated formula $\alpha$, the oracle returns the initial state $q_{0}$ of the (product) DPA recognising $\varphi$.

• •

${\mathcal{O}}_{p}(\alpha)$: Given the annotated formula $\alpha$, the oracle returns the parity $p$ of the (product) DPA recognising $\varphi$.

• •

${\mathcal{O}}_{\delta}(\alpha,q)$: Given the annotated formula $\alpha$ and a (product) state $q$, the oracle returns a set of outgoing transitions from $q$. The elements of the set are tuples $(I,O,c,q^{\prime})$, where $I\subseteq\Sigma_{\textsf{in}}$ are the input letters, $O\subseteq\Sigma_{\textsf{out}}$ are the output letters, $c$ is the colour of the transition and $q^{\prime}$ is the successor state. Formally for each such tuple $(I,O,c,q^{\prime})$ we have $\delta(q,i\cup o)=q^{\prime}$ and $\chi(q,i\cup o)=c$ for all $i\in I$ and $o\in O$. The oracle will return $q^{\prime}=\bot$ for states that are trivially losing for the system and $q^{\prime}=\top$ for states that are trivially winning.

• •

${\mathcal{O}}_{\textsf{win}}$: Given $(V_{\mathord{\scalerel*{\bigcirc}{\square}}},V_{\mathbin{\square}},E,\chi,B,q,\mathsf{P},p,\kappa)$, compute whether the state $q$ is won by player $\mathsf{P}\in\{{\mathord{\scalerel*{\bigcirc}{\square}}},{\mathbin{\square}}\}$, where $V_{\mathord{\scalerel*{\bigcirc}{\square}}}$ is the set of nodes from which player ${\mathord{\scalerel*{\bigcirc}{\square}}}$ moves, $V_{\mathbin{\square}}$ is the set of nodes from which player ${\mathbin{\square}}$ moves, $E\subseteq\left(V_{\mathord{\scalerel*{\bigcirc}{\square}}}\cup V_{\mathbin{\square}}\right)\times 2^{\Sigma}\times\left(V_{\mathord{\scalerel*{\bigcirc}{\square}}}\cup V_{\mathbin{\square}}\right)$ is the labeled edge relation, $\chi\colon E\to{\mathbb{N}}_{0}$ is an edge colouring, $B\subseteq V_{\mathbin{\square}}$ is the set of boundary nodes (i.e. nodes whose successors have yet to be constructed), $p$ is the parity for player $\mathsf{P}$, i.e. player $\mathsf{P}$ wins if the minimal colour occurring infinitely often along the edges of a play has parity $p$, and $\kappa$ is an initial (partial, nondeterministic)333We will later see the advantage of using nondeterministic strategies (multiple actions allowed) compared to deterministic strategies (only one action allowed). strategy for player $\mathsf{P}$. ${\mathcal{O}}_{\textsf{win}}$ also returns an updated strategy $\kappa^{\prime}$, which is winning from $q$ for $\mathsf{P}$ if $q$ is won by player $\mathsf{P}$. Depending on the player $\mathsf{P}$ boundary nodes are declared as winning for the opponent in order to correctly under-approximate the parity game on the completely constructed arena.

• •

${\mathcal{O}}_{\textsf{expl}}$: Given a set $B$ of boundary nodes, the so far constructed arena and the intermediate strategies, the oracle returns a nonempty subset of $B$ of nodes that should be further explored.

We use the specification of a simple arbiter as an example. In this setting two processes ($i\in\{1,2\}$) request access to the critical section by raising the flag $r_{i}$ and the arbiter eventually grants access to process $i$ by raising $g_{i}$. Thus we have ${\mathsf{Ap}_{\textsf{in}}}=\{r_{1},r_{2}\}$ and ${\mathsf{Ap}_{\textsf{out}}}=\{g_{1},g_{2}\}$ and the following specification:

[TABLE]

Applying the annotation oracle, we obtain from the specification $\phi$ an annotated syntax tree $\alpha$ shown in Fig. 1 that represents a decomposition of $\phi$ into subformulas w.r.t. the weakest class of deterministic automata needed for their translation and how to combine the automata in order to obtain the automaton for $\phi$ itself. In our example, $\psi_{0}$ is a simple mutex requirement which is classified as recognisable by a DWA (denoted by $\mathcal{W}$), and $\psi_{1}$ and $\psi_{2}$ are fairness requirements that are classified as recognisable by a DBA (denoted by $\mathcal{B}$). The conjunctions $\psi_{1}\wedge\psi_{2}$ and $\phi$ itself are then also recognisable by a DBA (denoted by $\mathcal{B}_{\wedge}$). The corresponding automata are displayed in Fig. 2.

We query ${\mathcal{O}}_{q_{0}}(\alpha)$ and obtain $q_{0}\coloneqq(a_{0},((b_{0},c_{0}),0))$, which matches the tree structure of $\alpha$. Here, we have add a round-robin counter $r\in\{0,1\}$ for the intersection of the two Büchi automata representing $\psi_{1}$ and $\psi_{2}$: This round-robin counter remembers which of the two Büchi automata is due to take an accepting transition. To ease notation for our example and the corresponding figures we flatten $(a_{0},((b_{0},c_{0}),0))$ to $(a_{0},\underline{b_{0}},c_{0})$ with the underlined state representing the round-robin counter. Further, we query ${\mathcal{O}}_{p}(\alpha)$ for the parity associated with the controller, i.e. player ${\mathord{\scalerel*{\bigcirc}{\square}}}$. In our example it is [math] and ${\mathord{\scalerel*{\bigcirc}{\square}}}$ wins a play if the minimal colour encountered infinitely often is even.

As we are using Mealy semantics, we let the environment ${\mathbin{\square}}$ move from the initial node $(a_{0},\underline{b_{0}},c_{0})$. Our parity game also includes two nodes $\bot$ and $\top$ where by our construction $\bot$ is always won by the environment ${\mathbin{\square}}$, while $\top$ is always won by the controller ${\mathord{\scalerel*{\bigcirc}{\square}}}$.

We now start the on-the-fly forward exploration of parity game arena. In every iteration of the while-loop in Algorithm 1 we extend the boundary $B$. The boundary always consists of nodes belonging to the environment ${\mathbin{\square}}$ whose successors have yet to be explored. Initially the boundary is just the initial node of the parity game, in our example $B=\{(a_{0},\underline{b_{0}},c_{0})\}$.

As initially $B$ is a singleton set, ${\mathcal{O}}_{\textsf{expl}}$ tells us to explore all direct successors of $q_{0}=(a_{0},\underline{b_{0}},c_{0})$. ${\mathcal{O}}_{\delta}(\alpha,q_{0})$ groups the outgoing transitions $\delta(q_{0},\star)$ using $\Sigma_{\textsf{in}}$ and $\Sigma_{\textsf{out}}$ as previously mentioned as a set of tuples of the shape $(I,O,q^{\prime},c)$. Due to the Mealy semantics each such tuple $(I,O,q^{\prime},c)$ is broken up in two steps: starting in $q_{0}$, first the environment issues a signal $i\in I$, which leads the game into the intermediate state $(q_{0},I)$;444We represent the intermediate states simply by circular shaped nodes in the figures. as this is only an intermediate step the corresponding edge is assigned the (w.r.t. min-parity) ‘neutral’ colour $\infty$; in $(q_{0},I)$ the controller ${\mathord{\scalerel*{\bigcirc}{\square}}}$ then issues a signal $o\in O$ leading to the next state of the DPA. We illustrate this using our example: we have $4$ choices for the inputs at $(a_{0},\underline{b_{0}},c_{0})$:

$\overline{r_{1}}\,\overline{r_{2}}=\{\emptyset\}$, i.e. no process requests access; 2. 2.

$r_{1}\,\overline{r_{2}}=\{\{r_{1}\}\}$, i.e. only process $1$ requests access; 3. 3.

$\overline{r_{1}}\,r_{2}=\{\{r_{2}\}\}$, i.e. only process $2$ requests access; and 4. 4.

$r_{1}\,r_{2}=\{\{r_{1},r_{2}\}\}$, i.e. both processes want to access the critical section.

Consider the case that the environment chooses the input $I=r_{1}\,\overline{r_{2}}$. ${\mathcal{O}}_{\delta}$ groups the outputs available to ${\mathord{\scalerel*{\bigcirc}{\square}}}$ into the three groups $g_{1}\,g_{2}$ (grant access to both processes), $g_{1}\,\overline{g_{2}}$ (grant access to only process 1), and $\overline{g_{1}}$ (do not grant access to process 1). In case of $O=\overline{g_{1}}=\{\{\},\{g_{2}\}\}$, the DBA ${\mathcal{A}}_{\psi_{1}}$ takes a non-accepting transition, hence, the round-robin counter stays unchanged, while the other two automata take a loop, arriving at state $(a_{0},\underline{b_{1}},c_{0})$ in the product; ${\mathcal{O}}_{\delta}$ determines by analysing $\alpha$ that we only need the colours $\{0,1\}$ for the parity game under construction; as ${\mathcal{A}}_{\psi_{1}}$ takes a non-accepting transition, ${\mathcal{O}}_{\delta}$ gives the input-output pair $(I,O)=(r_{1}\,\overline{r_{2}},\overline{g_{1}})$ a colour of parity $\overline{p}$ in order to prevent ${\mathord{\scalerel*{\bigcirc}{\square}}}$ from replying to $r_{1}\,\overline{r_{2}}$ by $\overline{g_{1}}$ infinitely often. Thus $(r_{1}\,\overline{r_{2}},\overline{g_{1}},1,(a_{0},\underline{b_{1}},c_{0}))\in{\mathcal{O}}_{\delta}(\alpha,q_{0})$. For $O=g_{1}\,\overline{g_{2}}$ we obtain analogously the entry $(r_{1}\,\overline{r_{2}},g_{1}\,\overline{g_{2}},0,(a_{0},\underline{b_{0}},c_{0}))$: as all automata take an accepting loop in this case the input-output pair is given the colour [math] and, as the round-robin counter is incremented twice, we are back in the initial node of the parity game. Finally, for $O=g_{1}\,g_{2}$ the oracle ${\mathcal{O}}_{\delta}$ determines that ${\mathord{\scalerel*{\bigcirc}{\square}}}$ has no chance of winning anymore as the DWA ${\mathcal{A}}_{\psi_{0}}$ representing the mutex requirements cannot reach an accepting transition anymore; for this reason, ${\mathcal{O}}_{\delta}$ simplifies the successor state to $\bot$ which by construction is always won by the environment ${\mathbin{\square}}$ and includes the tuple $(r_{1}\,\overline{r_{2}},g_{1}g_{2},1,\bot)$ into its output.555Should ${\mathcal{O}}_{\delta}$ determine that all automata will accept any possible input-output pairs from now on, it simplifies the successor state to $\top$ which, again by construction, is always won by ${\mathord{\scalerel*{\bigcirc}{\square}}}$. Analogously, ${\mathcal{O}}_{\delta}$ handles the other three possible inputs by ${\mathbin{\square}}$ which eventually leads to the arena shown in Fig. 3 with border $B=\{(a_{0},\underline{b_{0}},c_{1}),(a_{0},b_{0},\underline{c_{1}}),(a_{0},\underline{b_{1}},c_{1})\}$.

We now run the parity game solver, i.e. query ${\mathcal{O}}_{\textsf{win}}$ for the so-far constructed arena. We first mark the boundary nodes as losing for the controller and ask ${\mathcal{O}}_{\textsf{win}}$ for an optimal winning strategy for the controller. In this case, this leads to the nondeterministic strategy $\sigma$ depicted in Fig. 4 where the thick edges in dark green belong to $\sigma$, while edges disabled by $\sigma$ are drawn as dashed lines. We will describe our instantiation of ${\mathcal{O}}_{\textsf{win}}$ in Section 3.2 in more detail, but intuitively ${\mathcal{O}}_{\textsf{win}}$ tries to maximise the distance from the trivial losing states $\bot$ and the boundary $B$ with each colour interpreted as a distance; hence, in the intermediate states corresponding to $I\in\{\overline{r_{1}}\,r_{2},\overline{r_{1}}\,\overline{r_{2}},r_{1}\,\overline{r_{2}}\}$, ${\mathcal{O}}_{\textsf{win}}$ chooses to let the controller play back to the initial state so that ideally never the losing state is reached and thus the distance to it is maximised. One particular feature of our instantiation of ${\mathcal{O}}_{\textsf{win}}$ is that it outputs nondeterministic strategies, i.e. a strategy $\sigma$ for ${\mathbin{\square}}$ is still required to respect the edge relation of the parity game but $\sigma(q)$ is only required to be some subset of the successors of $q$ in the parity game; in particular $\sigma(q)=\emptyset$ is allowed and has to be interpreted as ${\mathord{\scalerel*{\bigcirc}{\square}}}$ giving up at node $q$ which is the case of the strategy shown in Fig. 4 at the intermediate node $(q_{0},r_{1}\,r_{2})$. Note that we do not draw $\bot$ and the corresponding edges in Fig. 4 and Fig. 5 as ${\mathcal{O}}_{\textsf{win}}$ will always prefer to tell the controller ${\mathord{\scalerel*{\bigcirc}{\square}}}$ to give up instead of playing to $\bot$ (analogously for ${\mathbin{\square}}$ and $\top$). More importantly, if a strategy tells a player to give up at a specific node this means that the player loses any play reaching this specific node. For this reason, the computed strategy $\sigma$ is not winning for the controller so far, hence, we also ask ${\mathcal{O}}_{\textsf{win}}$ if the environment ${\mathbin{\square}}$ might win the initial state – now with the boundary marked as winning for the controller. As ${\mathcal{O}}_{\textsf{win}}$ also fails to find a winning strategy for the environment (${\mathord{\scalerel*{\bigcirc}{\square}}}$ can easily force ${\mathbin{\square}}$ directly into the boundary), we proceed to further explore and construct the arena.

In this iteration ${\mathcal{O}}_{\textsf{expl}}$ now uses $\sigma$ and $\tau$: as neither the controller nor the environment wins the initial node so far, starting in $q_{0}=(a_{0},\underline{b_{0}},c_{0})$ each player can force his opponent into the boundary; hence, $\sigma$ and $\tau$ give us some information where to further explore the arena; further, from $\alpha$ we obtain scores that tell us how far from acceptance resp. rejection a given boundary state is w.r.t. to the product of the underlying automata; in our example, using $\alpha$ the oracle ${\mathcal{O}}_{\textsf{expl}}$ tells us to first explore only the two states $(a_{0},\underline{b_{1}},c_{0})$ and $(a_{0},b_{0},\underline{c_{0}})$ as in both cases only one of the two processes is waiting for being granted access. Proceeding as before, we further extend the parity game under construction leading to the parity game shown in Fig. 5 (which also shows the strategy obtained for ${\mathord{\scalerel*{\bigcirc}{\square}}}$) and again ask if either ${\mathord{\scalerel*{\bigcirc}{\square}}}$ or ${\mathbin{\square}}$ can now win the initial node $q_{0}$. As the extended parity game coincides with that of the previous iteration in all but the boundary nodes, we pass the so-far computed strategies also to ${\mathcal{O}}_{\textsf{win}}$ in order to re-use the information stored in them.

Fig. 5 shows the strategy that ${\mathcal{O}}_{\textsf{win}}$ now computes: the updated $\sigma$ coincides with the previous $\sigma$ on the nodes where ${\mathord{\scalerel*{\bigcirc}{\square}}}$ did not give up (edges coloured in dark green); it only adds the edges coloured in light blue. The so updated $\sigma$ now wins the initial node for the controller. In particular, $\sigma$ keeps the nondeterminism at $(q_{0},r_{1}\,r_{2})$ where it only tells the controller to grant access to exactly one process but it does not tell ${\mathord{\scalerel*{\bigcirc}{\square}}}$ which one of the processes should be preferred. This ambiguity can be used when translating the strategy into a circuit or a program to reduce the description size. Finally note that as we mark the nodes on the boundary as losing for the respective ‘main’ player when calling ${\mathcal{O}}_{\textsf{win}}$, if the ‘main’ player can win the so-far constructed parity game, then his strategy has to avoid the boundary, i.e. by construction we always find winning strategies that try to enclose all plays starting in the initial node in a ‘minimal’ winning region. We remark that this bears some similarity to the local strategy iteration schemes by Friedmann DBLP:journals/ijfcs/FriedmannL12 ; but there the parity game is assumed to be explicitly given, and the goal is simply to speed-up strategy iteration itself; in our case the goal is to construct as little as possible from the actual parity game, while the actual choice of the oracle ${\mathcal{O}}_{\textsf{win}}$ is unimportant at this point.

This brings us to the end of our walk-through of the main algorithm. In the following sections we describe in more detail how we choose to instantiate the oracles.

3.1 DPA Construction

3.1.1 Formula Analysis and Decomposition

Before constructing a DPA the formula is analysed and its syntax-tree is annotated with automata acceptance conditions based on syntactic criteria. Such a formula decomposition focussed on conjunctions has been previously used in other work such as DBLP:journals/corr/abs-1006-1408 ; DBLP:journals/fmsd/FiliotJR11 ; DBLP:journals/fmsd/Ehlers12 . However, we will also consider disjunctions and bi-implications. In Section 2.1 we introduced the following three sub-classes of DPAs: DWAs, DBAs, and DCAs. Accordingly we annotate the LTL formula with ‘acceptance-typing’ information:

Definition 3 (Acceptance-Type Annotated LTL)

[TABLE]

We obtain an acceptance-typed LTL formula $\alpha$ from an LTL formula $\varphi$ using the following heuristic approach: First, we determine syntactically the ‘simplest’ acceptance type, denoted $\tau_{\varphi}$, such that we can build a deterministic automaton with acceptance $\tau_{\varphi}$ for $\varphi$ efficiently. Second, we annotate $\varphi$ with this information and obtain $\alpha$ as the result of $\mathcal{T}_{\varphi}$. Formally:

Definition 4

Let $\varphi$ be a formula. Then $\tau$ is recursively defined as:

[TABLE]

where $\sqcup$ denotes the least upper bound relative to the partial order $\preceq$ defined by $\mathcal{W}\prec\mathcal{B}$, $\mathcal{W}\prec\mathcal{C}$, $\mathcal{B}\prec\mathcal{P}$, $\mathcal{C}\prec\mathcal{P}$, $\mathcal{B}\not\preceq\mathcal{C}$ and $\mathcal{C}\not\preceq\mathcal{B}$. The acceptance-type annotated formula $\mathcal{T}_{\varphi}$ is then recursively defined as:

[TABLE]

In a specific implementation this decomposition and annotation might be fine-tuned to allow better translation performance, e.g. safety properties classified as separate weak sub-formulas might be grouped for performance reasons.

Further, let $\mathcal{X}$, $\mathcal{Y}$, and $\mathcal{Z}$ be acceptance-typed LTL formulas. We make use of the following simple pattern matching notation:

• •

$\mathcal{X}=\mathcal{B}_{\land}(\mathcal{X}_{1},\mathcal{X}_{2})$: Here $\mathcal{X}_{1}$ and $\mathcal{X}_{2}$ are fresh variables binding to the left and right subtree of $\mathcal{X}$, which is constrained to be a conjunction typed as Büchi acceptance.

• •

$\mathcal{Y}=\mathcal{Y}_{\lor}(\mathcal{C}_{1},\mathcal{Y}_{2})$: Here $\mathcal{C}_{1}$ and $\mathcal{Y}_{2}$ are fresh variables binding to the left and right subtree of $\mathcal{Y}$. Further, $\mathcal{C}_{1}$ has to be typed as co-Büchi acceptance and $\mathcal{Y}$ can be typed with any acceptance condition, but needs to be a disjunction.

• •

$\mathcal{Z}=\mathcal{W}_{\leftrightarrow}(\mathcal{W}_{1},\mathcal{W}_{2})$: Here $\mathcal{W}_{1}$ and $\mathcal{W}_{2}$ are fresh variables binding to the left and right subtree of $\mathcal{Z}$ and are both typed with weak acceptance. Moreover, $\mathcal{Z}$ is a bi-implication with weak acceptance.

Moreover, instead of only binary conjunctives, we use Büchi conjunction and co-Büchi disjunction of sets, i.e. we add

[TABLE]

for any $n\geq 2$ to the syntax. We restrict this rule to applications where all children are in the Büchi class for $\mathcal{B}_{\land}$ (resp. co-Büchi class for $\mathcal{C}_{\lor}$). After computing $\mathcal{T}_{\varphi}$, successive conjunctions are directly grouped together with the rule $\mathcal{B}_{\land}(\mathcal{B}_{\land}(\mathcal{B}_{1},\mathcal{B}_{2}),\mathcal{B}_{3})=\mathcal{B}_{\land}(\mathcal{B}_{1},\mathcal{B}_{\land}(\mathcal{B}_{2},\mathcal{B}_{3}))=\mathcal{B}_{\land}(\mathcal{B}_{1},\mathcal{B}_{2},\mathcal{B}_{3})$, and the respective rule for $\mathcal{C}_{\lor}$.

3.1.2 Product Construction with LAR

Given an acceptance-type annotated syntax tree $\mathcal{T}_{\varphi}$ for a formula $\varphi$, we now describe a recursive procedure to construct a (transition-based) DPA ${A}(\mathcal{T}_{\varphi})$ with $\mathcal{L}({A}(\mathcal{T}_{\varphi}))=\mathcal{L}(\varphi)$. Observe that not all patterns that are syntactically possible are covered, but all patterns generated by $\mathcal{T}_{\varphi}$.

Base Case.

In the case $\mathcal{T}_{\varphi}\in\{\mathcal{W}(\varphi),\mathcal{B}(\varphi),\mathcal{C}(\varphi),\mathcal{P}(\varphi)\}$ we use one of the direct automata constructions described in Section 2.3.

Conjunction.

Now consider the case for the conjunction $\mathcal{T}_{\varphi}=\mathcal{X}_{\land}(\mathcal{T}_{\psi_{1}},\mathcal{T}_{\psi_{2}})$, or $\mathcal{T}_{\varphi}=\mathcal{B}_{\land}(\mathcal{T}_{\psi_{1}},\ldots,\mathcal{T}_{\psi_{n}})$. We start the construction by recursively constructing DPAs ${A}(\mathcal{T}_{\psi_{i}})=(Q_{i},\delta_{i},q^{0}_{i},\chi_{i},d_{i},p_{i})$ for each child $\mathcal{T}_{\psi_{i}}$. Then we apply a case distinction based on $\mathcal{T}_{\varphi}$ and each $\mathcal{T}_{\psi_{i}}$.

• •

In the cases where we have $\mathcal{X}_{\land}(\mathcal{W}_{1},\mathcal{X}_{2})$ (and symmetrically $\mathcal{X}_{\land}(\mathcal{X}_{1},\mathcal{W}_{2})$), we can use a simple product construction. Then define the DPA

[TABLE]

with:

[TABLE]

• •

In the cases where we have $\mathcal{X}_{\land}(\mathcal{C}_{1},\mathcal{X}_{2})$ (and symmetrically $\mathcal{X}_{\land}(\mathcal{X}_{1},\mathcal{C}_{2})$), we can also use a product construction, with possibly one extra colour. W.l.o.g. assume $p_{2}=1$. This can be achieved by switching the parity of $A(\mathcal{X}_{2})$ if necessary. Then define the DPA

[TABLE]

with:

[TABLE]

• •

Next, we consider the case $\mathcal{B}_{\land}(\mathcal{B}_{1},\ldots,\mathcal{B}_{n})$ with two or more Büchi children, and only Büchi children. Here, on top of a product construction, we need an additional round-robin-counter to track of successive satisfaction of the Büchi acceptance of the children. We define the DBA

[TABLE]

with $Q\coloneqq\left(Q_{1}\times\ldots\times Q_{n}\right)$, $q^{0}\coloneqq(q^{0}_{1},\ldots,q^{0}_{n})$ and

[TABLE]

where $r^{\prime}\coloneqq\max\{s\in\{r,r+1,\ldots,n\}\mid\forall r<j\leq s:\chi_{j}(q_{j},a)=0\}$.

• •

Last, we consider the case $\mathcal{P}_{\land}(\mathcal{B}_{1},\mathcal{P}_{2})$ (and symmetrically $\mathcal{P}_{\land}(\mathcal{P}_{1},\mathcal{B}_{2})$). W.l.o.g. we may assume $p_{2}=1$ by switching parity if necessary. Here, we need additional memory to remember the minimal colour of $\mathcal{P}_{2}$ between acceptances of $\mathcal{B}_{1}$. We define the DPA

[TABLE]

with $d\coloneqq\min\{d\in\{d_{2},d_{2}+1\}\mid d\equiv_{2}0\}$ and

[TABLE]

where $c^{\prime}\coloneqq\min\left(c,\chi_{2}(q_{2},a)\right)$.

Note that if some child in a conjunction reaches a non-accepting sink, then we also know that the conjunction can never accept again, and we can simplify the product state. A similar argument holds if all children reach a accepting sink. Formally, we replace $\delta$ by $\delta^{\prime}$ and $\chi$ by $\chi^{\prime}$ defined by:

[TABLE]

Disjunction.

The construction of the DPA ${A}(\mathcal{X}_{\lor}(\mathcal{X}_{1},\mathcal{X}_{2}))$ or ${A}(\mathcal{C}_{\lor}(\mathcal{C}_{1},\ldots,\mathcal{C}_{n}))$ for the disjunctive $\mathcal{X}_{\lor}$ is dual to the conjunction case.

Bi-implication.

Finally, we consider the bi-implication $\mathcal{X}_{\leftrightarrow}(\mathcal{X}_{1},\mathcal{X}_{2})$. This can be expressed through $\mathcal{X}_{\land}$ and $\mathcal{X}_{\lor}$ by the logical equivalence $\varphi\leftrightarrow\psi\equiv(\varphi\land\psi)\lor(\lnot\varphi\land\lnot\psi)$. However, this construction would increase the state space and number of colours in some cases, since four automata ($\varphi$, $\neg\varphi$, $\psi$, $\neg\psi$) instead of two ($\varphi$, $\psi$) need to be constructed. Therefore we have a special construction for the DPA ${A}(\mathcal{X}_{\leftrightarrow}(\mathcal{X}_{1},\mathcal{X}_{2}))$. As before, we start by constructing the DPAs for the children $\mathcal{X}_{1},\mathcal{X}_{2}$. Let ${A}(\mathcal{X}_{i})=(Q_{i},\delta_{i},q^{0}_{i},\chi_{i},d_{i},p_{i})$ for $i\in\{1,2\}$.

• •

In the case $\mathcal{W}_{\leftrightarrow}(\mathcal{W}_{1},\mathcal{W}_{2})$, we can apply a simple product construction. W.l.o.g. assume $p_{1}=p_{2}$ by switching parity if necessary. We define the DWA

[TABLE]

with:

[TABLE]

• •

Now we consider the general case for $\mathcal{P}_{\leftrightarrow}(\mathcal{X}_{1},\mathcal{X}_{2})$ (note that $\mathcal{B}_{\leftrightarrow}$ and $\mathcal{C}_{\leftrightarrow}$ never occur). W.l.o.g. assume that $\mathcal{X}_{1}\neq\mathcal{P}$ and thus $d_{1}=1$. We consider $\mathcal{X}_{2}$ to be of class $\mathcal{P}$ and need to store its minimal colour between acceptances of $\mathcal{X}_{1}$, as for conjunction. However, whenever $\mathcal{X}_{1}$ does not accept, we emit the colour of $A_{2}$, shifted by one. If $\mathcal{X}_{1}=\mathcal{W}$, we can actually omit the memory to store the colour of $\mathcal{X}_{2}$. We define the DPA

[TABLE]

with $d\coloneqq d_{2}+1$, $p\coloneqq\left(p_{1}+p_{2}\right)\bmod 2$ and

[TABLE]

where $c^{\prime}\coloneqq\min\left(c,\chi_{2}(q_{2},a)\right)$.

• •

We note that the construction of the previous case can be generalized to the product of two arbitrary DPAs by remembering for each colour $c$ of ${A}(\mathcal{X}_{1})$ the minimal colour of ${A}(\mathcal{X}_{2})$ between minimal occurrences of $c$ in ${A}(\mathcal{X}_{1})$.

As with conjunction, we apply the simplification to ${A}(\mathcal{X}_{\leftrightarrow}(\mathcal{X}_{1},\mathcal{X}_{2}))$, that if both children reach a state in $\{\bot,\top\}$, also the product state is either $\bot$ or $\top$. Replace $\delta$ by $\delta^{\prime}$ and $\chi$ by $\chi^{\prime}$ defined by:

[TABLE]

Let $\varphi$ be a formula and let $\alpha=\mathcal{T}_{\varphi}$ be the acceptance-type annotated formula. We then implement the oracles ${\mathcal{O}}_{p}$, ${\mathcal{O}}_{q_{0}}$, and ${\mathcal{O}}_{\delta}$ by the DPA ${A}(\alpha)=(Q,\delta,q^{0},\chi,d,p)$ in the following way: ${\mathcal{O}}_{p}(\alpha)\coloneqq p$, ${\mathcal{O}}_{q_{0}}(\alpha)\coloneqq q^{0}$, and ${\mathcal{O}}_{\delta}(\alpha,q)\coloneqq\{(\{i\},\{o\},\chi(q,i\cup o),\delta(q,i\cup o))\mid i\in\Sigma_{\textsf{in}},o\in\Sigma_{\textsf{out}}\}$.

3.1.3 Implementation Details

On-the-fly construction.

For this construction, the functions $\delta$ and $\chi$ only need to query the local state, and never need a global state. They might call the functions $\delta$ and $\chi$ for their children, but those also only depend on the local state and their respective children. Therefore it is possible to implement the construction of the DPA ${A}(\alpha)$ for a decomposition $\alpha$ on-the-fly: Starting with the initial state, successor states are only generated when necessary, and the DPA is not fully constructed until all states have been queried. This holds both for the root automaton and for any child automata constructed by the decomposition.

Memoization.

When querying the root DPA for successors, the successors of the same state in a child DPA may be needed several times. Instead of recomputing them each time, the successors of the state are cached or memoized for direct access.

Formula Isomorphism.

Building up on the memoization feature the construction only constructs one automaton for a pair of formulas isomorphic under renaming atomic propositions und remaps letters in the query stage, effectively reducing the automata states needed to be constructed for parametric formulas, where the same pattern is repeated with different atomic propositions.

Symbolic Construction and Representation of Transition Relations.

The description of the oracle interface only specifies that successor function represented by a set needs to be returned. An implementation can choose to represent such a transition relation explicitly (e.g. by a list of length $2^{n}$) or symbolically (e.g. by an MTBDD). In fact Strix 19.07 relies on a symbolic construction and representation of the transition relation of the arena and the automata. This then allows efficient (symbolic) grouping of inputs and outputs into equivalence classes by ${\mathcal{O}}_{\delta}$.

3.2 Parity Game Solver

We instantiate ${\mathcal{O}}_{\textsf{win}}$ with a variant of the strategy iteration algorithm in DBLP:journals/corr/abs-0806-2923 .

We first give a brief description of what strategy iteration is and why we deem it particularly useful when combined with a demand-driven construction of the arena. We then exemplify these ideas in a bit more detail using our preceding example from Sec. 3.

In brief, strategy iteration consists of improving the current strategy (resp. controller) by iterating the two steps: (i) compute the ‘worst case’ the environment can inflict on the system w.r.t. the current strategy; (ii) state-wise redefine the current strategy by selecting any successor(s) which lead to a better ‘worst case’. The iteration stops as soon as the strategy cannot be improved anymore i.e. if the currently selected successors led to the best ‘worst case’. Strategy iteration nicely combines with our approach of constructing the actual arena in a demand driven way: we only construct the arena to that extent that allows the controller to stay within the constructed subarena; all nodes resp. edges which are outside of this subarena are simply flagged to be lost to the controller, when checking for realisability, resp. the system, when checking for unrealisability; in addition, if we need to further explore the arena as we could neither prove realisability nor unrealisability using the subarena constructed so far, we can re-use the already computed strategies as initial strategies for computing the optimal strategies for the extended subarena.

We exemplify these ideas now. Let ${\mathcal{A}}=(V_{\mathord{\scalerel*{\bigcirc}{\square}}},V_{\mathbin{\square}},E,\chi,B)$ be a parity game arena with nodes $V=V_{\mathord{\scalerel*{\bigcirc}{\square}}}\cup V_{\mathbin{\square}}$ split between the two players ${\mathord{\scalerel*{\bigcirc}{\square}}}$ and ${\mathbin{\square}}$, edges $E$, edge colouring $\chi\colon E\to{\mathbb{N}}_{0}$, and boundary nodes $B\subseteq V$. We assume that ${\mathcal{A}}$ includes two special nodes $\bot$ and $\top$ where $\bot$ is always won by the environment ${\mathbin{\square}}$ and $\top$ is always won by the controller ${\mathord{\scalerel*{\bigcirc}{\square}}}$. We further require that all nodes in $V\setminus B$ have at least one successor w.r.t. $E$.666Actually, the edges are also labeled by corresponding inputs and outputs coming from the environment and the controller, respectively. To simplify notation, we forget about the inputs and outputs that also label the edges (as shown e.g. in Fig. 3) s.t. we can simply write $vE$ for the set of successors of the node $v$.

Besides ${\mathcal{A}}$, the parity game solver takes as additional input the ‘main player’ $\mathsf{P}\in\{{\mathord{\scalerel*{\bigcirc}{\square}}},{\mathbin{\square}}\}$, the parity $p\in\{0,1\}$ with which $\mathsf{P}$ wins a play, a node $q\in V$ of the arena whose winner we want to determine, and an initial strategy $\kappa$ for the main player $\mathsf{P}$. We will write $\overline{\mathsf{P}}$ for the opponent of $\mathsf{P}$ s.t. $\{\mathsf{P},\overline{\mathsf{P}}\}=\{{\mathord{\scalerel*{\bigcirc}{\square}}},{\mathbin{\square}}\}$ with the parity of the opponent $\overline{\mathsf{P}}$ being $\overline{p}$ accordingly. All nodes in $B$ are considered to be losing for the main player $P$, i.e. $\overline{\mathsf{P}}$ can win be forcing $\mathsf{P}$ into $B$.

In order to solve the parity game, we reformulate the winning condition into a sup-inf-distance problem: To this end, we first introduce an (implicit) auxiliary node $\bullet$ to which only the main player $\mathsf{P}$ can move to in order to give up. This node is in addition to the two nodes $\top$ and $\bot$ and only serves to simplify presentation. All edges leading to $\bullet$ are defined to be coloured by $\infty$ (‘don’t care’). We denote such a modification of an arena ${\mathcal{A}}$ by ${\mathcal{A}}^{\bullet}$.

We interpret the edge colours $\chi(v,w)$ as weights $\gamma(v,w)$ that measure how close $P$ comes to winning resp. losing when taking the corresponding edge. Let $C\subseteq{\mathbb{N}}_{0}$ be the set of all colours occurring in ${\mathcal{A}}$ except for $\infty$. (Recall that we used the colour ‘$\infty$’ for edges that are unimportant w.r.t. the winning condition.) A colour $c\in C$ is identified with the multiset $\{c\}$ which we represent by its characteristic function w.r.t. ${\mathbb{N}}_{0}^{C}$. The colour $\infty$ is identified with the empty multiset resp. its characteristic function. Addition on ${\mathbb{N}}_{0}^{C}$ is defined point-wise as usual s.t. it coincides with the union of multisets. The weight of a finite play is then simply the sum of the weights of the edges traversed by it, i.e. the multiset of the colours of the edges of a play.

We order ${\mathbb{N}}_{0}^{C}$ from the point of view of $\mathsf{P}$ by means of the following order relation $\prec_{\mathsf{P}}$: Given two distinct functions $g,g^{\prime}\in{\mathbb{N}}_{0}^{C}$, let $c:=\min\{c^{\prime}\in C\mid g(c^{\prime})\neq g^{\prime}(c^{\prime})\}$ be the least colour in which the two differ; if $c$ has parity $p$, we set $g\prec_{\mathsf{P}}g^{\prime}$ if and only if $g(c)<g^{\prime}(c)$; else if $c$ has parity $\overline{p}$, we set $g\prec_{\mathsf{P}}g^{\prime}$ if and only if $g(c)>g^{\prime}(c)$. For instance, taking a look at the arena of Fig. 3, the colours [math] and $1$ are mapped on the functions (represented as tuples) $(1,0)$ and $(0,1)$, respectively. From the perspective of the controller ${\mathord{\scalerel*{\bigcirc}{\square}}}$ and its winning parity [math], the weight $(1,0)$ (representing the colour [math]) is more attractive than the weight $(0,1)$ (representing the colour $1$), i.e. $(1,0)\prec_{\mathsf{P}}(0,1)$.

To make the interpretation of the functions in ${\mathbb{N}}_{0}^{C}$ as weights more intuitive, let us remark that one can recover the order $\prec_{\mathsf{P}}$ by reading the function $g\in{\mathbb{N}}_{0}^{C}$ as a numeral w.r.t. the alternating basis $-b$, i.e. $g$ is interpreted as the integer $\sum_{c\in C}g(c)\cdot(-1)^{p+c}\cdot b^{-c+\max C}$ where $b$ is any sufficiently large positive integer, e.g. $b=\left|{V}\right|$. This ensures that in every simple cycle in ${\mathcal{A}}$ we have that the cycle is won by $\mathsf{P}$ if and only if the total weight of the cycle is positive, i.e. staying forever in the cycle leads to gaining infinite distance. For instance in the arena of Fig. 6 we could choose $b=2$ s.t. $(1,0)$ is mapped onto $2$, while $(0,1)$ is mapped on $-1$.

$\mathsf{P}$’s goal thus becomes to maximise the distance to losing, i.e. the minimal total weight accumulated along a play – thus $P$ will only accept infinite plays if these yield an infinite distance to losing, otherwise $P$ will use the option to play to $\bullet$ (or into the boundary) in order to terminate a play and bound the distance to losing to a finite value.

Computation of the sup-inf-distances in ${\mathcal{A}}^{\bullet}$ is complicated by the existence of both positive and negative cycles (w.r.t. the interpretation of ${\mathbb{N}}_{0}^{C}$ as numerals). For this reason, we use strategy iteration, i.e. we construct a sequence of strategies for $\mathsf{P}$ where each strategy only allows for positive cycles, while negative cycles are prevented by playing to $\bullet$: Assume $\mathsf{P}$ uses a (nondeterministic memoryless) strategy $\kappa$ (i.e. $\emptyset\neq\kappa(v)\subseteq vE$ for all $v\in V_{P}$) s.t. in the accordingly restricted arena ${\mathcal{A}}^{\bullet}_{\kappa}$ (i.e. $\mathsf{P}$ may only move to a successor in $\kappa(v)$ at every node $v\in V_{\mathsf{P}}$) s.t. no negative cycles exist anymore (e.g. consider $\kappa=V_{P}\times\{\bullet\}$); then the sup-inf-distance for every node can be easily computed using fixed-point iteration just as in the case of the standard attractor computation using some variant of the Bellmann-Ford algorithm (in order to identify infinite positive sup-inf-distance). Let $d_{\kappa}(v)$ denote the sup-inf-distance of node $v$ in ${\mathcal{A}}^{\bullet}_{\kappa}$. For every node $v$ in $B\cup\{\bullet\}$, we define $d_{\kappa}(v)=0$; for the nodes $\bot$ and $\top$ we predefine $d_{\kappa}$ accordingly; for every $v$ controlled by $\overline{\mathsf{P}}$ we have the unrestricted optimality equation $d_{\kappa}(v)=\min^{\prec_{\mathsf{P}}}\{\gamma(v,w)+d_{\kappa}(w)\mid w\in vE\}$, while for $v$ controlled by $\mathsf{P}$ we have the $\kappa$-restricted optimality equation $d_{\kappa}(v)=\max^{\prec_{\mathsf{P}}}\{\gamma(v,w)+d_{\kappa}(w)\mid w\in\kappa(v)\}$ (with $\gamma(v,w)$ the weight induced by the colour of the edge from $v$ to $w$). We call any nondeterministic strategy $\kappa^{\prime}$ an improvement of $\kappa$ if (1) $\kappa^{\prime}\neq\kappa$, (2) $\emptyset\neq\kappa^{\prime}(v)\subseteq vE$ for all $v\in V_{P}$, (3) if $(v,w)\in\kappa^{\prime}\setminus\kappa$, then $d_{\kappa}(v)<\gamma(v,w)+d_{\kappa}(w)$ (i.e. $v$’s sup-inf-distance can be improved by playing to $w$), and (4) if $(v,w)\in\kappa^{\prime}\cap\kappa$, then $d_{\kappa}(v)=\gamma(v,w)+d_{\kappa}(w)$. DBLP:journals/corr/abs-0806-2923 shows that any such improvement $\kappa^{\prime}$ does not introduce any negative cycles and that $d_{\kappa^{\prime}}>d_{\kappa}$, i.e. the sup-inf-distances w.r.t. $\kappa^{\prime}$ do not decrease for any node and strictly improves for at least one node. Thus, no strategy can be encountered twice. Finally, note that if $W_{\mathsf{P}}\uplus W_{\overline{\mathsf{P}}}$ is the winning partition of the nodes $V$ of ${\mathcal{A}}$ w.r.t. the min-parity-condition, then $\mathsf{P}$ can use his (memoryless deterministic) winning strategy from the parity game to ensure infinite sup-inf-distance on $W_{\mathsf{P}}$ also in ${\mathcal{A}}^{\bullet}$, while $\overline{\mathsf{P}}$ can use his winning strategy from the parity game to ensure at least finite sup-inf-distance in ${\mathcal{A}}^{\bullet}$. Hence, eventually the strategy iteration will terminate in a strategy that guarantees infinite sup-inf-distance on exactly $W_{P}$.

In our implementation, we make use of the fact that the fixed-point iteration used for solving the optimality equations stated above can be easily parallelised in order to make use of modern multi-core CPUs (or even GPUs DBLP:conf/atva/MeyerL16 ).

3.2.1 Exploring the Boundary

${\mathcal{O}}_{\textsf{expl}}$ selects nodes from the boundary $B$ that should be further explored, i.e., where successors should be computed. After each expansion $B$ is recomputed such that it contains the nodes which successors have not yet been explored. We instantiate ${\mathcal{O}}_{\textsf{expl}}$ with two different approaches. One is based on breadth-first search exploration, and one on a priority queue ordering states in the boundary by some quality score. For each method, we then have an additional variant that filters the states that are currently needed to determine the winner of the arena. In total, this results in the following four methods.

• •

${\mathcal{O}}_{\textsf{expl}}^{\textsf{bfs}}$ (breadth-first search (BFS) exploration): In the initial implementation the algorithm explored and constructed the parity game using a breadth-first-search (BFS). This approach helps to ignore parts of the game that are far away from the initial state and not decisive for winning the game, however it also explores states that are close to the initial state, but are irrelevant with the currently computed strategy.

Conceptually, we use the exploration function that picks states from $B$ with a minimal distance from the initial state $q_{0}$ in each step. Define ${\mathcal{O}}_{\textsf{expl}}^{\textsf{bfs}}$ by:

[TABLE]

In the implementation, instead of recomputing the minimal distances in each step, we select the next state from the boundary from a worklist queue.

• •

${\mathcal{O}}_{\textsf{expl}}^{\textsf{bfs+}}$ (BFS exploration with strategy-based worklist filtering): This exploration strategy is a variant of ${\mathcal{O}}_{\textsf{expl}}^{\textsf{bfs}}$. The worklist is still populated in a BFS way, but we only keep states that we know are needed to determine if the initial state is winning or losing. These are states which are reachable through some path not blocked by an already winning or losing state. We define the exploration function ${\mathcal{O}}_{\textsf{expl}}^{\textsf{bfs+}}$ as follows:

[TABLE]

We reuse the results of ${\mathcal{O}}_{\textsf{win}}$ already computed in the main algorithm. However, in contrast to ${\mathcal{O}}_{\textsf{expl}}^{\textsf{bfs}}$, we need to check for existence of a path from $q_{0}$ to all states $b\in B$ without already won states, which we do using a single linear-time search in each iteration.

• •

${\mathcal{O}}_{\textsf{expl}}^{\textsf{pq}}$ (priority queue exploration based on scores): This exploration method is based on quality scores (to be defined in the next section) assigned to each state in the boundary. The idea is that a high score means this state is a promising state for ${\mathord{\scalerel*{\bigcirc}{\square}}}$ to win the game from the initial state, while a low score is a promising state for ${\mathbin{\square}}$ to win the game. As we initially do not know if the specification is realisable or unrealisable, and thus do not know for which player the initial state is winning, this method explores both states with high and low scores simultaneously. We assign scores not to states, but to edges, to incorporate information from colours and updates in the LAR. Let ${\mathcal{O}}_{\textsf{score}}(\alpha,q,a,q^{\prime})$ be a function assigning a score to a given edge $(q,a,q^{\prime})$ of the parity automaton ${A}(\alpha)$. With an intermediate function $s(b)$ assigning to a state $b\in B$ all scores of incoming edges, we define the exploration method ${\mathcal{O}}_{\textsf{expl}}^{\textsf{pq}}$ by:

[TABLE]

We implement this method with a double-ended priority queue, in which states are inserted with their respective minimal and maximal score of an incoming edge upon discovery.

• •

${\mathcal{O}}_{\textsf{expl}}^{\textsf{pq+}}$ (priority queue exploration with strategy-based worklist filtering): Finally, we can combine the exploration using scores with the filtering function filter from ${\mathcal{O}}_{\textsf{expl}}^{\textsf{bfs+}}$, yielding the method ${\mathcal{O}}_{\textsf{expl}}^{\textsf{pq+}}$ defined by:

[TABLE]

3.2.2 Quality Scores

We now describe how to compute scores by ${\mathcal{O}}_{\textsf{score}}(\mathcal{T}_{\varphi},q,a,q^{\prime})$ for an edge $(q,a,q^{\prime})$ of the DPA ${A}(\mathcal{T}_{\varphi})$ leading to a boundary state $q^{\prime}$. We first define a function score, which takes the acceptance-type annotated formula $\mathcal{T}_{\varphi}$ and an edge $(q,a,q^{\prime})$ of ${A}(\mathcal{T}_{\varphi})$, and returns a weighted score $(w,s)=\textsf{score}(\mathcal{T}_{\varphi},q,a,q^{\prime})$. We always assign the score value $s$ such that $s=0$ if $q^{\prime}=\bot$, $s=1$ if $q^{\prime}=\top$ and $0<s<1$ otherwise. The function $\textsf{score}(\mathcal{T}_{\varphi},q,a,q^{\prime})$ computes $(w,s)$ recursively on $\mathcal{T}_{\varphi}$, similarly to the LAR-product construction, and we define it by case distinction on $\mathcal{T}_{\varphi}$ and $q$.

• •

If $q=\bot$, return $w=1$ and $s=0$.

• •

If $q=\top$, return $w=1$ and $s=1$.

• •

In the base case for $\mathcal{W}(\varphi),\mathcal{B}(\varphi),\mathcal{C}(\varphi)$ and $\mathcal{P}(\varphi)$, return $w=1$ and compute $s$ depending on the type of automaton.

• –

If we encounter $\mathcal{W}(\varphi)$, then $\varphi\in\mu{LTL}\cup\nu{LTL}$. By using the construction of DBLP:conf/lics/EsparzaKS18 the state $q^{\prime}$ is in fact a Boolean formula over modal operators treated as variables. Let $\mathcal{V}$ be the set of variables and let $\mathcal{M}$ be the set of satisfying assignments of $q^{\prime}$. We then set $s=|\mathcal{M}|/2^{|\mathcal{V}|}$. Using this definition, we assign to the state ${\mathbf{tt}}$ (which corresponds to $\top$) $s=1$ and to the state ${\mathbf{ff}}$ (which corresponds to $\bot$) $s=0$.

• –

If we encounter $\mathcal{B}(\varphi)$, then we apply the construction of DBLP:conf/cav/SickertEJK16 and the state $q^{\prime}=(p,p^{\prime})$ is a tuple of two Boolean formulas $p$ and $p^{\prime}$. We then construct $p\wedge p^{\prime}$ and compute the scoring for $\mathcal{W}(p\wedge p^{\prime})$.

• –

If we encounter $\mathcal{C}(\varphi)$, then we apply the same approach as in $B(\varphi)$, since these automata are obtained by complementing Büchi automata and have an identical structure besides the acceptance condition.

• –

If we encounter $\mathcal{P}(\varphi)$, we bail and return $s=\frac{1}{2}$.

• •

In the case $\mathcal{T}_{\varphi}=\mathcal{X}_{\land}(\mathcal{X}_{1},\ldots,\mathcal{X}_{n})$ and $\mathcal{T}_{\varphi}=\mathcal{X}_{\lor}(\mathcal{X}_{1},\ldots,\mathcal{X}_{n})$, we first compute the child scores $(w_{i},s_{i})=\textsf{score}(\mathcal{X}_{i},q,a,q^{\prime})$. Then, for each $\mathcal{X}_{i}$, we update $w_{i}$ and $s_{i}$ as follows:

• –

If $\mathcal{T}_{\varphi}=\mathcal{X}_{\land}$, set $w_{i}\leftarrow w_{i}\cdot\log_{\nicefrac{{1}}{{2}}}s_{i}$. This gives score values close to [math] an increased weight, which could make the whole conjunction false.

• –

If $\mathcal{T}_{\varphi}=\mathcal{X}_{\lor}$, set $w_{i}\leftarrow w_{i}\cdot\log_{\nicefrac{{1}}{{2}}}(1-s_{i})$. This gives score values close to $1$ an increased weight, which could make the whole disjunction true.

• –

If $\mathcal{T}_{\varphi}=\mathcal{B}_{\land}(\mathcal{B}_{1},\ldots,\mathcal{B}_{n})$, or $\mathcal{T}_{\varphi}=\mathcal{C}_{\lor}(\mathcal{C}_{1},\ldots,\mathcal{C}_{n})$, then $\mathcal{X}_{i}=\mathcal{B}$ or $\mathcal{X}_{i}=\mathcal{C}$ and $q=(q^{\prime\prime},r)$ and $q^{\prime}=(q^{\prime\prime\prime},r^{\prime})$ for some round-robin counters $r,r^{\prime}$. Now if the child caused the round-robin counter to increase, i.e. we have $r\leq i<r^{\prime}$, then we set $w_{i}\leftarrow 2\cdot w_{i}$ and update the score. If $\mathcal{X}_{i}=\mathcal{B}$, set $s_{i}\leftarrow\frac{3+s_{i}}{4}$ to increase the score, and if $\mathcal{X}_{i}=\mathcal{C}$, set $s_{i}\leftarrow\frac{s_{i}}{4}$ to decrease the score.

• –

If either $\mathcal{T}_{\varphi}=\mathcal{P}_{\land}(\mathcal{X}_{1},\mathcal{X}_{2})$, $\mathcal{X}_{i}=\mathcal{P}$, and $\mathcal{X}_{3-i}=\mathcal{B}$, or $\mathcal{T}_{\varphi}=\mathcal{P}_{\lor}(\mathcal{X}_{1},\mathcal{X}_{2})$, $\mathcal{X}_{i}=\mathcal{P}$, and $\mathcal{X}_{3-i}=\mathcal{C}$, then $q=(q^{\prime\prime},c)$ and $q^{\prime}=(q^{\prime\prime\prime},c^{\prime})$ for some minimal colour memory values $c,c^{\prime}$. Let $p$ be the parity of the DPA ${A}(\mathcal{T}_{\varphi})$. Now if ${A}(\mathcal{X}_{i})$ caused the memory to decrease to a value with parity $p$, we increase the score, and if it decreased it to a value with different parity, we decrease the score. Therefore if $c^{\prime}<c$ and $c^{\prime}\equiv_{2}p$, then set $w_{i}\leftarrow 2\cdot w_{i}$ and $s_{i}\leftarrow\frac{3+s_{i}}{4}$, and if $c^{\prime}<c$ and $c^{\prime}\equiv_{2}\overline{p}$, then set $w_{i}\leftarrow 2\cdot w_{i}$ and $s_{i}\leftarrow\frac{s_{i}}{4}$.

Finally, we return $w\coloneqq\sum_{i=1}^{n}w_{i}$ and $s\coloneqq\left(\sum_{i=1}^{n}w_{i}\cdot s_{i}\right)\mathbin{/}w$.

• •

In the case $\mathcal{X}_{\leftrightarrow}(\mathcal{X}_{1},\mathcal{X}_{2})$, we also first compute the child scores $(w_{i},s_{i})=\textsf{score}(\mathcal{X}_{i},q,a,q^{\prime})$ for $i\in\{1,2\}$, and then update each $w_{i}$ and $s_{i}$ similarly to conjunction and disjunction:

• –

If $0<s_{i}<1$, set $w_{i}\leftarrow w_{i}\cdot\max(\log_{\nicefrac{{1}}{{2}}}s_{i},\log_{\nicefrac{{1}}{{2}}}(1-s_{i}))$.

• –

If $\mathcal{T}_{\varphi}=\mathcal{P}_{\leftrightarrow}(\mathcal{X}_{1},\mathcal{X}_{2})$ and ${A}(\mathcal{X}_{i})$ is the child for which we store the colours in memory, then $q=(q^{\prime\prime},c)$ and $q^{\prime}=(q^{\prime\prime\prime},c^{\prime})$ for some minimal colour memory values $c,c^{\prime}$ of ${A}(\mathcal{X}_{i})$. Let $p$ be the parity of the DPA ${A}(\mathcal{T}_{\varphi})$. As for $\mathcal{P}_{\land}$ and $\mathcal{P}_{\lor}$, if $c^{\prime}<c$ and $c^{\prime}\equiv_{2}p$, then set $w_{i}\leftarrow 2\cdot w_{i}$ and $s_{i}\leftarrow\frac{3+s_{i}}{4}$, and if $c^{\prime}<c$ and $c^{\prime}\equiv_{2}\overline{p}$, then set $w_{i}\leftarrow 2\cdot w_{i}$ and $s_{i}\leftarrow\frac{s_{i}}{4}$.

Then we return $w\coloneqq\sum_{i=1}^{n}w_{i}$ and $s\coloneqq\left(\sum_{i=1}^{n}w_{i}\cdot s_{i}\right)\mathbin{/}w$.

We then define ${\mathcal{O}}_{\textsf{score}}(\mathcal{T}_{\varphi},q,a,q^{\prime})\coloneqq s$ where $(w,s)=\textsf{score}(\mathcal{T}_{\varphi},q,a,q^{\prime})$. The value $w$ is only necessary to normalise intermediate scores due to the recursive definition of score.

3.3 Controller Extraction

3.3.1 Mealy machine

When we determine that ${\mathord{\scalerel*{\bigcirc}{\square}}}$ has a winning strategy $\sigma$ from $q_{0}$, we can extract a controller from $\sigma$ that ensures realisation of the specification.

We use an incompletely specified Mealy machine, where some outputs might not be specified and could be instantiated either way. This allows further minimisation and more compact representations by a circuit. Given an input/output partition $\mathsf{Ap}={\mathsf{Ap}_{\textsf{in}}}\uplus{\mathsf{Ap}_{\textsf{out}}}$, a Mealy machine is a tuple $M=(Q,q_{0},\delta,\lambda)$ where $Q$ is a finite set of states, $q_{0}\in Q$ is the initial state, $\delta:Q\times 2^{\mathsf{Ap}_{\textsf{in}}}\to Q$ is the transition function and $\lambda:Q\times 2^{\mathsf{Ap}_{\textsf{out}}}\to\{0,1,\symunknown\}^{\mathsf{Ap}_{\textsf{out}}}$ is the output function, where $\symunknown$ stands for an unspecified output. The output can be given by a Boolean product term, where missing variables are unspecified.

Let $(V_{\mathord{\scalerel*{\bigcirc}{\square}}},V_{\mathbin{\square}},E)$ be the parity game arena where ${\mathord{\scalerel*{\bigcirc}{\square}}}$ wins from $q_{0}$ with the strategy $\sigma$. We use $Q\coloneqq\{q\in V_{\mathbin{\square}}\mid{\mathcal{O}}_{\textsf{win}}(V_{\mathord{\scalerel*{\bigcirc}{\square}}},V_{\mathbin{\square}},E,\chi,B,q,{\mathord{\scalerel*{\bigcirc}{\square}}},p,\sigma)\}$ as the set of states. For the transition function, we define $\delta(q,i)\coloneqq q^{\prime}$ by choosing some $q^{\prime}$ where $((q,I),O,q^{\prime})\in\sigma$ for some $I\subseteq\Sigma_{\textsf{in}}$ with $i\in I$ and any $O\subseteq\Sigma_{\textsf{out}}$. By construction, and as $\sigma$ is a winning strategy for all $q\in Q$, such a $q^{\prime}$ always exists. However, there may be multiple applicable $q^{\prime}$. We construct $Q$ and $\delta$ iteratively, starting from $Q\leftarrow\{q_{0}\}$, and try to choose for every $q\in Q$ and $i\in 2^{\mathsf{Ap}_{\textsf{in}}}$ a $q^{\prime}=\delta(q,i)$ such that $q^{\prime}\in Q$, if possible, and otherwise extend $Q\leftarrow Q\cup\{q^{\prime}\}$. As a secondary heuristic, we try to choose a successor that gives the most flexibility in choosing the output, i.e. a $q^{\prime}$ such that $\sum\{|O|\mid\exists I:i\in I\land((q,I),O,q^{\prime})\in\sigma\}$ is maximal.

For the output function, let $\delta(q,i)=q^{\prime}$ be an edge of the Mealy machine; then take a minimal prime implicant $o^{\prime}$ of the Boolean formula over ${\mathsf{Ap}_{\textsf{out}}}$ that encodes the set $\{o\mid\exists I,O:i\in I\land o\in O\land(q,I),O,q^{\prime})\in\sigma\}$, and define $\lambda(q,i)\coloneqq o^{\prime}$. This again exploits non-determinism of the strategy $\sigma$.

Example 1

Using the winning strategy for the simple arbiter specification in Fig. 5, we obtain $Q=\{(a_{0},\underline{b_{0}},c_{0}),(a_{0},\underline{b_{1}},c_{0}),(a_{0},b_{0},\underline{c_{1}})\}$ as states of the Mealy machine. For $\delta((a_{0},\underline{b_{0}},c_{0}),r_{1}r_{2})$, we may choose any of the other two states as a successor. If we choose $(a_{0},\underline{b_{1}},c_{0})$, we get the output $o=\lambda((a_{0},\underline{b_{0}},c_{0}),r_{1}r_{2})=\overline{g_{1}}g_{2}$, specifying $o(g_{1})=0$ and $o(g_{2})=1$. For the output $\lambda((a_{0},\underline{b_{0}},c_{0}),\overline{r_{1}}\,\overline{r_{2}})$, we may choose one of the two min-terms $\overline{g_{1}}$ or $\overline{g_{2}}$ as an output. If we choose $o=\overline{g_{1}}$, then $o(g_{1})=0$, but the output $o(g_{2})=\symunknown$ is unspecified. An implementation is then free to choose $o(g_{2})=0$ or $o(g_{2})=1$.

This incompletely specified Mealy machine can optionally be minimised. We use the exact minimisation algorithm from DBLP:conf/iccad/0002R15 , which in turn uses a SAT solver. While this problem is harder than minimisation of fully specified Mealy machines, it can also result in smaller machines.

3.3.2 Controller as BDD or AIG

While we can directly output the controller as a Mealy machine, we can also encode it as a binary decision diagram (BDD) or and-inverter graph (AIG), representing a circuit. For this, we need to encode the transition function $\delta$ and output function $\lambda$ of the Mealy machine as a BDD or AIG. Both of these representations use decisions over binary variables. The inputs $i\in 2^{\mathsf{Ap}_{\textsf{in}}}$ and outputs $o\in\{0,1,\symunknown\}^{\mathsf{Ap}_{\textsf{out}}}$ are already binary vectors after one resolves the unspecified $\symunknown$ outputs. However, one needs to choose a binary encoding of the state space $Q$. Here we offer two options:

First, we can use an unstructured encoding $l_{\textsf{unstr}}$. We simply enumerate the states $Q=\{q_{0},\ldots,q_{n}\}$ and use the encoding function $l_{\textsf{unstr}}:Q\to 2^{\lceil\log_{2}|Q|\rceil}$ with $l_{\textsf{unstr}}(q_{i})=i$ which maps each state to the binary encoding of its number.

Second, we can use the shape of the states for a structured encoding $l_{\textsf{struct}}$. As a state $q$ is a vector $(q_{1},\ldots,q_{n})$, we can encode each component separately into a binary vector. Assume that for each component $1\leq i\leq n$, the states $q_{i}$ are numbered from [math] to $|Q_{i}|-1$. Then we use the encoding function $l_{\textsf{struct}}:Q\to 2^{\sum_{i=1}^{n}\lceil\log_{2}|Q_{i}|\rceil}$, with

[TABLE]

which concatenates the binary encoding of the state number in each component. Note that this also includes additional memory information such as the round-robin counter or minimal colour memory.

Example 2

For the Mealy machine obtained from the strategy in Fig. 5, we have as states $Q=\{(a_{0},\underline{b_{0}},c_{0}),(a_{0},\underline{b_{1}},c_{0}),(a_{0},b_{0},\underline{c_{1}})\}$. With the unstructured encoding for $Q=\{q_{0},q_{1},q_{2}\}$, we get the binary state encodings $l_{\textsf{unstr}}(Q)=\{00_{2},01_{2},10_{2}\}$. If we represent the product states as numbers with $q_{i}=i$ for $q\in\{a,b,c\}$ and the round-robin counter by $r\in\{0,1\}$, then after applying the structured encoding function, we get the state encodings $l_{\textsf{struct}}(Q)=\{0000_{2},0100_{2},0011_{2}\}$.

We also minimise the controller for these output formats. When constructing a BDD, we minimise it using the CUDD library CUDD by reordering the variables. When constructing an AIG, we first construct a BDD and minimise it, and then construct the AIG from the BDD. Afterwards, we minimise the AIG using functionality from the ABC library DBLP:conf/cav/BraytonM10 .

When using the encoding function, it can sometimes also be more effective to not minimise the Mealy machine before, as this can destroy the structure from the product state. Structured encoding can also sometimes increase the size of a circuit. We offer an option to construct a circuit using the three following combinations in parallel and then return the smallest circuit: Mealy minimisation and unstructured encoding, no minimisation and structured encoding, and no minimisation and unstructured encoding.

4 Experimental Evaluation

The three main research questions we want to answer in this section are:

• •

RQ1: How does Strix compare to existing tools? Specifically, we analyse:

• –

Number of instances correctly identified to be realisable.

• –

Number of instances for which a correct controller was synthesised.

• –

Circuit size of the constructed controller.

• –

Performance with increasing alphabet size.

• •

RQ2: What is the difference in performance of the proposed exploration strategies (bfs and pq, with and without filtering)? Specifically, we analyse:

• –

Number of constructed states.

• –

Runtime.

• •

RQ3: What is the difference in size of the proposed circuit encoding strategies (structured and unstructured, with and without minimisation)? Specifically, we analyse:

• –

Circuit size.

Experimental Design.

We approach all three research questions by evaluating the different tools and configurations on the specifications from the TLFS/LTL-track of the Syntcomp2019 competition777http://www.syntcomp.org/, which subsumes all benchmarks of Syntcomp2018 DBLP:journals/corr/abs-1904-07736 . To the best of our knowledge this dataset is the most complete set of LTL specifications for synthesis stemming from a wide range of different applications. These include industrial examples such as the AMBA AHB arbiter Jobstmann07 ; DBLP:journals/sttt/GodhalCH13 ; DBLP:journals/corr/BloemJK14a , and case studies for hardware controller synthesis DBLP:conf/haskell/Finkbeiner0PS19 ; XXXX:conf/fmcad/G19 . For more details, see previous Syntcomp competition reports DBLP:journals/corr/JacobsBBK0KKLNP16 ; DBLP:journals/corr/abs-1711-11439 ; DBLP:journals/corr/abs-1904-07736 . The Syntcomp2019 set of specifications contains in total 434 LTL synthesis specifications, of which 337 are realisable and 97 are unrealisable. All experiments were run on a server with an Intel E5-2630 v4 clocked at 2.2 GHz (boost disabled, 40 cores). We imposed a memory limit of 100 GB (as in Syntcomp2019) and a wall-clock time limit of one hour for each specification.

In Section 4.1 we address RQ1 and evaluate overall performance on the benchmark set and compare against ltlsynt, BoSy and a previous version of Strix. In Section 4.2 (RQ2), we compare the different exploration strategies, and in Section 4.3 (RQ3) different construction approaches for the circuit.

Independent Evaluations.

Since the first release of Strix DBLP:conf/cav/MeyerSL18 independent researchers used, evaluated, and compared it to other tools. At Syntcomp2019, Strix in its submitted version (19.07) again made first place in all categories in the LTL synthesis track. In two case studies DBLP:conf/haskell/Finkbeiner0PS19 ; XXXX:conf/fmcad/G19 by Finkbeiner et al. Strix was used to synthesise controllers for small hardware devices; in the second case study XXXX:conf/fmcad/G19 , Strix was also compared to BoSy and the not publicly available BoWSer where Strix was the only tool to solve all synthesis problems, and also performed best w.r.t. time and size of the obtained controller in almost all of the synthesis problems; interestingly, BoWSer clearly outperformed Strix in the specification SensorSelector where BoWSer was roughly seven times faster than Strix and also succeeds in finding a trivial controller with zero gates within 38 seconds while Strix needed 280 seconds for returning a controller using 17 gates.

Finally, DBLP:conf/atva/EhlersA19 compares Strix to GuiSynth, a tool for synthesising code for graphical user interfaces. Here, GuiSynth clearly outperforms Strix in most benchmarks. As Ehlers and Adabala already noted this probably has to be contributed to the fact that GuiSynth is specifically designed for the task at hand and the embedding into a standard LTL synthesis problem causes an exponential blow-up in the alphabet size.

4.1 RQ1: Comparison with previous version, with ltlsynt, and with BoSy

Experimental Design.

We run Strix using the default exploration strategy ${\mathcal{O}}_{\textsf{expl}}^{\textsf{bfs}}$, AIG output and portfolio minimisation to find the smallest AIG. We compare against Strix in the version submitted to CAV 2018 DBLP:conf/cav/MeyerSL18 in April 2018. This version also used the exploration strategy ${\mathcal{O}}_{\textsf{expl}}^{\textsf{bfs}}$, but did not have many of the improvements such as formula isomorphism detection, memoization, symbolic representation of edges, or structured encoding. Further, we compare our implementation with BoSy and ltlsynt which achieved second888Strix was ranked on the first place. and third place in Syntcomp2018 in the ‘synthesis quantity’-ranking. We use ltlsynt from the Spot library DBLP:conf/atva/Duret-LutzLFMRX16 ; DBLP:journals/corr/abs-1711-11439 in the version 2.8.1 from July 2019, with parameter --algo=ds, and against BoSy DBLP:conf/cav/FaymonvilleFT17 in the newest version available as of July 2019, with parameter --optimize.

We run each tool on each specification twice: once to check only realisability and in the realisable case once more to synthesise a controller in the AIGER format. Table 1 gives the overall results.

The category Realisability counts the number of specifications for which realisability is correctly decided within the time limit, and the category Synthesis counts the number of realisable specifications for which additionally a successfully verified controller is produced. For this we verified the circuits with an additional time limit of one hour using the nuXmv model checker DBLP:conf/cav/CavadaCDGMMMRT14 in version 1.1.1 with the check_ltlspec_klive routine.

The Quality rating compares the size of the solutions according to the Syntcomp2019 formula, where a tool gets $\max(0,2-\log_{10}\frac{n+1}{r+1})$ quality points for each verified solution of size $n$ for a specification with reference size $r$. The size of a solution is given by the number of and gates plus number of latches, and as reference size we chose the smallest size of a verified solution produced by any of the four tools during our experiments.

Further, we list notable outliers in pairwise comparisons with other approaches. We compute for each pair of tools and each specification successfully solved by both tools the difference in order of magnitudes ($|\log_{10}\frac{x}{y}|$)999…or $|\log_{10}\frac{x+1}{y+1}|$ to compensate for circuits of size 0. and select for each pair of tools the eight largest differences.

In order to study the impact of growing alphabet sizes we look at 4 parametrised benchmarks from Syntcomp2019 and measure the execution time for growing parameters. These parameters scale up the number of components and the size of the alphabet. Namely, we pick arbiter (AMBA), full_arbiter_enc, ltl2dba_Q, and ltl2dba_beta.

The results for these comparisons are given in table Table 2 for time to decide realisability, in Table 3 for size of the solutions, and Table 4 gives a cross-comparison.

Analysis.

Compared to the previous version of Strix we solve at least 40 additional specifications in the Realisability and Synthesis categories and see a considerable improvement in the Quality ratings. We believe that this is partly due to the symbolic construction and representation of the transition relation which applies to the arena and the automata for LTL fragments, e.g. safety. Only on smaller instances of the full_arbiter specification the previous version is faster. This might be related to the overhead of using symbolic data-structures for small alphabets. Further, the revised AIG encoding strategy yields smaller controllers in comparison to the previous version.

Compared to BoSy, our approach can scale better on larger and complex specifications. One can observe this on parameterised specifications that mainly increase the number of input propositions. Even though BoSy employs an input-symbolic QBF encoding it could not deal with the large specifications. We hypothesise that this is caused by an explicit representation somewhere in the synthesis chain. For synthesis, while BoSy produces a smaller solution in 101 cases, Strix produces a smaller solution in 129 cases, and often by a much larger factor. We believe this is due to our structured encoding, which is hard to recover from a solution given by the constraint solver that bounded synthesis employs.

4.2 RQ2: Comparison of different exploration strategies

Experimental Design.

We compare the four different exploration strategies ${\mathcal{O}}_{\textsf{expl}}^{\textsf{bfs}}$, ${\mathcal{O}}_{\textsf{expl}}^{\textsf{bfs+}}$, ${\mathcal{O}}_{\textsf{expl}}^{\textsf{pq}}$ and ${\mathcal{O}}_{\textsf{expl}}^{\textsf{pq+}}$ and measure the number of explored states and time needed to check realisability. Table 5 gives a cross-comparison in order to identify a dominant approach. Further, Table 6 lists runtimes and number of explored states where there is a significant difference in the number of explored states.

Analysis.

Table 5 suggests that ${\mathcal{O}}_{\textsf{expl}}^{\textsf{pq+}}$ can avoid the exploration of states not relevant for deciding realisability. However, this efficiency seems to be costly, since in the runtime comparison it falls behind the ${\mathcal{O}}_{\textsf{expl}}^{\textsf{bfs+}}$ configuration.

We see that filtering the queue in ${\mathcal{O}}_{\textsf{expl}}^{\textsf{bfs+}}$ and ${\mathcal{O}}_{\textsf{expl}}^{\textsf{pq+}}$ in comparison to ${\mathcal{O}}_{\textsf{expl}}^{\textsf{bfs}}$ and ${\mathcal{O}}_{\textsf{expl}}^{\textsf{pq}}$, respectively, often reduces the amount of explored states. However, filtering the queue generally incurs overhead, as the reachable state space needs to be explored and the queue rebuilt. For instance, on amba_case_study_2, we half the number of states explored when filtering is used. Further, comparing ${\mathcal{O}}_{\textsf{expl}}^{\textsf{pq}}$ with ${\mathcal{O}}_{\textsf{expl}}^{\textsf{bfs}}$, we see that using the scoring-based exploration can significantly reduce the amount of explored states. This especially seems to hold for unrealisable specifications. We assume this is because the environment player only needs to find a path to a state that forces the controller player to violate the specification, while the remaining states only contribute to satisfying the specification. However, ${\mathcal{O}}_{\textsf{expl}}^{\textsf{pq}}$ and ${\mathcal{O}}_{\textsf{expl}}^{\textsf{pq+}}$ can also drive the exploration of the state-space in the wrong direction as seen for example in TwoCountersInRangeM0 and TwoCounters3.

An artefact of the in-parallel running parity game construction and parity game solution can be observed for the collector_v3_[5-7] and the ltl2dba_R_[6-8] specifications. Here the construction of the states is faster than the algorithm solving the game and when the translation slows down with the increasing size of the alphabet the solver catches up.

4.3 RQ3: Comparison of different minimisation strategies

Experimental Design.

We compare the effect of Mealy machine minimisation and structured encoding on the size of the resulting AIG. For this experiment we use the exploration strategy ${\mathcal{O}}_{\textsf{expl}}^{\textsf{bfs}}$. We compare the four possible combinations: the unstructured and structured encoding functions applied to the unminimised Mealy machine ($l_{\textsf{unstr}}$ and $l_{\textsf{struct}}$) and to the minimised Mealy machine ($l_{\textsf{unstr}}^{\textsf{min}}$ and $l_{\textsf{struct}}^{\textsf{min}}$). Table 7 gives a cross-comparison over all realisable specifications and Table 8 contains outliers where the different techniques have the largest effect and at the bottom cumulative results for the whole set.

Analysis.

The cross-comparison of Table 7 suggests that $l_{\textsf{unstr}}^{\textsf{min}}$ is a good all-round strategy, since it yields smaller circuits compared to the three other approaches. However, Table 8 shows that the structured encoding $l_{\textsf{struct}}$ can sometimes give a significant reduction in size, e.g. for ltl2dba_Q_[6-12]. But sometimes there is also an increase in size, e.g. for round_robin_arbiter_7. This usually happens when minimisation is very effective. The combination $l_{\textsf{struct}}^{\textsf{min}}$ does usually not give an improvement over both $l_{\textsf{struct}}$ and $l_{\textsf{unstr}}^{\textsf{min}}$ on their own. For ltl2dba_beta_[6-10] we have that it can be implemented by a controller using a vector of bits to remember which combinations of inputs have been encountered. The unstructured encoding does not exploit this fact, but this natural structure is restored by $l_{\textsf{struct}}$. For full_arbiter_7, $l_{\textsf{struct}}$ gives a larger AIG than $l_{\textsf{unstr}}$, however it is easier to verify for our model checker, possibly due to the structure kept by $l_{\textsf{struct}}$. Due to these different characteristics we think that a portfolio approach is a sensible default configuration for Strix.

5 Conclusion and Future Work

The success of the described approach implemented in Strix relies on several key factors: (1) a demand-driven construction of the automata and the corresponding arena; (2) LTL translations that produce small deterministic automata on-the-fly; (3) a strategy iteration algorithm for solving parity games; especially the fact that the computed optimal strategy in an exploration step serves as a good initial strategy when computing the strategy for the next step; (4) semantic information that can be used for exploration guidance and controller extraction.

While the experimental evaluation places Strix ahead of other competing tools, specifications with large alphabets are still a challenge and need to be addressed. We think restricting the automata constructions of a decomposed formula to letters not violating other parts of the formula, e.g., safety conditions, could be beneficial, as already shown in DBLP:journals/sttt/SohailS13 . Further, we think we only have scratched the surface of what can be done using the available semantic information and we want to explore potential applications for guiding the exploration of the arena and for extracting implementations, such as circuits but also reactive programs. There are already attempts to extract reactive programs using bounded synthesis DBLP:conf/atva/GerstackerKF18 , but unfortunately this only works for toy examples. Work in this area could help addressing the third challenge mentioned in the introduction (representation of synthesised implementation).

Acknowledgements.

We want to thank the anonymous reviewers for their helpful comments and remarks on this manuscript. We also want to thank Swen Jacobs and Guillermo A. Pérez for valuable feedback and testing of Strix during Syntcomp2019.