Question About Determinism in Automata Construction

[alperkamil]

Hello,

First of all, thank you for providing this excellent library.

I was wondering if there is a straightforward way to ensure determinism in automata construction. For the same LTL input, I sometimes obtain different automata, which I believe might be due to parallelization. This occasionally hinders the reproducibility of my results.

I would greatly appreciate any insights you could provide regarding this issue.

For example, I observed different DPAs constructed from the LTL formula GFb & GFc & (FGd | FGe) & G!a by owl ltl2dpa, I have also encountered this issue with other LTL formulas.

Owl Version: 21.0
OS: Red Hat Enterprise Linux 9.6
Memory: 64 GB
Command: owl ltl2dpa -f 'GFb & GFc & (FGd | FGe) & G!a'

[incaseoftrouble]

IIRC, unfortunately no. We tried to make things as deterministic as possible, but some subtle things remain. Mostly, this is due to non-deterministic ordering in sets.

You can try with state annotations enabled, the indexing is (I think) arbitrary, but the labels should be deterministic.

Anyway, we will likely be working on a complete rework of owl that might solve this issue.