🚀 go-pugleaf

In a recent post, I wrote

TW> EMC is a model checker for CTL formulae over Kripke structures. 
TW> Literature: Emerson, Halper, "Sometimes" and "Not Never" Revisited,
TW> JACM, 33, 1, 1986.

It was brought to my attention that above statement could be construed as
claiming that the mentioned paper was the seminal reference about the EMC
system or model checking. Of course, it is not, but it was the only
reference that mentioned model checking at the time of posting. Model
checking was first proposed by E.M. Clarke.

Probably the best reference for EMC is E.M. Clarke, E.A. Emerson, A.P.
Sistla, "Automatic Verification of Finite-State Concurrent Systems Using
Temporal Logic Specifications", ACM Trans. Programming Languages and
Systems, 8, 2, 1986, pp. 244-263. 

I apologize for any confusion my post might have caused.

Cheers, Thomas.

--
+--------------------------------+---------------------------------+
| Thomas Weigert                 |                                 |
| Machine Inference Section      |                                 |
| Electrotechnical Laboratory    |                                 |
| Umezono 1-1-4, Tukuba-shi      | weigert@{mcs.anl.gov,etl.go.jp} |
| Ibaraki 305, Japan             | +81-298-58-5918 (phone+fax)     |
+--------------------------------+---------------------------------+