Article View: comp.specification
Article #96Re: Looking for linear temporal logic verifiers gnerating counterexamples
From: 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
Technical Details
Message-ID:
<1992Sep6.144349.8852@nntp.csl.sony.co.jp>Path:
arc1-ca.pugleaf.net!sparky!uunet!kithrup!hoptoad!decwrl!sun-barr!sh.wide!wnoc-tyo-news!scslwide!socslgw!daemonReferences:
<lma.715653113@dayton.Stanford.EDU>Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!sparky!uunet!kithrup!hoptoad!decwrl!sun-barr!sh.wide!wnoc-tyo-news!scslwide!socslgw!daemon From: kono@csl.sony.co.jp (Shinji Kono) Newsgroups: comp.specification Subject: Re: Looking for linear temporal logic verifiers gnerating counterexamples Message-ID: <1992Sep6.144349.8852@nntp.csl.sony.co.jp> Date: 6 Sep 92 14:43:49 GMT References: <lma.715653113@dayton.Stanford.EDU> Sender: daemon@nntp.csl.sony.co.jp (The devil himself) Reply-To: kono@csl.sony.co.jp Organization: Sony Computer Science Laboratory, Inc. Lines: 19