Thread View: comp.specification
2 messages
2 total messages
Started by Larry Augustin
Sat, 05 Sep 1992 00:31
Looking for linear temporal logic verifiers gnerating counterexamples
Author: Larry Augustin
Date: Sat, 05 Sep 1992 00:31
Date: Sat, 05 Sep 1992 00:31
18 lines
995 bytes
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
Re: Looking for linear temporal logic verifiers gnerating counterexamples
Author: Shinji Kono
Date: Sun, 06 Sep 1992 14:43
Date: Sun, 06 Sep 1992 14:43
19 lines
1405 bytes
1405 bytes
In article <lma.715653113@dayton.Stanford.EDU> , lma@dayton.Stanford.EDU (Larry Augustin) writes >I'm looking for algorithms for producing counterexamples for linear >propositional temporal logic (LPTL) verification. This is a rather easy part in temporal logic verification. In automaton gerating or tableau method, you have a finite automaton, which accepts satisfiable state of givien temporal logic formula. Your problem is how to find a path from start to end in the automaton. By tracing from the terminal state, the shortest example can be found easily. But if you try to find interesting example or meaningfull example, it will be difficult. I have such a verifier written in Prolog for Interval temporal logic ( a variant of LPTL). --- Shinji Kono @ kono@csl.sony.co.jp Sony Computer Science Laboratory, Inc,Japan
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