This Article 
 Bibliographic References 
 Add to: 
Comments on 'Temporal Logic-Based Deadlock Analysis for Ada' by G.M. Karam and R.J.A. Burh
February 1993 (vol. 19 no. 2)
pp. 198-199

The commenters discuss several flaws they found in the above-titled paper by G.M. Koran and R.J.A. Burh. 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.

[1] J. B. Burchet al., "Symbolic model checking: 1020states and beyond," inProc. 5th Symp. Logics in Computer Science, pp. 428-439, IEEE Computer Society Press, 1990.
[2] E. A. Emerson and J. Y. Halpen, "'Sometimes' and 'not never' revisted: On branching versus linear time," inProc. Principles of Programming Languages, Austin, TX, 1983, pp. 127-140.
[3] S. L. Hantler and J. C. King, "An introduction to proving the correctness of programs,"ACM Comput. Surveys, vol. 8, no. 3, pp. 331-353, Sept. 1983.
[4] G. J. Holzmann,Design and Validation of Computer Protocols. Englewood, Cliffs, NJ: Prentice-Hall, 1991.
[5] G. M. Karam and R. J. A. Burh, "Starvation and critical race analyzers for Ada,"IEEE Trans. Software Eng., vol. 16, no. 8, pp. 829-843, Aug. 1990.
[6] G. M. Karam and R. J. A. Burh, "Temporal logic-based deadlock analysis for Ada,"IEEE Trans. Software Eng., vol. 17, no. 10, pp. 1109-1125, Oct. 1991.
[7] R. E. Ladner, "The complexity of problems in systems of communicating sequential processes," inProc. 11th Ass. Comput. Mach. Symp. on Theory of Computing, Atlanta, GA, Apr. 1979, pp. 214-223.
[8] L. Lamport, "Sometimes is sometimes not never," inProc. Ass. Comput. Mach. Symp. Principles of Programming Languages, Las Vegas, NV, Jan. 1980, pp. 174-185.
[9] L. Lamport, "Specifying Concurrent ProgramModules,"ACM Trans. Programming Languages and Systems, Vol. 5, No. 2, Apr. 1983, pp. 190-222.
[10] L. Lamport, "A simple approach to specifying concurrent systems,"Commun. ACM, vol. 32, pp. 32-45, 1989.
[11] C. E. McDowell, "A practical algorithm for static analysis of parallel programs,"J. Parallel and Distributed Process., vol. 6, pp. 515-536, June 1989.
[12] S. A. Smolka, "Analysis of communicating finite state processes," Ph.D. dissertation, Dep. Comput. Sci., Brown Univ., Providence, RI, Tech. Rep. No. CS-84-05, 1984.
[13] R. N. Taylor, "Complexity of analyzing the synchronization structure of concurrent programs,"Acta Informatica, vol. 19, pp. 57-84, 1983.
[14] A. Valmari, "Error detection by reduced reachability graph generation," inProc. 9th European Workshop Application and Theory of Petri Nets, Venice, Italy, 1988, pp. 95-112.

Index Terms:
temporal logic-based deadlock analysis; state-based models; Ada; axiomatic proof method; event-based models; symbolic manipulation; nondeterminism; computational complexity; Ada; computational complexity; concurrency control; symbol manipulation; temporal logic
M. Agrawala, D.L. Jain, "Comments on 'Temporal Logic-Based Deadlock Analysis for Ada' by G.M. Karam and R.J.A. Burh," IEEE Transactions on Software Engineering, vol. 19, no. 2, pp. 198-199, Feb. 1993, doi:10.1109/32.214836
Usage of this product signifies your acceptance of the Terms of Use.