Nested semantics over finite trees are equationally hard

DOI10.1016/j.ic.2004.02.001zbMath1101.68690OpenAlexW2158342623MaRDI QIDQ598202

Luca Aceto, W. J. Fokkink, Anna Ingólfsdóttir, Robert J. van Glabbeek

Publication date: 6 August 2004

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: http://www.brics.dk/NS/03/2/

zbMATH Keywords

Process algebraConcurrencyBCCSPComplete axiomatizationsEquational logicHennessy--Milner logicNested simulationNested trace semanticsNon-finitely based algebrasPossible futures

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (10)

Ready to preorder: an algebraic and general proof ⋮ Bisimilarity is not finitely based over BPA with interrupt ⋮ Non-finite axiomatisability results via reductions: CSP parallel composition and CCS restriction ⋮ A Linear-Time–Branching-Time Spectrum of Behavioral Specification Theories ⋮ On finite alphabets and infinite bases ⋮ Unnamed Item ⋮ Coinductive Characterisations Reveal Nice Relations Between Preorders and Equivalences ⋮ On Finite Bases for Weak Semantics: Failures Versus Impossible Futures ⋮ Unnamed Item ⋮ A linear-time-branching-time spectrum for behavioral specification theories

Cites Work

• CCS expressions, finite state processes, and three problems of equivalence
• The equational theory of pomsets
• Structured operational semantics and bisimulation as a congruence
• Undecidable equivalences for basic process algebra
• Nonaxiomatisability of equivalences over finite state processes
• The max-plus algebra of the natural numbers has no finite equational basis
• Bisimulation equivalence is decidable for all context-free processes
• Decidability of bisimulation equivalence for process generating context-free languages
• Process algebra for synchronous communication
• Algebraic laws for nondeterminism and concurrency
• Formal verification of parallel programs
• A menagerie of non-finitely based process semantics over BPA* – from ready simulation to completed traces
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Nested semantics over finite trees are equationally hard