Algebraic laws for nondeterminism and concurrency
From MaRDI portal
Publication:3766826
DOI10.1145/2455.2460zbMath0629.68021MaRDI QIDQ3766826
Matthew C. B. Hennessy, Arthur J. Milner
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
68Q60: Specification and verification (program logics, model checking, etc.)
68N25: Theory of operating systems
Related Items
Modal logics for communicating systems, Refusal testing, Nested semantics over finite trees are equationally hard, 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, 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, Refinement of actions in event structures and causal trees, On the computational complexity of bisimulation, redux, A logical characterization of observation equivalence, Priorities in process algebras, Equivalence notions and model minimization in Markov decision processes, Two case studies of semantics execution in Maude: CCS and LOTOS, Preferential choice and coordination conditions, SOS formats and meta-theory: 20 years after, Combining data type and recursive process specifications using projection algebras, A refinement calculus for specifications in Hennessy-Milner logic with recursion, 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, Generalizing the Paige-Tarjan algorithm by abstract interpretation, Specification of communicating processes: temporal logic versus refusals-based refinement, On minimal coalgebras, Compositional verification of sequential programs with procedures, Automatic verification of distributed systems: the process algebra approach., Probabilistic mobile ambients, Non-deterministic data types: Models and implementations, Specification-oriented semantics for communicating processes, A logic for the specification and proof of regular controllable processes of CCS, A context dependent equivalence between processes, Bisimulations and abstraction homomorphisms, Algebraic solutions to recursion schemes, Type theory and concurrency, Concurrency and atomicity, A fixpoint approach to finite delay and fairness, Domain theory in logical form, Bisimulation through probabilistic testing, The equivalence in the DCP model, Partial specifications and compositional verification, Local model checking in the modal mu-calculus, Adequacy-preserving transformations of COSY path programs, Observational structures and their logic, Finitary logics for some CCS observational bisimulations, Structured operational semantics and bisimulation as a congruence, Complete sets of axioms for finite basic LOTOS behavioural equivalences, 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, A complete modal proof system for HAL: the Herbrand agent language, An efficiency preorder for processes, CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus, Model checking for action-based logics, Assisting requirement formalization by means of natural language translation, A theory of processes with localities, GSOS and finite labelled transition systems, Simple proof techniques for property preservation via simulation, On the operational semantics of nondeterminism and divergence, A \(\pi\)-calculus with explicit substitutions, An algebraic characterization of observational equivalence, Semantics for finite delay, Bisimulation congruence of \(\chi\)-calculus, An alternative formulation of operational conservativity with binding terms., Undecidable problems in unreliable computations., Undecidability of domino games and hhp-bisimilarity., Observational ultraproducts of polynomial coalgebras., Mathematical modal logic: A view of its evolution, Domain theory for concurrency, Swinging types=functions+relations+transition systems, Analysis of equivalence relations of event structures with continuous time, Impossible futures and determinism, CCS with Hennessy's merge has no finite-equational axiomatization, Weak and strong fairness in CCS, Bisimulation of automata, An algebraic characterization of transition system equivalences, Toward an infinitary logic of domains: Abramsky logic for transition systems, Inductive synthesis of recursive processes from logical properties, Corrigendum: ``A domain equation for bisimulation by S. Abramsky, Is your model checker on time? On the complexity of model checking for timed modal logics, Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS, A spatial logic for concurrency. II, Tau laws for pi calculus, Branching time and orthogonal bisimulation equivalence, Applicability of fair simulation, A spatial logic for concurrency. I, Logic of transition systems, Models of nondeterministic regular expressions, Testing equivalence as a bisimulation equivalence, On the universal and existential fragments of the \(\mu\)-calculus, Compositionality of Hennessy-Milner logic by structural operational semantics, Quantales, observational logic and process semantics, The Range of Modal Logic, Australasian Association for Logic George Hughes Memorial Conference, A logical analysis of aliasing in imperative higher-order functions, On the axiomatisability of priority, A survey of modal logics characterising behavioural equivalences for non-deterministic and stochastic systems, Multiple-Labelled Transition Systems for nominal calculi and their logics, Efficient and Expressive Tree Filters, Minimal refinements of specifications in modal and temporal logics, Minimal refinements of specifications in modal and temporal logics, Quantales, finite observations and strong bisimulation, A fully abstract denotational semantics for the calculus of higher-order communicating systems, Models and logics for true concurrency., Explicit substitutions for \(\pi\)-congruences, Executable structural operational semantics in Maude, Operational semantics for Petri net components, Ultraproducts and possible worlds semantics in institutions, Priority and abstraction in process algebra, Deciding orthogonal bisimulation, Expressivity of coalgebraic modal logic: the limits and beyond, ACTLW -- an action-based computation tree logic with unless operator, Bisimulation relations for weighted automata, A parametric analysis of the state-explosion problem in model checking, Splitting bisimulations and retrospective conditions, A modal proof theory for final polynomial coalgebras, Approximating and computing behavioural distances in probabilistic transition systems, Probabilistic temporal logics via the modal mu-calculus, Final coalgebras and the Hennessy-Milner property, A domain equation for bisimulation, A finite model construction for coalgebraic modal logic, Characteristic Formulae for Timed Automata, Twenty Years on: Reflections on the CEDISYS Project. Combining True Concurrency with Process Algebra, Branching vs. Linear Time: Semantical Perspective, Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains, A Complete Axiomatic System for a Process-Based Spatial Logic, Decidable Extensions of Hennessy-Milner Logic, Logics and Bisimulation Games for Concurrency, Causality and Conflict, Functions as processes, Unnamed Item
