Comments on "Temporal logic-based deadlock analysis for Ada" by G.M. Karam and R.J.A. Burh

The commenters discuss several flaws they found in the above-titled paper by G.M. Koran and R.J.A. Burh (see ibid., vol.17, no.10, p.109-1125, (1991)). The commenters argue that the characterization of operational and axiomatic proof method is modified and inaccurate; the classification of modeling techniques for concurrent systems confuses the distinction between state-based and event-based models with the essential distinction between explicit enumeration of behaviors and symbolic manipulation of properties; the statements about the limitations of linear-time temporal logic in relation to nondeterminism are inaccurate; and the characterization of the computational complexity of the analysis technique is overly optimistic.<>