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)

• Travelling salesman problem in tissue P systems with costs
• Order-sorted homeomorphic embedding modulo combinations of associativity and/or commutativity axioms
• Towards Erlang verification by term rewriting
• Symbolic computation in Maude: some tapas
• A partial evaluation framework for order-sorted equational programs modulo axioms
• Read atomic transactions with prevention of lost updates: ROLA and its formal analysis
• A compositional view of derivations as interactive processes with applications to regulated and distributed rewriting
• A Maude specification of an object-oriented model for telecommunication networks
• Actor theories in rewriting logic
• Model checking TLR* guarantee formulas on infinite systems
• Efficient safety enforcement for Maude programs via program specialization in the \textsf{ÁTAME} system
• Relaxed models for rewriting logic
• Formal verification of complex business processes based on high-level Petri nets
• A connector algebra for P/T nets interactions
• A Distributed Computing Model for Dataflow, Controlflow, and Workflow in Fractionated Cyber-Physical Systems
• Resource provisioning strategies for BPMN processes: specification and analysis using Maude
• Conditional Bigraphs
• Formal Methods in Software and Systems Modeling
• A process calculus BigrTiMo of mobile systems and its formal semantics
• Strategy-based proof calculus for membrane systems
• Strategies, model checking and branching-time properties in Maude
• Abstraction and model checking of core Erlang programs in Maude
• Comparing higher-order encodings in logical frameworks and tile logic
• Tiling transactions in rewriting logic
• Narrowing and rewriting logic: from foundations to applications
• Models of Computation: A Tribute to Ugo Montanari’s Vision
• Observational congruences for dynamically reconfigurable tile systems
• Transactions and contracts based on reaction systems
• True concurrency semantics for a linear logic programming language with broadcast communication
• Representation and Execution of Petri Nets Using Rewriting Logic as a Unifying Framework
• Parameterized strategies specification in Maude
• A rewriting semantics for Maude strategies
• Programming and symbolic computation in Maude
• Functional logic programming in Maude
• Concurrent semantics for fusions: weak prime domains and connected event structures
• An assertional language for the verification of systems parametric in several dimensions (preliminary results)
• Proving semantic properties as first-order satisfiability
• Axiomatizing permutation equivalence
• Relating two categorical models of term rewriting
• Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
• CPO models for infinite term rewriting
• Title not available (Why is that?)
• Ultraproducts and possible worlds semantics in institutions
• On relating rewriting systems and graph grammars to event structures
• Title not available (Why is that?)
• Bi-rewriting, a term rewriting technique for monotonic order relations
• Checking Sufficient Completeness by Inductive Theorem Proving
• Two Decades of Maude
• Using Maude and its strategies for defining a framework for analyzing Eden semantics
• Declarative Debugging of Membership Equational Logic Specifications
• Elimination of conditions
• Conditional rewriting logic: Deduction, models and concurrency
• A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems
• Capturing constrained constructor patterns in matching logic
• 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

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)