Looking for linear temporal logic verifiers gnerating counterexamples

Article View: comp.specification

Article #95

Back to comp.specification Previous Next

#95

From: Larry Augustin
Date: Sat, 05 Sep 1992 00:31

18 lines
995 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.  It's the
counterexample part that I'm interested in.

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.715653113@dayton.Stanford.EDU>

Path: arc1-ca.pugleaf.net!sparky!uunet!stanford.edu!leland.Stanford.EDU!dayton.Stanford.EDU!lma

Show Full Headers

Complete Article Headers

Newsgroups: comp.specification
Path: arc1-ca.pugleaf.net!sparky!uunet!stanford.edu!leland.Stanford.EDU!dayton.Stanford.EDU!lma
From: lma@dayton.Stanford.EDU (Larry Augustin)
Subject: Looking for linear temporal logic verifiers gnerating counterexamples
Message-ID: <lma.715653113@dayton.Stanford.EDU>
Sender: news@leland.Stanford.EDU (Mr News)
Organization: DSO, Stanford University
Date:  5 Sep 92 00:31:53 GMT
Lines: 18