On the refinement of liveness properties of distributed systems

DOI10.1007/s10703-011-0117-1zbMath1233.68160arXiv0801.0949OpenAlexW2008807688MaRDI QIDQ763239

Paul C. Attie

Publication date: 9 March 2012

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

Full work available at URL: https://arxiv.org/abs/0801.0949

zbMATH Keywords

automatalivenessrefinementsimulation relationsproof diagrams

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Dynamic input/output automata: a formal and compositional model for dynamic systems

Uses Software

• PVS
• UNITY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The existence of refinement mappings
• Recognizing safety and liveness
• On verifying that a concurrent program satisfies a nondeterministic specification
• Completing the temporal picture
• Proving correctness with respect to nondeterministic safety specifications
• Liveness in timed and untimed systems
• Eventually-serializable data services
• Safety, liveness and fairness in temporal logic
• Hybrid I/O automata.
• Verification by augmented finitary abstraction
• Forward and backward simulations. I. Untimed Systems
• Verification of concurrent programs: The automata-theoretic framework
• Generalized temporal verification diagrams
• Grammar Analysis and Parsing by Abstract Interpretation
• Verifying temporal properties without temporal logic
• Proving Liveness Properties of Concurrent Programs
• Proving the Correctness of Multiprocess Programs
• The Online Transportation Problem
• Verification by augmented abstraction: The automata-theoretic view

This page was built for publication: On the refinement of liveness properties of distributed systems