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
• 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)
• Conditional bigraphs
• 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
• 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
• Interpolation in Grothendieck institutions
• Relating state-based and process-based concurrency through linear logic (full-version)
• Plan in Maude specifying an active network programming language

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)