A Logical Viewpoint on Process-algebraic Quotients
Autoři | |
---|---|
Rok publikování | 2003 |
Druh | Článek v odborném periodiku |
Časopis / Zdroj | Journal of logic and computation |
Fakulta / Pracoviště MU | |
Citace | |
Obor | Informatika |
Klíčová slova | transition systems; behavioural equivalences; quotients |
Popis | Let E be a process equivalence. A formula F is preserved by E-quotients iff for every process S of a transition system T we have that if S satisfies F, then also [S] satisfies F, where [S] is the equivalence class of S in the quotient of T under E. We classify all formulae of Hennessy-Milner logic which are preserved by E-quotients of image-finite processes. Our result is generic in the sense that it works for a large class of process equivalences which admit a modal characterization in Hennessy-Milner logic satisfying certain closure properties. A practical applicability of the result is demonstrated on equivalences of the linear/branching time spectrum. |
Související projekty: |