home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #18 / NN_1992_18.iso / spool / comp / parallel / 1893 < prev    next >
Encoding:
Text File  |  1992-08-11  |  1.9 KB  |  48 lines
  1. Newsgroups: comp.parallel
  2. Path: sparky!uunet!gatech!hubcap!fpst
  3. From: weigert@etlhit.etl.go.jp (Thomas Weigert)
  4. Subject: Re: verification of real-time specs
  5. In-Reply-To: weigert@etlhit.etl.go.jp's message of 7 Aug 92 09: 23:39 GMT
  6. Message-ID: <1992Aug12.122012.6709@hubcap.clemson.edu>
  7. Apparently-To: hypercube-request@hubcap.clemson.edu
  8. Sender: news@etl.go.jp (News System)
  9. Nntp-Posting-Host: etlhit
  10. Reply-To: weigert@mcs.anl.gov
  11. Organization: Electrotechnical Laboratory, Tsukuba-shi, Japan
  12. References: <1992Aug7.121831.26534@hubcap.clemson.edu>
  13. Date: Wed, 12 Aug 1992 06:49:17 GMT
  14. Approved: parallel@hubcap.clemson.edu
  15. Lines: 31
  16.  
  17.  
  18. In a recent post, I wrote
  19.  
  20. TW> EMC is a model checker for CTL formulae over Kripke structures. 
  21. TW> Literature: Emerson, Halper, "Sometimes" and "Not Never" Revisited,
  22. TW> JACM, 33, 1, 1986.
  23.  
  24. It was brought to my attention that above statement could be construed as
  25. claiming that the mentioned paper was the seminal reference about the EMC
  26. system or model checking. Of course, it is not, but it was the only
  27. reference that mentioned model checking at the time of posting. Model
  28. checking was first proposed by E.M. Clarke.
  29.  
  30. Probably the best reference for EMC is E.M. Clarke, E.A. Emerson, A.P.
  31. Sistla, "Automatic Verification of Finite-State Concurrent Systems Using
  32. Temporal Logic Specifications", ACM Trans. Programming Languages and
  33. Systems, 8, 2, 1986, pp. 244-263. 
  34.  
  35. I apologize for any confusion my post might have caused.
  36.  
  37. Cheers, Thomas.
  38.  
  39. --
  40. +--------------------------------+---------------------------------+
  41. | Thomas Weigert                 |                                 |
  42. | Machine Inference Section      |                                 |
  43. | Electrotechnical Laboratory    |                                 |
  44. | Umezono 1-1-4, Tukuba-shi      | weigert@{mcs.anl.gov,etl.go.jp} |
  45. | Ibaraki 305, Japan             | +81-298-58-5918 (phone+fax)     |
  46. +--------------------------------+---------------------------------+
  47.  
  48.