×

zbMATH — the first resource for mathematics

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.)
PDF BibTeX XML Cite
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, (), 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, (), 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, (), 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.