@inbook{d9ba004de0e8438eb6a92f772bbeeea0,
title = "ASERE: Assuring the Satisfiability of Sequential Extended Regular Expressions",
abstract = "One purpose of Property Assurance is to check the satisfiability of properties. The Sequential Extended Regular Expressions (SEREs) play important roles in composing PSL properties. The SEREs are regular expressions with repetition and conjunction. Current assurance method for LTL formulas are not applicable to SEREs. In this paper, we present a method for checking the satisfiability of SEREs. We propose an extension of Alternating Finite Automata with internal transitions and logs of universal branches (IAFA). The new representation enables memoryful synchronization of parallel words. The compilation from SEREs to IAFAs is in linear space. An algorithm, and two optimizations are proposed for searching satisfying words of SEREs. They reduce the stepwise search space to the product of universal branches' guard sets. Experiments confirm their effectiveness.",
keywords = "Alternating Automata, Memoryful Synchronization, Satisfiability",
author = "Naiyong Jin and Huibiao Zhu",
year = "2009",
language = "英语",
isbn = "9783540884781",
series = "Communications in Computer and Information Science",
pages = "237--251",
editor = "Tiziana Margaria and Bernhard Steffen",
booktitle = "Communications in Computer and Information Science",
}