Two case studies of semantics execution in Maude: CCS and LOTOS

DOI10.1007/s10703-005-2254-xzbMath1086.68552OpenAlexW2053342841WikidataQ123905900 ScholiaQ123905900MaRDI QIDQ816216

Alberto Verdejo, Narciso Martí-Oliet

Publication date: 20 February 2006

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-005-2254-x

zbMATH Keywords

rewriting logicCCSMaudeACT ONEexecutable semantic frameworkHennessy-Milner modal logicinternal strategiessymbolic semantics for LOTOS

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Grammars and rewriting systems (68Q42)

Related Items

Rewriting logic: Roadmap and bibliography ⋮ The rewriting logic semantics project ⋮ SOS formats and meta-theory: 20 years after ⋮ The rewriting logic semantics project: a progress report ⋮ Twenty years of rewriting logic ⋮ Strategy based semantics for mobility with time and access permissions ⋮ The Rewriting Logic Semantics Project: A Progress Report ⋮ Maude: specification and programming in rewriting logic ⋮ Two case studies of semantics execution in Maude: CCS and LOTOS

Uses Software

• Coq
• ML
• Isabelle/HOL
• ELAN
• CADP
• HOL
• Maude
• Oz
• LEGO
• XSB
• LOTOSphere

Cites Work

• Symbolic bisimulations
• Two case studies of semantics execution in Maude: CCS and LOTOS
• Conditional rewriting logic as a unified model of concurrency
• \(\pi\)-calculus in (Co)inductive-type theory
• Isabelle/HOL. A proof assistant for higher-order logic
• Maude: specification and programming in rewriting logic
• Reflection in conditional rewriting logic
• Rewriting logic: Roadmap and bibliography
• Formalising a value-passing calculus in H0L
• A First-Order Syntax for the π-Calculus in Isabelle/HOL using Permutations
• Algebraic laws for nondeterminism and concurrency
• Tabled evaluation with delaying for general logic programs
• Generic tools for verifying concurrent systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item