On regular temporal logics with past |
| |
Authors: | Christian Dax Felix Klaedtke Martin Lange |
| |
Affiliation: | (1) Dipartimento di Elettronica e Informazione, Politecnico di Milano, P.za Leonardo da Vinci 32, 20133 Milano, Italia;(2) CNR Istituto di Elettronica e di Ingegneria dell’Informazione e delle Telecomunicazioni, sez. Milano, Via Ponzio 34/5, 20133 Milano, Italia |
| |
Abstract: | 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 article, we extend the common core of these specification languages with past operators. We name this extension PPSL.
Although all ω-regular properties are expressible in PSL, SVA, and PPSL, past operators often allow one to specify properties more naturally
and concisely. In fact, we show that PPSL is exponentially more succinct than the cores of PSL and SVA. On the star-free properties,
PPSL is double exponentially more succinct than LTL. Furthermore, we present a translation of PPSL into language-equivalent
nondeterministic Büchi automata, which is based on novel constructions for 2-way alternating automata. The upper bound on
the size of the resulting nondeterministic Büchi automata obtained by our translation is almost the same as the upper bound
for the nondeterministic Büchi automata obtained from existing translations for PSL and SVA. Consequently, the satisfiability
problem and the model-checking problem for PPSL fall into the same complexity classes as the corresponding problems for PSL
and SVA. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|