A logical characterization of observation equivalence

DOI10.1016/0304-3975(85)90004-0MaRDI QIDQ802306zbMATH OpenOpenAlexFDO

Authors Stephen L. Bloom, Douglas R. Troeger

Publication date 1985

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(85)90004-0

zbMATH Keywords

infinitary formal languageobservation equivalencesynchronization treestrace languagetrace logic

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Abstract data types; algebraic specification (68Q65)

Review text

\textit{S. D. Brookes} and \textit{W. C. Rounds} [Lect. Notes Comput. Sci. 154, 97-108 (1983; Zbl 0536.68042)] showed that a finitary formal language ('regular trace language', or Reg-TL, for short) which allowed a certain kind of quantification using regular subsets of \(\Sigma^*\) was not strong enough to distinguish all pairs of observationally inequivalent synchronization trees. In the present paper this result is extended to show that there is no class C of subsets of \(\Sigma^*\) such that C-TL can distinguish all pairs of observationally inequivalent synchronization trees. Then a characterization of observation equivalence in terms of an infinitary formal language S-TL(\(\omega)\) is given. This language is obtained as an extension of the language S-TL ('singleton trace language') of Hennessy and Milner by the addition of a connective of \(\omega\)-conjunctions of formulas of finite bounded depth.

Recommendations

• scientific article; zbMATH DE number 408805
• An algebraic characterization of observational equivalence
• A proof-theoretic characterization of observational equivalence
• scientific article; zbMATH DE number 3858386
• Iteration theories of synchronization trees

Cites work

• A calculus of communicating systems
• Algebraic laws for nondeterminism and concurrency
• Calculi for synchrony and asynchrony
• scientific article; zbMATH DE number 3888909 (Why is no real title available?)
• scientific article; zbMATH DE number 3852428 (Why is no real title available?)
• scientific article; zbMATH DE number 3688686 (Why is no real title available?)
• scientific article; zbMATH DE number 3744561 (Why is no real title available?)
• Synchronization trees

Cited in

(6)

• An algebraic characterization of transition system equivalences
• On the logic of factual equivalence
• scientific article; zbMATH DE number 3878352 (Why is no real title available?)
• scientific article; zbMATH DE number 3936496 (Why is no real title available?)
• scientific article; zbMATH DE number 408805 (Why is no real title available?)
• Proof systems for satisfiability in Hennessy-Milner logic with recursion

This page was built for publication: A logical characterization of observation equivalence

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q802306)