A Logical Viewpoint on Process-algebraic Quotients
| Authors | |
|---|---|
| Year of publication | 2003 |
| Type | Article in Periodical |
| Magazine / Source | Journal of logic and computation |
| MU Faculty or unit | |
| Citation | |
| Field | Informatics |
| Keywords | transition systems; behavioural equivalences; quotients |
| Description | 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. |
| Related projects: |