Characteristic Formulae: From Automata to Logic

Luca Aceto
Anna Ingólfsdóttir

January 2007


This paper discusses the classic notion of characteristic formulae for processes using variations on Hennessy-Milner logic as the underlying logical specification language. It is shown how to characterize logically (states of) finite labelled transition systems modulo bisimilarity using a single formula in Hennessy-Milner logic with recursion. Moreover, characteristic formulae for timed automata with respect to timed bisimilarity and the faster-than preorder of Moller and Tofts are offered in terms of the logic of Laroussinie, Larsen and Weise.

Available as PostScript, PDF, DVI.


Last modified: 2007-01-18 by webmaster.