Conditional rewriting logic as a unified model of concurrency

From MaRDI portal

Publication:1190488

Jump to:navigation, search

DOI10.1016/0304-3975(92)90182-FzbMath0758.68043WikidataQ125052689 ScholiaQ125052689MaRDI QIDQ1190488

José Meseguer

Publication date: 26 September 1992

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

zbMATH Keywords

concurrent systems deduction rewriting logic initial model

Mathematics Subject Classification ID

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

Related Items

Rewriting logic: Roadmap and bibliography, Structured theories and institutions, Interpolation in Grothendieck institutions, Invariant-driven specifications in Maude, Algebraic simulations, Quasi-Boolean encodings and conditionals in algebraic specification, Verifying a distributed list system: A case history, Creol: A type-safe object-oriented model for distributed concurrent systems, Parallel dynamic semantics of sequential programs with speculative and incremental computation, A basic algebra of stateless connectors, Formal analysis of Kerberos 5, A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties, Specification and analysis of the AER/NCA active network protocol suite in real-time Maude, Rewriting modulo SMT and open system analysis, Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic, The rewriting logic semantics project, SOS formats and meta-theory: 20 years after, Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, 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, Comparing three coordination models: Reo, ARC, and PBRD, The rewriting logic semantics project: a progress report, Specification of abstract dynamic-data types: A temporal logic approach, Parameterized strategies specification in Maude, Twenty years of rewriting logic, Declarative debugging of rewriting logic specifications, Rewriting semantics of production rule sets, Strategy based semantics for mobility with time and access permissions, Compositional reasoning about active objects with shared futures, Coinduction for preordered algebra, A generic framework for \(n\)-protocol compatibility checking, Verifying hierarchical Ptolemy II discrete-event models using real-time maude, Formal modeling and validation of a power-efficient grouping protocol for WSNs, Efficient safety enforcement for Maude programs via program specialization in the \textsf{ÁTAME} system, State space reduction in the Maude-NRL protocol analyzer, Termination of just/fair computations in term rewriting, A formal library of set relations and its application to synchronous languages, Integrating deployment architectures and resource consumption in timed object-oriented models, Elimination of conditions, Exploring conditional rewriting logic computations, Specification and proof in membership equational logic, Equational abstractions, Travelling salesman problem in tissue P systems with costs, Deciding observational congruence of finite-state CCS expressions by rewriting, Strategies, model checking and branching-time properties in Maude, Resource provisioning strategies for BPMN processes: specification and analysis using Maude, Formal methods for web security, Backwards type analysis of asynchronous method calls, Strict coherence of conditional rewriting modulo axioms, A Maude environment for CafeOBJ, A compositional view of derivations as interactive processes with applications to regulated and distributed rewriting, Collaborative planning with confidentiality, An algebraic semantics for MOF, Formalization and correctness of the PALS architectural pattern for distributed real-time systems, An overview of the K semantic framework, Structural induction in institutions, Observational congruences for dynamically reconfigurable tile systems, A process calculus BigrTiMo of mobile systems and its formal semantics, Saturated models in institutions, Modeling and analyzing mobile ad hoc networks in Real-Time Maude, Normal forms and normal theories in conditional rewriting, Relating state-based and process-based concurrency through linear logic (full-version), Proving semantic properties as first-order satisfiability, Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude, Programming and symbolic computation in Maude, A partial evaluation framework for order-sorted equational programs modulo axioms, Formal verification of complex business processes based on high-level Petri nets, Applications and extensions of context-sensitive rewriting, Debugging Maude programs via runtime assertion checking and trace slicing, Transactions and contracts based on reaction systems, A rewriting logic approach to operational semantics, Concurrent semantics for fusions: weak prime domains and connected event structures, Confluence by critical pair analysis revisited, Composing proof terms, Theorem proving in a mathematical information environment, A hidden agenda, Actor languages. Their syntax, semantics, translation, and equivalence, Replicated data types that unify eventual consistency and observable atomic consistency, Read atomic transactions with prevention of lost updates: ROLA and its formal analysis, A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems, Capturing constrained constructor patterns in matching logic, Relating CASL with other specification languages: the institution level., Relaxed models for rewriting logic, Tile formats for located and mobile systems., Bisimilarity of open terms., An abstract machine for concurrent modular systems: CHARM, Dynamic connectors for concurrency, A causal semantics for CCS via rewriting logic, ELAN from a rewriting logic point of view, Maude: specification and programming in rewriting logic, Reflection in conditional rewriting logic, Logical foundations of CafeOBJ, Comparing logics for rewriting: Rewriting logic, action calculi and tile logic, Specification of real-time and hybrid systems in rewriting logic, A Maude specification of an object-oriented model for telecommunication networks, Actor theories in rewriting logic, Equational rules for rewriting logic, Algebraic specification of agent computation, Two case studies of semantics execution in Maude: CCS and LOTOS, Symbolic computation in Maude: some tapas, Algorithmic Analysis of Blockchain Efficiency with Communication Delay, An Institution for Graph Transformation, True concurrency semantics for a linear logic programming language with broadcast communication, Executable structural operational semantics in Maude, Unnamed Item, Equational formulas and pattern operations in initial order-sorted algebras, Ultraproducts and possible worlds semantics in institutions, Probabilistic Real-Time Rewrite Theories and Their Expressive Power, Towards Erlang Verification by Term Rewriting, Bi-rewriting, a term rewriting technique for monotonic order relations, More problems in rewriting, Concurrent garbage collection for concurrent rewriting, Relating two categorical models of term rewriting, Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories, Tiles for Reo, A Rewriting Logic Approach to Type Inference, Declarative Debugging of Rewriting Logic Specifications, Converting between Combinatory Reduction Systems and Big Step Semantics, Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties, Herbrand theorems in arbitrary institutions, A semantics preserving actor translation, ACUOS: A System for Modular ACU Generalization with Subtyping and Inheritance, A probabilistic approximate logic for neuro-symbolic learning and reasoning, Simulating and model checking membrane systems using strategies in Maude, Metalevel transformation of strategies, Optimization of rewrite theories by equational partial evaluation, A Distributed Computing Model for Dataflow, Controlflow, and Workflow in Fractionated Cyber-Physical Systems, José Meseguer: Scientist and Friend Extraordinaire, Combining Runtime Checking and Slicing to Improve Maude Error Diagnosis, Two Decades of Maude, Rewriting Strategies and Strategic Rewrite Programs, Verifying Reachability-Logic Properties on Rewriting-Logic Specifications, Weak Bisimulation as a Congruence in MSOS, From Rewriting Logic, to Programming Language Semantics, to Program Verification, On relating rewriting systems and graph grammars to event structures, A foundation for higher-order concurrent constraint programming, CPO models for infinite term rewriting, Conditional Bigraphs, Assertion-based analysis via slicing withABETS(system description), Symbolic Analysis of Maude Theories with Narval, Compositional Specification in Rewriting Logic, Declarative Debugging of Membership Equational Logic Specifications, Models of Computation: A Tribute to Ugo Montanari’s Vision, Safety enforcement via programmable strategies in Maude, Verification of the ROS NavFn planner using executable specification languages, Effectively Checking the Finite Variant Property, A rewriting framework and logic for activities subject to regulations, Algebraic structures of directed acyclic graphs: application to concurrent calculus, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting, Relating State-Based and Process-Based Concurrency through Linear Logic, Strategy-Based Rewrite Semantics for Membrane Systems Preserves Maximal Concurrency of Evolution Rule Actions, An Assertional Language for the Verification of Systems Parametric in Several Dimensions, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Representation and Execution of Petri Nets Using Rewriting Logic as a Unifying Framework, Categorical rewriting of term-like structures, Unnamed Item, Rewriting on cyclic structures: Equivalence between the operational and the categorical description, Semantic foundations for generalized rewrite theories, An Object-Oriented Component Model for Heterogeneous Nets, Unnamed Item, Integrating Maude into Hets, Validating Timed Models of Deployment Components with Parametric Concurrency, A Modular Equational Generalization Algorithm, The Rewriting Logic Semantics Project: A Progress Report, Axiomatizing permutation equivalence, A Connector Algebra for P/T Nets Interactions, TAGED Approximations for Temporal Properties Model-Checking, Egalitarian State-Transition Systems, Order-Sorted Generalization, Foundations of the rule-based system ρLog, Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*, Abstract Beth definability in institutions, Certifying Term Rewriting Proofs in ELAN, Knuth-Bendix Completion for Non-Symmetric Transitive Relations, Comparing Higher-Order Encodings in Logical Frameworks and Tile Logic, Comparing cospan-spans and tiles via a Hoare-style process calculus, Comparing Meseguer's Rewriting Logic with the Logic CRWL, Behavioural specification for hierarchical object composition, Deduction, Strategies, and Rewriting, A Formal Framework for Interactive Agents, Semantic Determinism and Functional Logic Program Properties, Using Maude and Its Strategies for Defining a Framework for Analyzing Eden Semantics, Bigraphs and Their Algebra, Executable rewriting logic semantics of Orc and formal analysis of Orc programs, A Rewriting Logic Approach to Operational Semantics (Extended Abstract), Partial Order Reduction for Rewriting Semantics of Programming Languages, Solving Sudoku Puzzles with Rewriting Rules, Abstraction and Model Checking of Core Erlang Programs in Maude, A Rewriting Logic Framework for Soft Constraints, Narrowing and Rewriting Logic: from Foundations to Applications, Detection and diagnosis of deviations in distributed systems of autonomous agents, An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis, Symbolic Specialization of Rewriting Logic Theories with Presto, Rewriting logic as a semantic framework for concurrency: a progress report, Variants and satisfiability in the infinitary unification wonderland, The Maude strategy language, Modular rewritable Petri nets: an efficient model for dynamic distributed systems, Business processes resource management using rewriting logic and deep-learning-based predictive monitoring, Variant-based equational anti-unification, Canonization of reconfigurable PT nets in \texttt{Maude}, Optimizing Maude programs via program specialization, Strand spaces with choice via a process algebra semantics, Towards Modelling Actor-Based Concurrency in Term Rewriting, Unnamed Item, Model Checking TLR* Guarantee Formulas on Infinite Systems, Inspecting Rewriting Logic Computations (in a Parametric and Stepwise Way), Functional Logic Programming in Maude, Partially Ordered Knowledge Sharing and Fractionated Systems in the Context of other Models for Distributed Computing, Memory Policy Analysis for Semantics Specifications in Maude, Strategy-Based Proof Calculus for Membrane Systems, A Declarative Debugger for Maude Functional Modules, Variant Narrowing and Equational Unification, Equational Abstractions for Reducing the State Space of Rewrite Theories, Proof Search for the First-Order Connection Calculus in Maude, A Rewriting Semantics for Maude Strategies, Combining Techniques to Reduce State Space and Prove Strong Properties, Defining and Executing P Systems with Structured Data in K, REWRITING WITH STRATEGIES IN $\mathsf{ELAN}$: A FUNCTIONAL SEMANTICS, Testing Concurrent Objects with Application-Specific Schedulers, A White Box Perspective on Behavioural Adaptation, A Non-Deterministic Multiset Query Language

Uses Software

Cites Work

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Publication:1190488&oldid=13247113"