home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #20 / NN_1992_20.iso / spool / sci / logic / 1352 < prev    next >
Encoding:
Text File  |  1992-09-07  |  946 b   |  31 lines
  1. Newsgroups: sci.logic
  2. Path: sparky!uunet!stanford.edu!leland.Stanford.EDU!dayton.Stanford.EDU!lma
  3. From: lma@dayton.Stanford.EDU (Larry Augustin)
  4. Subject: Linear Temporal Logic verifiers generating counterexamples??
  5. Message-ID: <lma.715652332@dayton.Stanford.EDU>
  6. Sender: news@leland.Stanford.EDU (Mr News)
  7. Organization: DSO, Stanford University
  8. Date:  5 Sep 92 00:18:52 GMT
  9. Lines: 20
  10.  
  11. I'm looking for algorithms for producing counterexamples for linear
  12. propositional temporal logic (LPTL) verification.
  13.  
  14. That is, given two LPTL formulae p and q, check if (p implies q) is
  15. valid (check if the complement is satisfiable), and, if it's not,
  16. produce an example of a sequence that satisfies p but not q.
  17.  
  18. I would appreciate references to published work.
  19.  
  20. Thanks,
  21.  
  22. Larry
  23.  
  24. ---
  25.  
  26. Larry M. Augustin            ERL 414, M/C 4055
  27. lma@dayton.stanford.edu            Computer Systems Lab
  28. +1 415.723.9285 (voice)            Stanford University
  29. +1 415.725.7398 (fax)            Stanford, CA 94305
  30.  
  31.