A Logical Viewpoint on Process-Algebraic Quotients

We study the following problem: Given a transition system T and its quotient T/∼ under an equivalence ∼, which are the sets L, L′ of Hennessy-Milner formulae such that: if ϕ ∈ L and T satisfies ϕ, then T/∼ satisfies ϕ; if ϕ ∈ L′ and T/∼ satisfies ϕ, then T satisfies ϕ.

• Type: Conference
• Year: 1999
• Where: CSL
• Authors: Antonín Kucera, Javier Esparza
• Keywords: Automated Reasoning, CSL 1999, Quotient T/∼, T/∼ Satisfies