Generating optimal monitors for extended regular expressions

By Koushik Sen and Grigore Rosu. Electr. Notes Theor. Comput. Sci, 89(2):226–245, 2003.

Publisher Link:

http://dx.doi.org/10.1016/S1571-0661(04)81051-X

Abstract

Ordinary software engineers and programmers can easily understand regular patterns, as shown by the immense interest in and the success of scripting languages like Perl, based essentially on regular expression pattern matching. We believe that regular expressions provide an elegant and powerful specification language also for monitoring requirements, because an execution trace of a program is in fact a string of states. Extended regular expressions (EREs) add complementation to regular expressions, which brings additional benefits by allowing one to specify patterns that must not occur during an execution. Complementation gives one the power to express patterns on strings more compactly. In this paper we present a technique to generate optimal monitors from EREs. Our monitors are deterministic finite automata (DFA) and our novel contribution is to generate them using a modern coalgebraic technique called coinduction. Based on experiments with our implementation, which can be publicly tested and used over the web, we believe that our technique is more efficient than the simplistic method based on complementation of automata which can quickly lead to a highly-exponential state explosion.

BibTeX

@article{journals/entcs/SenR03,
    author = "Sen, Koushik and Rosu, Grigore",
    title = "Generating Optimal Monitors for Extended Regular
             Expressions",
    ee = "http://dx.doi.org/10.1016/S1571-0661(04)81051-X",
    journal = "Electr. Notes Theor. Comput. Sci",
    keywords = "formal methods, sensor networks, real-time systems,
                software engineering",
    number = "2",
    pages = "226-245",
    volume = "89",
    year = "2003",
}