Decidability and optimality in pushdown control systems: A new approach to discrete event control

Supervisory Control Theory (SCT) was developed by P. J. Ramadge and W. M. Wonham in the late 80's as a method of understanding control of a wide variety of discrete event dynamic systems. A discrete event dynamic system (DEDS) is characterized by a directed, labeled graph. The nodes of this system are called the states, the arcs of the system are called transitions. Each transition has an event label. In this sense, an event causes the DEDS to change from one state to another. There is a special state called the starting state and a set of special states called the terminal, marked or final states. A system modeled by a state machine is assumed to exist in one of the states and transition from state to state as a result of the generation or execution of events. The alphabet of events is partitioned into controllable and uncontrollable events. Controllable events may be disabled by a system supervisor. Given a system to control (called the plant) modeled by a DEDS, a supervisor will disable certain events from occurring in the system in order to achieve a certain desired behavior. The supervisor is often designed as a second DEDS whose transitions correspond to enabled events. When the two DEDS are run in parallel, the supervisor may exert enabling and disabling control over the plant.; SCT is well understood in the case when both the plant and the supervisor are modeled as finite state machines; i.e., the number of DEDS states in both the plant and supervisor are finite. Several authors have remarked that the theory of SCT need not be restricted to the finite state case and in many ways they are correct. However, with the notable exception of a few Petri Net models, almost all of the results on SCT have been restricted to finite state systems. Specifically, decision algorithms for controllability and optimality are all restricted to the finite state case because in the infinite state case they become poorly defined.; The purpose of this thesis is three-fold: First, we develop an extended SCT that enables the modeling of infinite state systems by adding pushdown stack memory to the finite state machine models of the DEDS supervisors. Second we show that there are strong computability bounds on the nature of our new extended models with respect to the primary controllability criterion for discrete event control. That is, certain classes of control specifications cannot be provably enforced. Third, we provide a new theory of parametric optimal control in DEDS systems that extends to cases when the controller is a pushdown machine. We explore the problem of synthesizing a controller that will act optimally for all time. We derive a novel branch and bound algorithm for synthesizing such an optimal controller.; Three applications of the theoretical framework developed in this thesis are provided. The first shows how pushdown machines are capable of modeling subsets of the 802.11 wireless network protocol and displays methods for analyzing such protocols for robustness to attacks. The second application demonstrates how to use discrete event control to model computer security policies and shows how the pushdown stack memory of a deterministic pushdown machine can be used to enumerate file access information. The third example shows how the pushdown stack model can generalize the NASA Livingstone modeling system for use in validating robotic control systems for missions in deep space.