Algebraic laws for nondeterminism and concurrency
From MaRDI portal
Publication:3766826
DOI10.1145/2455.2460zbMath0629.68021OpenAlexW1978469611MaRDI QIDQ3766826
Arthur J. Milner, Matthew C. B. Hennessy
Publication date: 1985
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/2455.2460
Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)
Related Items (only showing first 100 items - show all)
CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus ⋮ Coinductive predicates and final sequences in a fibration ⋮ A complete classification of the expressiveness of interval logics of Allen's relations: the general and the dense cases ⋮ Bunched sequential information ⋮ A logic for the specification and proof of regular controllable processes of CCS ⋮ A characterization of finitary bisimulation ⋮ A context dependent equivalence between processes ⋮ Bisimulations and abstraction homomorphisms ⋮ Algebraic solutions to recursion schemes ⋮ Preferential choice and coordination conditions ⋮ A pseudometric in supervisory control of probabilistic discrete event systems ⋮ Two-thirds simulation indexes and modal logic characterization ⋮ Nested semantics over finite trees are equationally hard ⋮ SOS formats and meta-theory: 20 years after ⋮ Type theory and concurrency ⋮ Concurrency and atomicity ⋮ Testing probabilistic equivalence through reinforcement learning ⋮ A fixpoint approach to finite delay and fairness ⋮ A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences ⋮ An observationally complete program logic for imperative higher-order functions ⋮ Temporal BI: proof system, semantics and translations ⋮ Synthesising correct concurrent runtime monitors ⋮ A state/event-based model-checking approach for the analysis of abstract system properties ⋮ Theory of interaction ⋮ An algebra of behavioural types ⋮ Divide and congruence: from decomposition of modal formulas to preservation of branching and \(\eta \)-bisimilarity ⋮ Value-passing CCS with noisy channels ⋮ A calculus and logic of bunched resources and processes ⋮ On intuitionistic modal and tense logics and their classical companion logics: topological semantics and bisimulations ⋮ Combining data type and recursive process specifications using projection algebras ⋮ A refinement calculus for specifications in Hennessy-Milner logic with recursion ⋮ Coalgebraic semantics of modal logics: an overview ⋮ Approximating Markov processes through filtration ⋮ Proof systems for satisfiability in Hennessy-Milner logic with recursion ⋮ A partial ordering semantics for CCS ⋮ A rewriting strategy to verify observational congruence ⋮ CCS expressions, finite state processes, and three problems of equivalence ⋮ First-order reasoning for higher-order concurrency ⋮ Generalizing the Paige-Tarjan algorithm by abstract interpretation ⋮ Lattice-valued simulations for quantitative transition systems ⋮ Domain theory in logical form ⋮ Bisimulation through probabilistic testing ⋮ Specification of communicating processes: temporal logic versus refusals-based refinement ⋮ The equivalence in the DCP model ⋮ Partial specifications and compositional verification ⋮ A modal characterization of alternating approximate bisimilarity ⋮ Local model checking in the modal mu-calculus ⋮ On minimal coalgebras ⋮ Compositional verification of sequential programs with procedures ⋮ Adequacy-preserving transformations of COSY path programs ⋮ Modelling causality via action dependencies in branching time semantics ⋮ A complete axiomatization of timed bisimulation for a class of timed regular behaviours ⋮ Structural operational semantics for weak bisimulations ⋮ Studying equivalences of transition systems with algebraic tools ⋮ Deciding observational congruence of finite-state CCS expressions by rewriting ⋮ Translations between modal logics of reactive systems ⋮ A brief history of Timed CSP ⋮ Observational structures and their logic ⋮ Rough approximations based on bisimulations ⋮ Logical characterizations of simulation and bisimulation for fuzzy transition systems ⋮ Maximally permissive controlled system synthesis for non-determinism and modal logic ⋮ Finitary logics for some CCS observational bisimulations ⋮ Graphical versus logical specifications ⋮ Transition system specifications with negative premises ⋮ Bisimulation and action refinement ⋮ Modal logics for mobile processes ⋮ The expressive power of implicit specifications ⋮ Universal axioms for bisimulations ⋮ Structured operational semantics and bisimulation as a congruence ⋮ Complete sets of axioms for finite basic LOTOS behavioural equivalences ⋮ Refinement of actions in event structures and causal trees ⋮ On bisimulations for description logics ⋮ Automatic verification of distributed systems: the process algebra approach. ⋮ CSP is a retract of CCS ⋮ Differential privacy in probabilistic systems ⋮ Model-checking games for fixpoint logics with partial order models ⋮ Bisimilarity control of partially observed nondeterministic discrete event systems and a test algorithm ⋮ Algebra and logic for access control ⋮ SOS rule formats for zero and unit elements ⋮ On the computational complexity of bisimulation, redux ⋮ Modal logics for communicating systems ⋮ Component simulation-based substitutivity managing QoS and composition issues ⋮ Refusal testing ⋮ Behavioural and abstractor specifications revisited ⋮ Is hyper-extensionality preservable under deletions of graph elements? ⋮ Probabilistic mobile ambients ⋮ (Bi)simulations up-to characterise process semantics ⋮ Bialgebraic methods and modal logic in structural operational semantics ⋮ A complete axiomatisation for observational congruence of finite-state behaviours ⋮ Modal languages and bounded fragments of predicate logic ⋮ Reasoning about nondeterministic and concurrent actions: A process algebra approach ⋮ A behavioural theory of first-order CML ⋮ Non-deterministic data types: Models and implementations ⋮ Specification-oriented semantics for communicating processes ⋮ A logical characterization of observation equivalence ⋮ A complete modal proof system for HAL: the Herbrand agent language ⋮ Priorities in process algebras ⋮ Equivalence notions and model minimization in Markov decision processes ⋮ An efficiency preorder for processes ⋮ Two case studies of semantics execution in Maude: CCS and LOTOS
This page was built for publication: Algebraic laws for nondeterminism and concurrency
