Finite and infinite implementation of transition systems

DOI10.1016/j.tcs.2012.08.014zbMath1250.68209OpenAlexW2003749264MaRDI QIDQ1758157

Gerard R. Renardel de Lavalette, Wim H. Hesselink

Publication date: 8 November 2012

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

Full work available at URL: https://doi.org/10.1016/j.tcs.2012.08.014

zbMATH Keywords

model checkingimplementationtransition systemKönig's lemmastuttering

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Uses Software

• SPIN

Cites Work

• The existence of refinement mappings
• Forward and backward simulations. I. Untimed Systems
• Eternity variables to prove simulation of specifications