Inconsistencies in the Process Specification Language (PSL).
Michael Beeson, Jay Halcomb, Wolfgang Mayer · 2011
The Process Specification Language (PSL) [6] is a first-order logical theory designed to describe manufac-turing or business processes and formalize reasoning about them. It has been developed by several authors over a period of years, yet it is inconsistent with the simplest axioms that preclude non-trivial models. We demonstrate several inconsistencies using an automated theorem prover and attempt to repair the inconsis-tencies. We conclude that even with our amendments, PSL with its infinite models remains inadequate to represent complex industrial processes. We propose an alternative axiomatization that admits finite models, which may be better suited to automated theorem provers and model finders than the current version of PSL. 1