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

Arnold, André; Dicky, Anne

Inf. Comput. 82, No. 2, 198-229 (1989).

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

Citations:

Zbl 0619.68021; Zbl 0557.68029

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