Implementing and Evaluating pLTL to Deterministic Rabin Automata Conversion

Abstract

Linear Temporal Logic with Past (pLTL) extends standard LTL by introducing pasttime operators, enabling more concise specifications of system properties. While theoretically advantageous, applying pLTL in practical verification tasks requires converting its formulas into ω-automata, a process that remains computationally challenging. A recent algorithm proposed by Azzopardi et al.[1] provides a direct construction of deterministic Rabin automata from pLTL formulas, yet no functional implementation of this algorithm currently exists. Without such an implementation, researchers and practitioners lack validation of its feasibility, efficiency, and applicability. This thesis bridges this gap by developing the first working implementation of Azzopardi et al.’s algorithm [1] and systematically evaluating its performance. The study benchmarks the implementation against existing methods that indirectly achieve the same transformation via Büchi automata and determinization tools. We measured construction time and memory usage across both real-world and synthetic pLTL formulas. The results assess the algorithm’s scalability and check whether it offers practical advantages over traditional approaches. Findings from this research contribute to the field of formal methods by providing the first working implementation of the direct pLTL-to-deterministic automata conversion algorithm and offering insight into its performance. It is also the only known tool capable of converting certain types of pLTL formulas with more than 15 temporal operators to ω-automata within reasonable time and memory constraints, a feat previous tools could not achieve. Practitioners could use the produced tool for faster model checking and reactive synthesis, enabling more effective use of pLTL in real-world applications.