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

DOI10.1016/J.JAL.2015.06.005MaRDI QIDQ893593zbMATH OpenOpenAlexFDO

Authors N. E. Zubov

Publication date 19 November 2015

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

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

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)

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.

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 -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

Cites work

• scientific article; zbMATH DE number 3928330 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 4059362 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 48630 (Why is no real title available?)
• scientific article; zbMATH DE number 2080212 (Why is no real title available?)
• scientific article; zbMATH DE number 3204690 (Why is no real title available?)
• A complete axiomatisation for observational congruence of finite-state behaviours
• A ground-complete axiomatisation of finite-state processes in a generic process algebra
• A logic for the description of non-deterministic programs and their properties
• A logical process calculus
• Axiomatizing weak simulation semantics over BCCSP
• Bisimulation can't be traced
• Bisimulation through probabilistic testing
• Complete inference systems for weak bisimulation equivalences in the -calculus.
• Conjunction on processes: Full abstraction via ready-tree semantics
• Nets, Terms and Formulas
• On recursive operations over logic LTS
• Ready simulation for concurrency: it's logical!
• Safe reasoning with logic LTS
• Software reliability methods. Foreword by Edmund M. Clarke
• The linear time -- branching time spectrum. I: The semantics of concrete, sequential processes.
• The meaning of negative premises in transition system specifications

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)