Pardinus: A Temporal Relational Model Finder

This article presents 𝖯𝖺𝗋𝖽𝗂𝗇𝗎𝗌 , an extension of the popular 𝖪𝗈𝖽𝗄𝗈𝖽 relational model finder with linear temporal logic (including past operators), to simplify the analysis of dynamic systems. 𝖯𝖺𝗋𝖽𝗂𝗇𝗎𝗌 includes a SAT-based bounded-model checking engine and an SMV-based complete model checking engine, both allowing iteration through the different instances (or counter-examples) of a specification. It also supports a decomposed parallel analysis strategy that improves the efficiency of both analysis engines on commodity multi-core machines.