Title: Analysis and Checking of Multi-Actor Liveness Rules from Fairness
Abstract:Liveness properties are important in model checking. We put forward multi-actor liveness rules based on Lesilie Lamport's TLA (temporal logic of actions) and liveness rules, then prove them, which inv...Liveness properties are important in model checking. We put forward multi-actor liveness rules based on Lesilie Lamport's TLA (temporal logic of actions) and liveness rules, then prove them, which involve existential or universal quantification under weak and strong fairness., At last we formalize the Internet banking system with TLA+ and check them with TLC. The results show these rules are appropriate.Read More
Publication Year: 2008
Publication Date: 2008-10-01
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot