Linear temporal logic (LTL) is widely used in industrial verification. LTL formulae can be learned from traces. Scaling LTL formula learning is an open problem. We implement the first GPU-based LTL learner using a novel form of enumerative program synthesis. The learner is sound and complete. Our benchmarks indicate that it handles traces at least 2048 times more numerous, and on average at least 46 times faster than existing state-of-the-art learners. This is achieved with, among others, novel branch-free LTL semantics that has $O(\log n)$ time complexity, where $n$ is trace length, while previous implementations are $O(n^2)$ or worse (assuming bitwise boolean operations and shifts by powers of 2 have unit costs -- a realistic assumption on modern processors).

翻译：线性时序逻辑（LTL）广泛应用于工业验证领域。LTL公式可从轨迹中学习得到，但扩展LTL公式的学习仍是一个开放性问题。我们首次实现了一种基于GPU的LTL学习器，采用新颖的枚举式程序综合方法。该学习器既具有完备性又具有可靠性。基准测试表明，与现有最先进的学习器相比，我们的方法可处理至少2048倍的轨迹数量，平均速度提升至少46倍。这一突破主要得益于创新的无分支LTL语义，其时间复杂度为$O(\log n)$（其中$n$为轨迹长度），而此前实现的时间复杂度为$O(n^2)$或更差（假设按位布尔运算和2的幂次移位操作的单元成本——这一假设在现代处理器上成立）。