Characteristic Formulae: From Automata to Logic
AbstractThis 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). https://doi.org/10.7146/brics.v14i2.21925
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.