On the greatest solution of equations in CLL_R

DOI10.1016/J.IPL.2015.05.008MaRDI QIDQ2353634zbMATH OpenOpenAlexFDO

Authors Yan Zhang, Zhaohui Zhu, Jinjin Zhang

Publication date 15 July 2015

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

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

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)

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.

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

Cites work

• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• Conjunction on processes: Full abstraction via ready-tree semantics
• Ready simulation for concurrency: it's logical!
• Safe reasoning with logic LTS
• 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)