Paper Info
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.
Year
DOI
Venue
2008
10.1007/978-3-540-88479-8_17
Communications in Computer and Information Science
Keywords
Field
DocType
Alternating Automata,Satisfiability,Memoryful Synchronization
Regular expression,Algebra,Computer science,Satisfiability,Theoretical computer science
Conference
Volume
ISSN
Citations 
17
1865-0929
0
PageRank 
References 
Authors
0.34
15
2
Name
Order
Citations
PageRank
Naiyong Jin1958.40
Huibiao Zhu258386.68