A Logical Viewpoint on Process-algebraic Quotients

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

KUČERA Antonín ESPARZA Javier

Year of publication 2003
Type Article in Periodical
Magazine / Source Journal of logic and computation
MU Faculty or unit

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.