Efficient Time State Space for Analysis of Real-Time Systems

摘要

Time Petri Nets are widely accepted as a formal model of realtime systems. As is well known, a fundamental issue in automated analysis of concurrent systems is to overcome state space explosion problem, i.e., developing an efficient method to generate compact state space. In the case of real time systems, the problem gets worse, namely there are infinitely many states, since time constraints are given over continuous time domain. Several researches have been conducted on this issue and some solutions have been proposed. Class graph is one of them. However there is some redundancy in class graphs. In this paper, redundancy included in the previous work - class graph - is explicitly pointed out. Then a new definition of a time state, called C-class, C-class represents compact class, to remove the redundancy is proposed. In consequence compact time state space can be generated with the proposed notion of time state.