1. LTL translation benchmark

This page shows the result of some benchmarks run with LBTT.

1.1. Keys

LaCIM and FM correspond to the two algorithms of J.-M. Couvreur that are implemented in Spot.

degen means the automata has been degeneralized. gen means it is still generalized.

LTLopt means the LTL formula has been simplified beforehand using Oddoux's ltl2ba implementation. (This is historic, because we did not have rewriting rules in Spot itself when we started doing such benchmark.)

+pre means the formula has been simplified with all the LTL rewriting rules implemented in Spot.

+post means the automaton has been simplified with direct simulation.

symb_merge and exprop are two options corresponding respectively to the merge states ... and optimize determinism check-boxes of the on-line translator

+flapprox stands for fair loop approximations

+post_branch is branching postponement

1.2. Versions

Spot 0.0u of 2004-06-26.

Spin is version 4.0.6

Produces degeneralized automata only.

LBT is version 1.2.1

ltl2ba is version 1.0

The generalized version of ltl2ba is a quite unfair measure. First the generalized automata is an intermediate step of their algorithm and I think their SCC optimizations are applied only afterwards (OTOH Spot doesn't yet perform such SCC optimization). Second their generalized automata have several initial states, while LBTT accepts only one initial state, I had to fix this by merging their initial states (sometimes adding a new initial state, sometimes removing some). The resulting automaton is still correct, but it can be larger or smaller by one state.

Wring is version 1.1.0.

It translations can fail due to random Perl errors.
(Their NEWS files recommend using only Perl 5.005, and I haven't tried that.) I'm using wring2lbtt. Apparently ./wring2lbtt --5 or ./wring2lbtt -d --5 makes no difference: the produced automata are always degeneralized.

Modella is version 1.5.1

Produces degeneralized automata only.

LTL2NBA has no version.

Produces degeneralized automata only.

1.3. A note on times

Most of these translators are run through a set of programs or scripts to perform a conversion to and from LBTT. The only algorithms that need no wrapper are LBT, ltl2ba degen (but not the gen version), and Modella.

The run-time of these wrappers is included in the times displayed below. These wrappers can actually be slower than the LTL translation itself, however they have a complexity linear in the size of the LTL formula and automaton.

Therefore it is hard to compare the speed of two different algorithms: if they differ only by a few second it might be because one of the wrapper is slower.

Also no effort have been made to compile these tools with optimizations. The FM and LaCIM tests, for instance, were run with a development version of Spot compiled with assertion checking turned on and all compiler optimizations explicitly disabled. Tools like Wring and LTL2NBA are script, in Perl and Python, so they will not compete with native code.

2. Results

Each table (except the last) sums the size of the automata produced for 100 random formulas, as well as the size of the product with a random state space.

The last table use 39 known formulae.

2.1. 100 random formulae of size 10

		automata			translating	product		successful
	Algorithm	states	trans.	acc.	time (sec)	states	trans.	translations
0	LaCIM, degen	1368	7424	98	5.44	273578	14325980	100
1	LaCIM, gen	962	5010	130	5.37	192400	10589209	100
1b	LaCIM, gen, +pre	812	3878	103	5.38	162400	8765697	100
2	LaCIM, degen, +pre, +post	1099	5265	97	26.06	219756	11262463	100
3	LaCIM, gen, +pre, +post	795	3727	103	10.28	159000	8479070	100
4	FM, degen, +symb_merge, +exprop, LTLopt	572	1239	97	6.66	114202	4232307	100
5	FM, degen, +symb_merge, +exprop, +pre	565	1223	97	5.22	112802	4185417	100
6	FM, degen, +symb_merge, +exprop, +pre, +post	497	990	97	5.44	99282	3516845	100
7	FM, degen, +symb_merge, +exprop, +pre, +post, +flapprox	497	990	97	6.02	99282	3516845	100
8	FM, degen, +symb_merge, +exprop, +pre, +post, +flapprox, +post_branch	527	1156	97	5.41	105323	3509804	100
9	FM, degen, +symb_merge, +exprop, +post_branch, LTLopt	566	1238	97	6.63	113002	4126367	100
10	FM, degen, +symb_merge, +exprop, +flapprox, LTLopt	541	1110	97	6.71	108077	3864929	100
11	FM, degen, +symb_merge, +exprop, +post_branch, +flapprox, LTLopt	568	1302	97	6.65	113448	3798906	100
12	FM, gen, -symb_merge, -exprop	553	1172	104	5.14	110598	4638420	100
13	FM, gen, -symb_merge, +exprop	553	1172	104	5.11	110484	3988863	100
14	FM, gen, +symb_merge, -exprop	524	1086	104	5.20	104798	4421932	100
15	FM, gen, +symb_merge, +exprop	524	1086	104	5.38	104709	3832079	100
16	FM, gen, -symb_merge, -exprop, LTLopt	511	1035	100	6.47	102198	4084879	100
17	FM, gen, -symb_merge, +exprop, LTLopt	511	1035	100	6.72	102089	3606468	100
18	FM, gen, +symb_merge, -exprop, LTLopt	494	975	100	6.63	98798	3935920	100
19	FM, gen, +symb_merge, +exprop, LTLopt	494	975	100	6.58	98707	3504671	100
20	FM, gen, +symb_merge, +exprop, +post_branch, LTLopt	492	986	100	6.61	98307	3444569	100
21	FM, gen, +symb_merge, +exprop, +flapprox, LTLopt	494	963	102	6.59	98707	3504084	100
22	FM, gen, +symb_merge, +exprop, +post_branch, +flapprox, LTLopt	539	1179	102	6.74	107681	3555402	100
23	FM, gen, +symb_merge, +exprop, +pre	487	959	100	5.27	97307	3457781	100
24	FM, gen, +symb_merge, +exprop, +pre, +post	479	919	103	5.65	95712	3373359	100
25	FM, gen, +symb_merge, +exprop, +pre, +post, +flapprox	479	919	103	5.33	95712	3373359	100
26	FM, gen, +symb_merge, +exprop, +pre, +post, +flapprox, +post_branch	524	1126	103	5.66	104692	3456246	100
27	Spin	723	2134	100	2.30	143191	7760542	100
28	LBT	1611	4498	133	1.15	321998	17171915	100
29	LTL2BA, degen	547	1172	100	1.21	109400	5147646	100
30	LTL2BA, gen (unfair)	507	1014	106	6.19	101400	4509576	100
31	Wring (Wring RewRule+BoolOpt+AutSempl)	761	1336	58	13.98	152125	6292227	96
32	Wring (Wring RewRule+BoolOpt+AutSempl), degen	761	1336	96	13.82	152125	6292227	96
33	Modella -o1 -g -e -r12	561	1181	100	0.77	112093	4078015	100
34	LTLNBA	499	991	97	8.96	99800	4392836	100

2.2. 100 random formulae of size 15..20

		automata			translating	product		successful
	Algorithm	states	trans.	acc.	time (sec)	states	trans.	translations
0	LaCIM, degen	6163	109497	97	13.56	1231860	66074303	100
1	LaCIM, gen	3287	53231	234	8.21	657400	40415644	100
1b	LaCIM, gen, +pre	2363	32343	193	7.11	472600	28859644	100
2	LaCIM, degen, +pre, +post	4163	55125	95	15982.94	832054	44600087	100
3	LaCIM, gen, +pre, +post	2330	31648	193	2018.34	466000	28218378	100
4	FM, degen, +symb_merge, +exprop, LTLopt	1286	5109	96	7.41	253084	9304307	100
5	FM, degen, +symb_merge, +exprop, +pre	1242	4907	95	5.87	244259	8852258	100
6	FM, degen, +symb_merge, +exprop, +pre, +post	1126	3944	95	33.20	222664	7985472	100
7	FM, degen, +symb_merge, +exprop, +pre, +post, +flapprox	1126	3944	95	34.05	222664	7985472	100
8	FM, degen, +symb_merge, +exprop, +pre, +post, +flapprox, +post_branch	1237	5376	95	44.84	241064	8367693	100
9	FM, degen, +symb_merge, +exprop, +post_branch, LTLopt	1171	4571	96	7.42	229646	8000221	100
10	FM, degen, +symb_merge, +exprop, +flapprox, LTLopt	1370	5095	96	7.56	270466	9680573	100
11	FM, degen, +symb_merge, +exprop, +post_branch, +flapprox, LTLopt	1446	6557	96	8.56	280294	9626074	100
12	FM, gen, -symb_merge, -exprop	1161	4455	200	5.78	231971	11344438	100
13	FM, gen, -symb_merge, +exprop	1161	4455	200	6.51	229575	8509410	100
14	FM, gen, +symb_merge, -exprop	1023	3609	200	5.26	204447	9609560	100
15	FM, gen, +symb_merge, +exprop	1023	3609	200	6.02	203077	7552753	100
16	FM, gen, -symb_merge, -exprop, LTLopt	1056	4000	191	7.15	211001	10170928	100
17	FM, gen, -symb_merge, +exprop, LTLopt	1056	4000	191	7.74	208817	7563089	100
18	FM, gen, +symb_merge, -exprop, LTLopt	961	3331	191	7.06	192050	8790687	100
19	FM, gen, +symb_merge, +exprop, LTLopt	961	3331	191	7.30	190684	6831836	100
20	FM, gen, +symb_merge, +exprop, +post_branch, LTLopt	899	3122	191	7.24	177998	6080813	100
21	FM, gen, +symb_merge, +exprop, +flapprox, LTLopt	961	3234	195	7.29	190684	6831488	100
22	FM, gen, +symb_merge, +exprop, +post_branch, +flapprox, LTLopt	1123	4833	193	8.41	218643	7527049	100
23	FM, gen, +symb_merge, +exprop, +pre	924	3155	191	5.77	183256	6444188	100
24	FM, gen, +symb_merge, +exprop, +pre, +post	898	2895	193	8.95	178232	6233221	100
25	FM, gen, +symb_merge, +exprop, +pre, +post, +flapprox	898	2895	193	9.16	178232	6233221	100
26	FM, gen, +symb_merge, +exprop, +pre, +post, +flapprox, +post_branch	1056	4310	193	17.69	206843	7063050	100
27	Spin	2044	13924	100	2856.37	398617	27056967	100
28	LBT	disabled
29	LTL2BA, degen	1175	4577	100	1.14	234870	12759396	100
30	LTL2BA, gen (unfair)	1004	3591	193	6.80	200729	10310947	100
31	Wring (Wring RewRule+BoolOpt+AutSempl)	disabled
32	Wring (Wring RewRule+BoolOpt+AutSempl), degen	disabled
33	Modella -o1 -g -e -r12	1472	6253	100	48.45	290869	10430392	100
34	LTL2NBA	1065	3881	95	47.50	212866	11464267	100

2.3. 39 known formulae

These are the formulae in http://www.science.unitn.it/~stonetta/modella/cfltl and http://www.science.unitn.it/~stonetta/modella/bfltl

		automata			translating	product		successful
	Algorithm	states	trans.	acc.	time (sec)	states	trans.	translations
0	LaCIM, degen	1378	13643	39	2.96	250389	11566062	39
1	LaCIM, gen	651	5603	81	2.15	129400	7147004	39
1b	LaCIM, gen, +pre	500	4409	76	2.20	99200	5475511	39
2	LaCIM, degen, +pre, +post	851	5671	38	7067.66	152998	7385199	39
3	LaCIM, gen, +pre, +post	416	3792	76	204.59	82196	4325770	39
4	FM, degen, +symb_merge, +exprop, LTLopt	222	904	37	2.65	43119	1813690	39
5	FM, degen, +symb_merge, +exprop, +pre	225	883	38	2.26	43719	1818870	39
6	FM, degen, +symb_merge, +exprop, +pre, +post	198	515	38	3.49	38785	1520334	39
7	FM, degen, +symb_merge, +exprop, +pre, +post, +flapprox	198	515	38	3.32	38785	1520334	39
8	FM, degen, +symb_merge, +exprop, +pre, +post, +flapprox, +post_branch	194	551	38	2.83	37459	1402330	39
9	FM, degen, +symb_merge, +exprop, +post_branch, LTLopt	223	909	37	2.65	43220	1791687	39
10	FM, degen, +symb_merge, +exprop, +flapprox, LTLopt	220	851	37	2.45	43126	1693270	39
11	FM, degen, +symb_merge, +exprop, +post_branch, +flapprox, LTLopt	216	921	37	2.78	41005	1604236	39
12	FM, gen, -symb_merge, -exprop	250	1735	74	2.38	46387	3360454	39
13	FM, gen, -symb_merge, +exprop	250	1735	74	2.38	46110	1951413	39
14	FM, gen, +symb_merge, -exprop	189	622	74	2.16	37200	2271545	39
15	FM, gen, +symb_merge, +exprop	189	622	74	2.01	37174	1580669	39
16	FM, gen, -symb_merge, -exprop, LTLopt	217	1599	64	2.79	39788	2816419	39
17	FM, gen, -symb_merge, +exprop, LTLopt	217	1599	64	2.84	39511	1590360	39
18	FM, gen, +symb_merge, -exprop, LTLopt	165	527	64	2.64	32400	1865274	39
19	FM, gen, +symb_merge, +exprop, LTLopt	165	527	64	2.59	32374	1310746	39
20	FM, gen, +symb_merge, +exprop, +post_branch, LTLopt	167	527	64	2.56	32737	1293659	39
21	FM, gen, +symb_merge, +exprop, +flapprox, LTLopt	165	512	64	2.55	32374	1310746	39
22	FM, gen, +symb_merge, +exprop, +post_branch, +flapprox, LTLopt	182	624	64	2.81	34564	1326087	39
23	FM, gen, +symb_merge, +exprop, +pre	170	549	70	2.08	33374	1369670	39
24	FM, gen, +symb_merge, +exprop, +pre, +post	162	489	70	2.65	31796	1284775	39
25	FM, gen, +symb_merge, +exprop, +pre, +post, +flapprox	162	489	70	2.78	31796	1284775	39
26	FM, gen, +symb_merge, +exprop, +pre, +post, +flapprox, +post_branch	168	543	70	2.43	32561	1232735	39
27	Spin	277	1196	39	450.10	54200	3548935	39
28	LBT	844	5584	83	0.57	161040	12530060	39
29	LTL2BA, degen	205	624	39	0.47	40200	2480261	39
30	LTL2BA, gen (unfair)	169	506	71	2.33	33200	1941344	39
31	Wring (Wring RewRule+BoolOpt+AutSempl)	276	1480	36	40.80	50986	3041195	38
32	Wring (Wring RewRule+BoolOpt+AutSempl), degen	407	5339	38	42.45	58762	4377735	38
33	Modella -o1 -g -e -r12	283	867	39	18.07	55689	2119971	39
34	LTL2NBA	235	1022	37	800.11	40800	2777045	39