Logical specifications play a key role in the formal analysis of behavioural models. Automating the derivation of such specifications is particularly valuable in complex systems, where manual construction is time-consuming and error-prone. This article presents an approach for generating logical specifications from process models discovered via workflow mining, combining pattern-based translation with automated reasoning techniques. In contrast to earlier work, we evaluate the method on both general-purpose and real-case event logs, enabling a broader empirical assessment. The study examines the impact of data quality, particularly noise, on the structure and testability of generated specifications. Using automated theorem provers, we validate a variety of logical properties, including satisfiability, internal consistency, and alignment with predefined requirements. The results support the applicability of the approach in realistic settings and its potential integration into empirical software engineering practices.