From PSL to NBA: a Modular Symbolic Encoding

The IEEE standard Property Specification Language (PSL) allows to express all omega-regular properties mixing Linear Temporal Logic (LTL) with Sequential Extended Regular Expressions (SEREs), and is increasingly used in many phases of the hardware design cycle, from specification to verification.Many verification engines are able to manipulate Nondeterministic Buchi Automata (NIBA), that can represent omega-regular properties. Thus, the ability to convert PSL into NBA is an important enabling factor for the reuse of a large wealth of verification tools.Recent works propose a two-step conversion from PSL to NBA: first, the PSL property is encoded into an Alternating Buchi Automaton (ABA); then, the ABA is converted into an NBA with variants of Miyano-Hayashi's construction. These approaches are problematic in practice: in fact, they are often unable to carry out the conversion in acceptable time, even for PSL specifications of moderate size.In this paper, we propose a modular encoding o...