Improving model checking stateful timed CSP with non-zenoness through clock-symmetry reduction

• Main Authors: SI, Yuanjie, SUN, Jun, LIU, Yang, WANG, Ting
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2013
• Subjects: Model Check; Label Transition System; Symmetry Reduction; Strongly Connected Component; Time Automaton; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/4998; https://ink.library.smu.edu.sg/context/sis_research/article/6001/viewcontent/improving_model.pdf
• Institution: Singapore Management University

Real-time system verification must deal with a special notion of ‘fairness’, i.e., clocks must always be able to progress. A system run which prevents clocks from progressing unboundedly is known as Zeno. Zeno runs are infeasible in reality and thus must be pruned during system verification. Though...