Concurrent Kleene algebra and its foundations

DOI10.1016/J.JLAP.2011.04.005MaRDI QIDQ549679zbMATH OpenOpenAlexWikidataFDO

Authors Bernhard Möller, Georg Struth, Ian Wehrman, Tony Hoare

Publication date 18 July 2011

Published in The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL https://opus.bibliothek.uni-augsburg.de/opus4/frontdoor/index/index/docId/38907

zbMATH Keywords

dependenceconcurrencyKleene algebraHoare calculusrely/guarantee calculus

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Foundations of concurrent Kleene algebra
• Concurrent Kleene Algebra
• Developments in concurrent Kleene algebra
• Concurrent Kleene algebra: free model and completeness
• Developments in concurrent Kleene algebra

Cites work

• scientific article; zbMATH DE number 1612485 (Why is no real title available?)
• scientific article; zbMATH DE number 4018370 (Why is no real title available?)
• scientific article; zbMATH DE number 4030272 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 3735177 (Why is no real title available?)
• scientific article; zbMATH DE number 3772918 (Why is no real title available?)
• scientific article; zbMATH DE number 46487 (Why is no real title available?)
• scientific article; zbMATH DE number 46740 (Why is no real title available?)
• scientific article; zbMATH DE number 1216133 (Why is no real title available?)
• scientific article; zbMATH DE number 701387 (Why is no real title available?)
• scientific article; zbMATH DE number 1555176 (Why is no real title available?)
• scientific article; zbMATH DE number 3995041 (Why is no real title available?)
• scientific article; zbMATH DE number 3204690 (Why is no real title available?)
• scientific article; zbMATH DE number 3366846 (Why is no real title available?)
• A calculus of communicating systems
• A completeness theorem for Kleene algebras and the algebra of regular events
• An axiomatic basis for computer programming
• Concurrent Kleene Algebra
• Concurrent Kleene algebra and its foundations
• Fixed-point calculus
• Foundations of concurrent Kleene algebra
• From CRL to mCRL2: motivation and outline
• Graphical models of separation logic
• Kleene algebra with domain
• Modeling concurrency with partial orders
• Resources, concurrency, and local reasoning
• Semiring-based constraint satisfaction and optimization
• Synchronous Kleene algebra
• The -calculus: A theory of mobile processes
• The equational theory of pomsets

Cited in

(78)

• A semantics and a logic for \textit{Fuzzy Arden Syntax}
• Mitigating covert channels based on analysis of the potential for communication
• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• Effectful semantics in bicategories: strong, commutative, and concurrent pseudomonads
• Mathematics of Program Construction
• scientific article; zbMATH DE number 7559476 (Why is no real title available?)
• ST-structures
• An event structure model for probabilistic concurrent Kleene algebra
• On weighted Petri net transducers
• On concurrent program algebra and demonic automata
• Brzozowski goes concurrent -- a Kleene theorem for pomset languages
• On the relation between concurrent separation logic and concurrent Kleene algebra
• Probabilistic concurrent Kleene algebra
• Balancing expressiveness in formal approaches to concurrency
• Laws of programming for references
• Algebraic coherent confluence and higher globular Kleene algebras
• Convolution and concurrency
• Concurrent dynamic algebra
• Taming multirelations
• Concurrent Kleene algebra: free model and completeness
• Convolution as a Unifying Concept
• scientific article; zbMATH DE number 7559485 (Why is no real title available?)
• An algebra of synchronous atomic steps
• Concurrent Kleene algebra with tests and branching automata
• Developments in concurrent Kleene algebra
• Reordering Derivatives of Trace Closures of Regular Languages.
• Restructuring a concurrent refinement algebra
• Irrationality of process replication for higher-dimensional automata
• Presenting interval pomsets with interfaces
• Developments in concurrent Kleene algebra
• Concurrent Kleene algebra and its foundations
• Synchronous Kleene algebra
• Concurrent Kleene algebra with observations: from hypotheses to completeness
• On algebra of program correctness and incorrectness
• Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
• On tools for completeness of Kleene algebra with hypotheses
• Observation-based concurrent program logic for relaxed memory consistency models
• A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
• The Boolean algebra of cubical areas as a tensor product in the category of semilattices with zero
• A semantic proof of generalised cut elimination for deep inference
• Weighted synchronous automata
• Proving language inclusion and equivalence by coinduction
• scientific article; zbMATH DE number 7407781 (Why is no real title available?)
• Generalised rely-guarantee concurrency: an algebraic foundation
• Schedulers and finishers: on generating and filtering the behaviours of an event structure
• Schedulers and finishers: on generating the behaviours of an event structure
• Foundations of concurrent Kleene algebra
• On locality and the exchange law for concurrent processes
• An algebraic glimpse at bunched implications and separation logic
• Exploring an interface model for CKA
• A program construction and verification tool for separation logic
• Concurrent Kleene algebra with tests
• Posets with interfaces as a model for concurrency
• Designing a semantic model for a wide-spectrum language with concurrency
• Syllepsis in homotopy type theory
• Cylindric Kleene lattices for program construction
• Completeness and incompleteness of synchronous Kleene algebra
• Concurrent algebras: an algebraic study of a fragment of concurrent propositional dynamic logic
• A discrete geometric model of concurrent program execution
• Generating Posets Beyond N
• Generic models of the laws of programming
• Modal algebra and Petri nets
• scientific article; zbMATH DE number 7204945 (Why is no real title available?)
• Catoids and modal convolution algebras
• Finite relational semantics for language Kleene algebra with complement
• Some uses of modal semirings
• In praise of algebra
• r-multisemigroups, modal quantales and the origin of locality
• Abstract strategies and coherence
• On tools for completeness of Kleene algebra with hypotheses
• Probabilistic rely-guarantee calculus
• On the algebraic structure of Weihrauch degrees
• Specifying and reasoning about shared-variable concurrency
• Completely and partially executable sequences of actions in deontic context
• Modeling quantitative aspects of concurrent systems using weighted Petri net transducers
• Concurrent Kleene Algebra
• Unifying Semantics for Concurrent Programming
• Higher catoids, higher quantales and their correspondences

Describes a project that uses

Uses Software

• Mace4
• Prover9

This page was built for publication: Concurrent Kleene algebra and its foundations

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