UNITY and Büchi automata

DOI10.1007/S00165-020-00528-XMaRDI QIDQ2026375zbMATH OpenOpenAlexFDO

Authors W. H. Hesselink

Publication date 19 May 2021

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

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

Büchi automatonconcurrencyLTLprogressUNITY

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• On the logic of UNITY
• scientific article; zbMATH DE number 2077135
• Logical foundations for compositional verification and development of concurrent programs in UNITY
• A simple proof of a completeness result for \(leads\)-\(to\) in the UNITY logic
• scientific article; zbMATH DE number 15894

Cites work

• A foundation for modular reasoning about safety and progress properties of state-based concurrent programs
• A predicate transformer for the progress property `to-always'
• Computation calculus bridging a formalization gap
• Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
• Distributed cooperation with action systems
• DUALITY: A simple formalism for the analysis of UNITY
• scientific article; zbMATH DE number 1639446 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 2077135 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 3237829 (Why is no real title available?)
• Predicate transformers for reasoning about concurrent computation
• Programs, Recursion and Unbounded Choice
• The existence of refinement mappings

Cited in

(3)

• Unambiguous Büchi automata.
• scientific article; zbMATH DE number 2077135 (Why is no real title available?)
• Unity properties and sequences of states, some observations

Describes a project that uses

Uses Software

• UNITY
• SPIN

This page was built for publication: UNITY and Büchi automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2026375)