Algebraic simulations

DOI10.1016/j.jlap.2009.07.003zbMath1184.68300OpenAlexW4212970249WikidataQ123905842 ScholiaQ123905842MaRDI QIDQ844884

Miguel Palomino, Narciso Martí-Oliet, José Meseguer

Publication date: 5 February 2010

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2009.07.003

zbMATH Keywords

model checkingKripke structuresrewriting logicrepresentability resultsstuttering simulations

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42) Logic programming (68N17) Temporal logic (03B44)

Related Items

ASM-based formal design of an adaptivity component for a cloud system ⋮ Amalgamation of domain specific languages with behaviour ⋮ José Meseguer: Scientist and Friend Extraordinaire ⋮ Model-Checking Helena Ensembles with Spin ⋮ Verifying Reachability-Logic Properties on Rewriting-Logic Specifications ⋮ Twenty years of rewriting logic ⋮ On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories ⋮ Equational Abstractions in Rewriting Logic and Maude

Uses Software

• CafeOBJ
• Maude
• CESAR
• ITP

Cites Work

• Equational abstractions
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Characterizing finite Kripke structures in propositional temporal logic
• Conditional rewriting logic as a unified model of concurrency
• Property preserving abstractions for the verification of concurrent systems
• Automated deduction -- CADE-19. 19th international conference on automated deduction, Miami Beach, FL, USA, July 28 -- August 2, 2003. Proceedings
• ELAN from a rewriting logic point of view
• Maude: specification and programming in rewriting logic
• Equational rules for rewriting logic
• Rewriting logic: Roadmap and bibliography
• Handbook of philosophical logic. Vol. 9
• Forward and backward simulations. I. Untimed Systems
• Specification and proof in membership equational logic
• Semantic foundations for generalized rewrite theories
• On degrees of unsolvability
• The Temporal Logic of Rewriting: A Gentle Introduction
• Algebra and Coalgebra in Computer Science
• Term Rewriting and Applications
• Recent Trends in Algebraic Development Techniques
• Correct Hardware Design and Verification Methods
• 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
• Unnamed Item