On Regular Temporal Logics with Past,

The IEEE standardized Property Specification Language, PSL for short, extends the well-known linear-time temporal logic LTL with so-called semi-extended regular expressions. PSL and the closely related SystemVerilog Assertions, SVA for short, are increasingly used in many phases of the hardware design cycle, from specification to verification. In this paper, we extend the common core of these specification languages with past operators. We name this extension RTL. Although all -regular properties are expressible in PSL, SVA, and RTL, past operators often allow one to specify properties more naturally and concisely. In fact, we show that RTL is exponentially more succinct than the cores of PSL and SVA. Furthermore, we present a translation of RTL into languageequivalent nondeterministic B?uchi automata, which is based on novel constructions for 2-way alternating automata. Our translation has almost the same worst-case complexity in terms of the size of the resulting nondeterministic B?u...

• Type: Conference
• Year: 2009
• Where: ICALP
• Authors: Christian Dax, Felix Klaedtke, Martin Lange
• Keywords: Extension Rtl, ICALP 2009, RTL Fall, RTL Formulas, Theoretical Computer Science