|
Characteristic Formulae: From Automata to Logic
Luca Aceto
January 2007 |
Abstract:
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. |