Analysis of hybrid systems based on hybrid net condition/event system model

In this paper, hybrid net condition/event systems are introduced as a model for hybrid systems. The model consists of a discrete timed Petri net and a continuous Petri net which interact each other through condition and event signals. By introducing timed discrete places in the model, timing constra ints in hybrid systems can be easily described. For a class of hybrid syste ms that can be described as linear hybrid net condition/event systems whose continuous part is a constant continuous Petri net, two methods are develo ped for their state reachability analysis. One is the predicate-transformat ion method, which is an extension of a state reachability analysis method f or linear hybrid automata. The other is the path-based method, which enumer ates all possible firing seqenences of discrete transitions and verifies if a given set of states can be reached from another set by firing a sequence of discrete transitions. The verification is performed by solving a constr aint satisfaction problem. A technique that adds additional constraints to the problem when a discrete state is revisited along the sequence is develo ped and used to prevent the method from infinite enumeration. These methods provide a basis for algorithmic analysis of this class of hybrid systems.