Linear Temporal Logic verifiers generating counterexamples??

Thread View: sci.logic

1 messages

[T] Back to Threads [V] Tree View [G] Group Articles

1 total messages Started by Larry Augustin Sat, 05 Sep 1992 00:18

#142

Author: Larry Augustin
Date: Sat, 05 Sep 1992 00:18

19 lines
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

Thread Navigation

This is a paginated view of messages in the thread with full content displayed inline.

Messages are displayed in chronological order, with the original post highlighted in green.

Use pagination controls to navigate through all messages in large threads.

Back to All Threads