Embedding Finite Automata within regular Expressions

Abstract. Regular expressions and their extensions have become a major component of industry-standard specification languages such as PSL/Sugar ([2]). The model checking procedure of regular expression based formulas, as well as of many LTL and CTL formulas, involves constructing an automaton which runs in parallel with the model. In this paper we re-examine this construction. Instead of directly translating a regular expression into an automaton, as traditionally done, we propose an algorithm which allows an intermediate representation mixing both regular expressions and automata. This representation can be thought of as plugging an automaton inside a regular expression, to replace an existing sub-expression. In order to be verified, the intermediate representation is then translated into another automaton, resulting in a set of automata running in parallel. A key feature of this algorithm is that the plug-in automaton is independent of the regular expression from which it originate...

• Type: Conference
• Year: 2004
• Where: ISOLA
• Authors: Shoham Ben-David, Dana Fisman, Sitvanit Ruah
• Keywords: Automaton, Intermediate Representation, ISOLA 2004, Regular Expression