|
Technical Report: DCC-2014-01
Glushkov and Equation Automata for KAT Expressions
Sabine Broda, António Machiavelo, Nelma Moreira,
Rogério Reis
Centro de Matemática da Universidade do Porto
R. Campo Alegre 687, 4169-007 Porto, Portugal
e-mail: sbb@dcc.fc.up.pt,ajmachia@fc.up.pt,nam@dcc.fc.up.pt,rvr@dcc.fc.up.pt
April 2013
Abstract
Kleene algebra with tests (KAT) is an equational
system that extends Kleene algebra, the algebra of regular
expressions, and that is specially suited to capture and verify
properties of simple imperative programs. In this paper we study two
constructions of automata from \kat expressions: the Glushkov
automaton (Apos), and a new construction based on the notion of
prebase (equation automata, Aeq). Contrary to other automata
constructions from KAT expressions, these two constructions enjoy the
same descriptional complexity behaviour as their counterparts for
regular expressions, both in the worst-case as well as in the
average-case. In particular, our main result is to show that,
asymptotically and on average the number of transitions of the
$Apos$ is linear in the size of the KAT expression.
|