Relational concurrent refinement. III: Traces, partial relations and automata
DOI10.1007/s00165-012-0262-3zbMath1342.68227OpenAlexW2151604085MaRDI QIDQ736917
Publication date: 5 August 2016
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-012-0262-3
extensionsimulationsZconcurrencytracesdata refinementfailuresautomata-based refinementscompletedfailure traces
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Uses Software
Cites Work
- 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
- Incompleteness of relational simulations in the blocking paradigm
- A process algebraic view of input/output automata
- Relational concurrent refinement
- Data refinement and singleton failures refinement are not equivalent
- Relational concurrent refinement. II: Internal operations and outputs
- Extensional equivalences for transition systems
- A state-based approach to communicating processes
- Quiescence, fairness, testing, and the notion of implementation
- Forward and backward simulations. I. Untimed Systems
- A singleton failures semantics for communicating sequential processes
- Modelling Divergence in Relational Concurrent Refinement
- Proving Linearizability Via Non-atomic Refinement
- Data Refinement
- More Relational Concurrent Refinement: Traces and Partial Relations
- ZB 2005: Formal Specification and Development in Z and B
This page was built for publication: Relational concurrent refinement. III: Traces, partial relations and automata
