home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #20 / NN_1992_20.iso / spool / comp / specific / 412 next >
Encoding:
Text File  |  1992-09-07  |  967 b   |  29 lines
  1. Newsgroups: comp.specification
  2. Path: sparky!uunet!stanford.edu!leland.Stanford.EDU!dayton.Stanford.EDU!lma
  3. From: lma@dayton.Stanford.EDU (Larry Augustin)
  4. Subject: Looking for linear temporal logic verifiers gnerating counterexamples
  5. Message-ID: <lma.715653113@dayton.Stanford.EDU>
  6. Sender: news@leland.Stanford.EDU (Mr News)
  7. Organization: DSO, Stanford University
  8. Date:  5 Sep 92 00:31:53 GMT
  9. Lines: 18
  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.  It's the
  17. counterexample part that I'm interested in.
  18.  
  19. Thanks,
  20.  
  21. Larry
  22.  
  23. ---
  24.  
  25. Larry M. Augustin            ERL 414, M/C 4055
  26. lma@dayton.stanford.edu            Computer Systems Lab
  27. +1 415.723.9285 (voice)            Stanford University
  28. +1 415.725.7398 (fax)            Stanford, CA 94305
  29.