Conditional rewriting logic as a unified model of concurrency

DOI10.1016/0304-3975(92)90182-FzbMATH Open0758.68043WikidataQ125052689 ScholiaQ125052689MaRDI QIDQ1190488FDOQ1190488

Authors: José Meseguer 

Publication date: 26 September 1992

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

Recommendations

• Conditional rewriting logic: Deduction, models and concurrency
• scientific article; zbMATH DE number 1615226
• Semantic foundations for generalized rewrite theories
• Rewriting logic as a semantic framework for concurrency: a progress report
• Twenty years of rewriting logic

zbMATH Keywords

deductionrewriting logicconcurrent systemsinitial model

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Models of other mathematical theories (03C65) Other applications of logic (03B80)

Cites Work

• Title not available (Why is that?)
• Varieties of ordered algebras
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Initial Algebra Semantics and Continuous Algebras
• Title not available (Why is that?)
• Title not available (Why is that?)
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Adjointness in Foundations
• Aspects of topoi
• Title not available (Why is that?)
• Title not available (Why is that?)
• Petri nets are monoids
• Title not available (Why is that?)
• Computing in systems described by equations
• Title not available (Why is that?)
• The gamma model and its discipline of programming
• Completion of a Set of Rules Modulo a Set of Equations
• The linear abstract machine
• From Petri nets to linear logic
• Title not available (Why is that?)
• Termination for direct sums of left-linear complete term rewriting systems
• Algebraic semantics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Concurrent transition systems
• Title not available (Why is that?)
• Graph expressions and graph rewritings
• On ``On graph rewritings
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Infinite trees in normal form and recursive equations having a unique solution
• Implementing term rewriting by graph reduction: Termination of combined systems
• On graph rewritings
• General recursive functions of natural numbers
• Title not available (Why is that?)
• Actor grammars
• Title not available (Why is that?)
• Title not available (Why is that?)
• Fair termination is decidable for ground systems
• The categorical abstract machine
• A mathematical approach to nondeterminism in data types
• Varieties of chain-complete algebras
• Subequalizers
• Title not available (Why is that?)
• Title not available (Why is that?)
• An abstract formulation for rewrite systems
• Operational and Semantic Equivalence Between Recursive Programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Compiling concurrent rewriting onto the Rewrite Rule Machine

Cited In (only showing first 100 items - show all)

• Backwards type analysis of asynchronous method calls
• A Modular Equational Generalization Algorithm
• Strict coherence of conditional rewriting modulo axioms
• Specification of abstract dynamic-data types: A temporal logic approach
• Equational formulas and pattern operations in initial order-sorted algebras
• Dynamic connectors for concurrency
• Reflection in conditional rewriting logic
• Structural induction in institutions
• Tile formats for located and mobile systems.
• Algebraic specification of agent computation
• Structured theories and institutions
• Priority rewriting: Semantics, confluence, and conditionals
• Formalization and correctness of the PALS architectural pattern for distributed real-time systems
• Rewriting semantics of production rule sets
• Specification and analysis of the AER/NCA active network protocol suite in real-time Maude
• Theorem proving in a mathematical information environment
• Title not available (Why is that?)
• REWRITING WITH STRATEGIES IN $\mathsf{ELAN}$: A FUNCTIONAL SEMANTICS
• Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
• Modeling and analyzing mobile ad hoc networks in Real-Time Maude
• More problems in rewriting
• Title not available (Why is that?)
• Applications and extensions of context-sensitive rewriting
• A new generic scheme for functional logic programming with constraints
• Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types
• Debugging Maude programs via runtime assertion checking and trace slicing
• Invariant-driven specifications in Maude
• Comparing logics for rewriting: Rewriting logic, action calculi and tile logic
• Foundations of the rule-based system \(\rho\,\text{Log}\)
• Solving Sudoku puzzles with rewriting rules
• Concurrent garbage collection for concurrent rewriting
• Compositional reasoning about active objects with shared futures
• Strategy based semantics for mobility with time and access permissions
• A rewriting based model for probabilistic distributed object systems.
• Toward the concurrent implementation of computational systems
• A semantics preserving actor translation
• An abstract machine for concurrent modular systems: CHARM
• Knuth-Bendix completion for non-symmetric transitive relations
• A causal semantics for CCS via rewriting logic
• Title not available (Why is that?)
• A formal framework for interactive agents
• Combining runtime checking and slicing to improve Maude error diagnosis
• From rewriting logic, to programming language semantics, to program verification
• Replicated data types that unify eventual consistency and observable atomic consistency
• Executable rewriting logic semantics of Orc and formal analysis of Orc programs
• On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
• Title not available (Why is that?)
• Comparing Meseguer's rewriting logic with the logic CRWL
• Verifying a distributed list system: A case history
• A probabilistic approximate logic for neuro-symbolic learning and reasoning
• CINNI -- a generic calculus of explicit substitutions and its application to \(\lambda\)-, \(\sigma\)- and \(\pi\)-calculi
• Termination of just/fair computations in term rewriting
• Parallel dynamic semantics of sequential programs with speculative and incremental computation
• A Non-Deterministic Multiset Query Language
• Deciding observational congruence of finite-state CCS expressions by rewriting
• Categorical rewriting of term-like structures
• Compositional specification in rewriting logic
• The rewriting logic semantics project: a progress report
• The rewriting logic semantics project: a progress report
• Twenty years of rewriting logic
• An Object-Oriented Component Model for Heterogeneous Nets
• A rewriting framework and logic for activities subject to regulations
• Strategy-based rewrite semantics for membrane systems preserves maximal concurrency of evolution rule actions
• Confluence by critical pair analysis revisited
• Composing proof terms
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• Two case studies of semantics execution in Maude: CCS and LOTOS
• The rewriting logic semantics project
• Herbrand theorems in arbitrary institutions
• Rewriting logic as a semantic framework for concurrency: a progress report
• An algebraic semantics for MOF
• Effectively Checking the Finite Variant Property
• A rewriting logic approach to operational semantics
• A rewriting logic framework for soft constraints
• A foundation for higher-order concurrent constraint programming
• Semantic foundations for generalized rewrite theories
• SOS formats and meta-theory: 20 years after
• Rewriting strategies and strategic rewrite programs
• The Maude LTL model checker
• Declarative Debugging of Rewriting Logic Specifications
• Tiles for Reo
• A rewriting-based model checker for the linear temporal logic of rewriting
• Verifying hierarchical Ptolemy II discrete-event models using real-time maude
• Specification of real-time and hybrid systems in rewriting logic
• Logical foundations of CafeOBJ
• Formal modeling and validation of a power-efficient grouping protocol for WSNs
• Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
• Coinduction for preordered algebra
• Executable structural operational semantics in Maude
• Deduction, strategies, and rewriting
• Weak bisimulation as a congruence in MSOS
• A generic framework for \(n\)-protocol compatibility checking
• Bisimilarity of open terms.
• Assertion-based analysis via slicing withABETS(system description)
• Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude
• Integrating Maude into Hets
• Quasi-Boolean encodings and conditionals in algebraic specification
• Collaborative planning with confidentiality
• A basic algebra of stateless connectors
• Specification and proof in membership equational logic

Uses Software

• OBJ3
• Maude
• UNITY
• Simula 67

This page was built for publication: Conditional rewriting logic as a unified model of concurrency

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