Automatic Generation of Logical Specifications for Behavioural Models

Logical specifications for behavioural models are crucial for the formal analysis of complex system designs. The automation of obtaining such a specification is essential particularly for promoting logical and deductive methods in software development. This article replicates earlier methods for automatically generating logical specifications equivalent to behavioural models, while also extending the approach to include workflow mining processes. Various and effective interactions with existing theorem provers are also proposed. We conducted straightforward, yet comprehensive, experiments covering multiple stages, which include workflow extraction, automatic logical specification generation, and theorem prover based analysis and the evaluation of these specifications.