Structured operational semantics and bisimulation as a congruence

DOI10.1016/0890-5401(92)90013-6zbMath0752.68053OpenAlexW1999706742MaRDI QIDQ1198952

Frits W. Vaandrager, Jan Friso Groote

Publication date: 16 January 1993

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://ir.cwi.nl/pub/1495

zbMATH Keywords

transition system specifications full abstraction bisimulation equivalence

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Modelling and analysing neural networks using a hybrid process algebra, Characteristic formulae for fixed-point semantics: a general framework, Proving the validity of equations in GSOS languages using rule-matching bisimilarity, GSOS and finite labelled transition systems, The meaning of negative premises in transition system specifications. II, Rule formats for compositional non-interference properties, Process languages with discrete relative time based on the ordered SOS format and rooted eager bisimulation, Non-strongly Stable Orders Also Define Interesting Simulation Relations, When is partial trace equivalence adequate?, Computable processes and bisimulation equivalence, Towards Bialgebraic Semantics for the Linear Time – Branching Time Spectrum, Compositionality of Hennessy-Milner logic by structural operational semantics, A format for semantic equivalence comparison, Kleene's three-valued logic and process algebra, A syntactic commutativity format for SOS, A complete equational axiomatization for prefix iteration, Operational semantics for Petri net components, A general SOS theory for the specification of probabilistic transition systems, A \(\pi\)-calculus with explicit substitutions, Reversing algebraic process calculi, Unnamed Item, Unnamed Item, Nested semantics over finite trees are equationally hard, A unified rule format for bounded nondeterminism in SOS with terms as labels, SOS formats and meta-theory: 20 years after, Weak Bisimulation as a Congruence in MSOS, Divide and congruence. II: From decomposition of modal formulas to preservation of delay and weak bisimilarity, Congruence from the operator's point of view. Syntactic requirements on modal characterizations, A π-calculus with explicit substitutions: The late semantics, Unnamed Item, A general conservative extension theorem in process algebras with inequalities, An alternative formulation of operational conservativity with binding terms., Compositional equivalences based on open pNets, Lang-n-Send Extended: Sending Regular Expressions to Monitors, Divide and congruence: from decomposition of modal formulas to preservation of branching and \(\eta \)-bisimilarity, Back to the format: a survey on SOS for probabilistic processes, Reactive bisimulation semantics for a process algebra with timeouts, Non-finite axiomatisability results via reductions: CSP parallel composition and CCS restriction, Equivalence checking 40 years after: a review of bisimulation tools, Correcting a Space-Efficient Simulation Algorithm, Rule formats for determinism and idempotence, A Linear-Time–Branching-Time Spectrum of Behavioral Specification Theories, Unnamed Item, Computing branching distances with quantitative games, Unnamed Item, Unnamed Item, Unnamed Item, The quantitative linear-time-branching-time spectrum, The fork calculus, On deciding some equivalences for concurrent processes, Rooted branching bisimulation as a congruence, Structural operational semantics for weak bisimulations, Transition system specifications with negative premises, Rewrite Systems with Constraints, CSP is a retract of CCS, Variable binding operators in transition system specifications, Notions of bisimulation and congruence formats for SOS with data, Behavioral abstraction is hiding information, Ensuring liveness properties of distributed systems: open problems, A precongruence format for should testing preorder, Quantales, finite observations and strong bisimulation, A coalgebraic presentation of structured transition systems, Divide and congruence. III: From decomposition of modal formulas to preservation of stability and divergence, Unnamed Item, Unnamed Item, Observational congruences for dynamically reconfigurable tile systems, From rewrite rules to bisimulation congruences, Explicit substitutions for \(\pi\)-congruences, An axiomatic semantics for Esterel, Barbed bisimulation, A linear-time-branching-time spectrum for behavioral specification theories, Unnamed Item, Equations, Contractions, and Unique Solutions, Structural Operational Semantics with First-Order Logic, Automating Soundness Proofs, Semantics and expressiveness of ordered SOS, Generating priority rewrite systems for OSOS process languages, Action transducers and timed automata, A conservative look at operational semantics with variable binding, A complete equational axiomatization for MPA with string iteration, Finite axiom systems for testing preorder and De Simone process languages, Swinging types=functions+relations+transition systems, Language preorder as a precongruence, Universal coalgebra: A theory of systems, A theory of stochastic systems. II: Process algebra, Discrimination by parallel observers: the algorithm., Tile formats for located and mobile systems., Bisimilarity of open terms., Ordered SOS process languages for branching and eager bisimulations, On Well-Foundedness and Expressiveness of Promoted Tyft, A Congruence Rule Format with Universal Quantification, Dynamic connectors for concurrency, Compositional SOS and beyond: A coalgebraic view of open systems, Denotational fixed-point semantics for constructive scheduling of synchronous concurrency, Final semantics for a higher order concurrent language

Cites Work