On the greatest solution of equations in CLL_R

DOI10.1016/J.IPL.2015.05.008zbMATH Open1332.68146arXiv1502.03629OpenAlexW317546781MaRDI QIDQ2353634FDOQ2353634

Authors: Yan Zhang, Zhaohui Zhu, Jinjin Zhang 

Publication date: 15 July 2015

Published in: Information Processing Letters (Search for Journal in Brave)

Abstract: It is shown that, for any equation $X{=}_{RS}{t}_X$ in the LLTS-oriented process calculus $ext{CLL}_R$, if $X$ is strongly guarded in $t_X$, then the recursive term $langleX|X=t_{X}angle$ is the greatest solution of this equation w.r.t L"{u}ttgen and Vogler's ready simulation.

Full work available at URL: https://arxiv.org/abs/1502.03629

Recommendations

• Recursive equations in higher-order process calculi
• Distributive laws for the coinductive solution of recursive equations
• Solving recursive net equations
• scientific article; zbMATH DE number 1638655
• Unguardedness mostly means many solutions

zbMATH Keywords

formal methodsspecificationprocess calculussolution of equationslogic-labelled transition system

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Title not available (Why is that?)
• Safe reasoning with logic LTS
• Conjunction on processes: Full abstraction via ready-tree semantics
• Ready simulation for concurrency: it's logical!
• The meaning of negative premises in transition system specifications

Cited In (1)

• Encoding safety in \(\mathrm{CLL}_R\)

This page was built for publication: On the greatest solution of equations in \(\mathrm{CLL}_R\)

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