Model Checking Prioritized Timed Automata

Abstract. Priorities are often used to resolve conflicts in timed systems. However, priorities are not directly supported by state-of-art model checkers. Often, a designer has to either abstract the priorities leading to a high degree of nondeterminism or model the priorities using existing primitives. In this work, it is shown how prioritized timed automata can make modelling prioritized timed systems easier through the support for priority specification and model checking. The verification of prioritized timed automata requires a subtraction operation to be performed on two clock zones, represented by DBMs, for which we propose an algorithm to generate the minimal number of zones partitioned. After the application of a series of DBM subtraction operations, the number of zones generated become large. We thus propose an algorithm to reduce the final number of zones partitioned by merging some of them. A typical bus arbitration example is used to illustrate the benefits of the prop...

• Type: Conference
• Year: 2005
• Where: ATVA
• Authors: Shang-Wei Lin, Pao-Ann Hsiung, Chun-Hsian Huang, Yean-Ru Chen
• Keywords: ATVA 2005, Prioritized Timed Automata, Prioritized Timed Systems, Timed Systems