Axiomatizing Lüttgen \& Vogler's ready simulation for finite processes in CLL_R

DOI10.1016/J.JAL.2015.06.005zbMATH Open1457.68196arXiv1502.03636OpenAlexW1589611972MaRDI QIDQ893593FDOQ893593

Authors: N. E. Zubov 

Publication date: 19 November 2015

Published in: Journal of Applied Logic (Search for Journal in Brave)

Abstract: In the framework of logic labelled transition system, a variant of weak ready simulation has been presented by L"{u}ttgen and Vogler. It has been shown that such behavioural preorder is the largest precongruence w.r.t parallel and conjunction composition satisfying desired properties. This paper offers a ground-complete axiomatization for this precongruence over processes containing no recursion in the calculus $ext{CLL}_R$. Compared with usual inference system for process calculus, in addition to axioms about process operators, such system contains a number of axioms to characterize the interaction between process operators and logical operators.

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

Recommendations

• Testing Finitary Probabilistic Processes
• scientific article; zbMATH DE number 3957058
• scientific article; zbMATH DE number 2169337
• \(L^p\) simulation for measures
• Finite axiomatization for symbolic probabilistic \(\pi \)-calculus
• An axiomatic approach to numerical approximations of stochastic processes
• Coinductive Proof Principles for Stochastic Processes
• A complete axiomatization of finite-state ACSR processes
• Proof(s) of the Lamperti representation of continuous-state branching processes
• The Vervaat process in \(L_p\) spaces

zbMATH Keywords

axiomatizationprocess calculuslogic labelled transition systemweak ready simulation

Mathematics Subject Classification ID

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

Cites Work

• The linear time -- branching time spectrum. I: The semantics of concrete, sequential processes.
• Title not available (Why is that?)
• Title not available (Why is that?)
• Bisimulation can't be traced
• Title not available (Why is that?)
• Software reliability methods. Foreword by Edmund M. Clarke
• Bisimulation through probabilistic testing
• Title not available (Why is that?)
• Nets, Terms and Formulas
• Safe reasoning with logic LTS
• A complete axiomatisation for observational congruence of finite-state behaviours
• 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
• Title not available (Why is that?)
• A logic for the description of non-deterministic programs and their properties
• Complete inference systems for weak bisimulation equivalences in the \(\pi\)-calculus.
• On recursive operations over logic LTS
• Title not available (Why is that?)
• A logical process calculus
• Title not available (Why is that?)
• Axiomatizing weak simulation semantics over BCCSP
• A ground-complete axiomatisation of finite-state processes in a generic process algebra

Cited In (2)

• Encoding safety in \(\mathrm{CLL}_R\)
• A theory of hyperfinite processes: The complete removal of individual uncertainty via exact LLN

This page was built for publication: Axiomatizing Lüttgen \& Vogler's ready simulation for finite processes in \(\mathrm{CLL}_{R}\)

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