Article View: sci.logic
Article #142Linear Temporal Logic verifiers generating counterexamples??
From: Larry Augustin
Date: Sat, 05 Sep 1992 00:18
Date: Sat, 05 Sep 1992 00:18
19 lines
974 bytes
974 bytes
I'm looking for algorithms for producing counterexamples for linear propositional temporal logic (LPTL) verification. That is, given two LPTL formulae p and q, check if (p implies q) is valid (check if the complement is satisfiable), and, if it's not, produce an example of a sequence that satisfies p but not q. I would appreciate references to published work. Thanks, Larry --- Larry M. Augustin ERL 414, M/C 4055 lma@dayton.stanford.edu Computer Systems Lab +1 415.723.9285 (voice) Stanford University +1 415.725.7398 (fax) Stanford, CA 94305
Technical Details
Message-ID:
<lma.715652332@dayton.Stanford.EDU>Path:
arc1-ca.pugleaf.net!sparky!uunet!stanford.edu!leland.Stanford.EDU!dayton.Stanford.EDU!lmaShow Full Headers
Complete Article Headers
Newsgroups: sci.logic Path: arc1-ca.pugleaf.net!sparky!uunet!stanford.edu!leland.Stanford.EDU!dayton.Stanford.EDU!lma From: lma@dayton.Stanford.EDU (Larry Augustin) Subject: Linear Temporal Logic verifiers generating counterexamples?? Message-ID: <lma.715652332@dayton.Stanford.EDU> Sender: news@leland.Stanford.EDU (Mr News) Organization: DSO, Stanford University Date: 5 Sep 92 00:18:52 GMT Lines: 20