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)

• 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
• Algebraic simulations
• Partial order reduction for rewriting semantics of programming languages
• A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties
• Formal analysis of Kerberos 5
• Order-sorted generalization
• Integrating deployment architectures and resource consumption in timed object-oriented models
• State space reduction in the Maude-NRL protocol analyzer
• A Rewriting Logic Approach to Type Inference
• Actor languages. Their syntax, semantics, translation, and equivalence
• A hidden agenda
• ELAN from a rewriting logic point of view
• Equational abstractions
• Exploring conditional rewriting logic computations
• Rewriting modulo SMT and open system analysis
• A declarative debugger for Maude functional modules
• Defining and Executing P Systems with Structured Data in K
• Bigraphs and their algebra
• Comparing three coordination models: Reo, ARC, and PBRD
• An overview of the K semantic framework
• Variant narrowing and equational unification
• Normal forms and normal theories in conditional rewriting
• Saturated models in institutions
• A formal library of set relations and its application to synchronous languages
• Creol: A type-safe object-oriented model for distributed concurrent systems
• Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• Maude: specification and programming in rewriting logic
• Equational abstractions for reducing the state space of rewrite theories
• Formal methods for web security
• Abstract Beth definability in institutions
• Relating state-based and process-based concurrency through linear logic
• Rewriting logic: Roadmap and bibliography
• Relating CASL with other specification languages: the institution level.
• A Maude environment for CafeOBJ
• ACUOS: a system for modular ACU generalization with subtyping and inheritance
• Equational rules for rewriting logic
• Inspecting rewriting logic computations (in a parametric and stepwise way)
• Title not available (Why is that?)
• Declarative debugging of rewriting logic specifications
• Validating timed models of deployment components with parametric concurrency
• Travelling salesman problem in tissue P systems with costs
• 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

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)