Reasoning with Temporal Logic on Truncated Paths

We consider the problem of reasoning with linear temporal logic on truncated paths. A truncated path is a path that is finite, but not necessarily maximal. Truncated paths arise naturally in several areas, among which are incomplete verification methods (such as simulation or bounded model checking) and hardware resets. We present a formalism for reasoning about truncated paths, and analyze its characteristics.

• Type: Conference
• Year: 2003
• Where: CAV
• Authors: Cindy Eisner, Dana Fisman, John Havlicek, Yoad Lustig, Anthony McIsaac, David Van Campenhout
• Keywords: CAV 2003, Formal Methods, Incomplete Verification Methods, Linear Temporal Logic, Truncated Paths