Modal logics for communicating systems

DOI10.1016/0304-3975(87)90012-0zbMath0624.68019OpenAlexW2036996017MaRDI QIDQ578896

Colin Stirling

Publication date: 1987

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(87)90012-0

zbMATH Keywords

modal logiccompletenessbisimulationconcurrencytransition systemssoundnessGentzen-like introductions rulesHennessy- Milner logicprogram combinatorsproof systems for SCCS and CCS

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Theory of operating systems (68N25)

Related Items (34)

Characteristic formulae for fixed-point semantics: a general framework ⋮ Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS ⋮ Termination, deadlock and divergence ⋮ Compositionality of Hennessy-Milner logic by structural operational semantics ⋮ A modal logic for message passing processes ⋮ Extension of synthesis algorithm of recursive processes to \(\mu\)-calculus ⋮ Extending modal transition systems with structured labels ⋮ A domain equation for bisimulation ⋮ Honesty in partial logic ⋮ Duality for modal \(\mu\)-logics ⋮ Reasoning about higher-order processes ⋮ Proof systems for satisfiability in Hennessy-Milner logic with recursion ⋮ Mathematical modal logic: A view of its evolution ⋮ Generating diagnostic information for behavioral preorders ⋮ Domain theory in logical form ⋮ Correctness of concurrent processes ⋮ Local model checking in the modal mu-calculus ⋮ Games for the \(\mu\)-calculus ⋮ Local model checking for infinite state spaces ⋮ Graphical versus logical specifications ⋮ Observing localities ⋮ Using typed lambda calculus to implement formal systems on a machine ⋮ A fully abstract denotational model for observational precongruence ⋮ A fully abstract denotational semantics for the calculus of higher-order communicating systems ⋮ Refusal testing ⋮ Models and logics for true concurrency. ⋮ A general method for proving decidability of intuitionistic modal logics ⋮ Bisimulation and divergence ⋮ Intuitionistic Layered Graph Logic ⋮ Full abstractness for a functional/concurrent language with higher-order value-passing ⋮ A Logical Process Calculus ⋮ Synthesis of Data Views for Communicating Processes ⋮ Inductive synthesis of recursive processes from logical properties ⋮ A complete modal proof system for HAL: the Herbrand agent language

Cites Work

• A fair calculus of communicating systems
• Calculi for synchrony and asynchrony
• Axiomatising finite delay operators
• Specification-oriented semantics for communicating processes
• A calculus of communicating systems
• A unified approach for studying the properties of transition systems
• Fairness and related properties in transition systems - a temporal logic to deal with fairness
• First-order dynamic logic
• Testing equivalences for processes
• The power of the future perfect in program logics
• A logic for the description of non-deterministic programs and their properties
• A Theory of Communicating Sequential Processes
• Algebraic laws for nondeterminism and concurrency
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Modal logics for communicating systems