Characteristic Formulae: From Automata to Logic

  • Luca Aceto
  • Anna Ingólfsdóttir


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 L_nu of Laroussinie, Larsen and Weise.
How to Cite
Aceto, L., & Ingólfsdóttir, A. (2007). Characteristic Formulae: From Automata to Logic. BRICS Report Series, 14(2).