UNITY and Büchi automata

DOI10.1007/s00165-020-00528-xOpenAlexW3126386092MaRDI QIDQ2026375

Wim H. Hesselink

Publication date: 19 May 2021

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-020-00528-x

zbMATH Keywords

progressconcurrencyUNITYBüchi automatonLTL

Mathematics Subject Classification ID

Computer science (68-XX)

Uses Software

• SPIN
• UNITY

Cites Work

• The existence of refinement mappings
• A predicate transformer for the progress property `to-always'
• A foundation for modular reasoning about safety and progress properties of state-based concurrent programs
• Computation calculus bridging a formalization gap
• Predicate transformers for reasoning about concurrent computation
• DUALITY: A simple formalism for the analysis of UNITY
• Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
• Distributed cooperation with action systems
• Programs, Recursion and Unbounded Choice
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item