Control synthesis of timed discrete event systems based on predicate invariance

In this paper, arc-timed Petri nets are used to model controlled real-time discrete event systems, and the control synthesis problem that designs a co ntroller for a system to satisfy its given closed-loop behavior specificati on is addressed. For the problem with the closed-loop behavior specified by a state predicate, real-time control-invariant predicates are introduced, and a fixpoint algorithm to compute the unique extremal control-invariant s ubpredicate of a given predicate, key to the control synthesis, is presente d. For the problem with the behavior specified by a labeled arc-timed Petri net, it is shown that the control synthesis problem can be transformed int o one that synthesizes a controller for an induced arc-timed Petri net with a state predicate specification, The problem can then be solved by using t he fixpoint algorithm as well. The algorithm involves conjunction and disju nction operations of polyhedral sets and can be algorithmically implemented , making automatic synthesis of controllers for real-time discrete event sy stems possible.