##
**An algebraic characterization of transition system equivalences.**
*(English)*
Zbl 0679.68116

From the text: “I. Castellani [1987, J. Comput. Syst. Sci. 34, 210-235 (1987; Zbl 0619.68021)] has shown that observation equivalence of transition systems could be characterized by particular reductions: systems are equivalent if, and only if, they can be reduced to the same form. Moreover, every transition system has a minimal reduced form. We extend these results to logical equivalence, by an algebraic interpretation of temporal logic: we characterize logical equivalence of transition systems by particular reductions (saturating quasi- homomorphisms) of their power algebras of sets of states and paths and prove that every power algebra has a minimal reduced form. We then offer alternative proofs for logical characterizations of observations equivalence: in particular we apply our method to prove M. Hennessy and C. Stirling’s [Lect. Notes Comput. Sci. 176, 301-311 (1984; Zbl 0557.68029)] result that “Future Perfect” logic characterizes observation equivalence of generalized transition systems, i.e. systems whose infinite behaviours are restricted by arbitrary fairness constraints.”

Reviewer: B.Ponděliček

### MSC:

68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |

### Keywords:

logical equivalence; algebraic interpretation of temporal logic; saturating quasi-homomorphisms; power algebras
PDF
BibTeX
XML
Cite

\textit{A. Arnold} and \textit{A. Dicky}, Inf. Comput. 82, No. 2, 198--229 (1989; Zbl 0679.68116)

Full Text:
DOI

### References:

[1] | Dicky, A., An algebraic and algorithmic method for analysing transition systems, Theoret. Comput. Sci., 46, 285-303 (1986) · Zbl 0617.68035 |

[2] | Bloom, S. L.; Troeger, D. R., A logical characterization of observation equivalence, Theoret. Comput. Sci., 35, 43-53 (1985) · Zbl 0558.68027 |

[3] | Stirling, C., Proof theoretic characterization of observation equivalence, Theoret. Comput. Sci., 39, 27-45 (1985) · Zbl 0567.68020 |

[4] | Kozen, D., Results on the propositional μ-calculus, Theoret. Comput. Sci., 27, 333-354 (1984) · Zbl 0553.03007 |

[5] | Park, D., Concurrency and automata on infinite sequence, (5th GI Conf. on Theoret. Comput. Sci., Karlsruhe. 5th GI Conf. on Theoret. Comput. Sci., Karlsruhe, Lect. Notes in Comput. Sci., Vol. 104 (1981), Springer-Verlag: Springer-Verlag New York/Berlin), 167-183 |

[6] | Hennessy, M.; Milner, R., Algebraic laws for nondeterminism and concurrency, J. Assoc. Comput. Mach., 32, 137-161 (1985) · Zbl 0629.68021 |

[7] | Hennessy, M.; Stirling, C., The power of the future perfect in program logics, (11th Math. Foundations of Comput. Sci.. 11th Math. Foundations of Comput. Sci., Praha. 11th Math. Foundations of Comput. Sci.. 11th Math. Foundations of Comput. Sci., Praha, Lect. Notes in Comput. Sci., Vol. 176 (1984), Springer-Verlag: Springer-Verlag New York/Berlin), 301-311 · Zbl 0557.68029 |

[8] | Castellani, I., Bisimulations and abstraction homomorphisms, J. Comput. System Sci., 34, 210-235 (1987) · Zbl 0619.68021 |

[9] | Sifakis, J., Property-preserving homomorphisms of transition systems, (Logics of Programs. Logics of Programs, Lect. Notes in Comput. Sci., Vol. 164 (1983)), 458-473 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.