Formalizing operator task analysis

Human operators are unique in their decision making capability, judgment and nondeterminism. Their sense of judgment, unpredictable decision procedures, susceptibility to environmental elements can cause them to erroneously execute a given task description to operate a computer system. Usually, a computer system is protected against some erroneous human behaviors by having necessary safeguard mechanisms in place. But some erroneous human operator behaviors can lead to severe or even fatal consequences especially in safety critical systems. A generalized methodology that can allow modeling and analyzing the interactions between computer systems and human operators where the operators are allowed to deviate from their prescribed behaviors will provide a formal understanding of the robustness of a computer system against possible aberrant behaviors by its human operators. We provide several methodology for assisting in modeling and analyzing human behaviors exhibited while operating computer systems. Every human operator is usually given a specific recommended set of guidelines for operating a system. We first present process algebraic methodology for modeling and verifying recommended human task execution behavior. We present how one can perform runtime monitoring of a computer system being operated by a human operator for checking violation of temporal safety properties. We consider the concept of a protection envelope giving a wider class of behaviors than those strictly prescribed by a human task that can be tolerated by a system. We then provide a framework for determining whether a computer system can maintain its guarantees if the human operators operate within their protection envelopes. This framework also helps to determine the robustness of the computer system under weakening of the protection envelopes. In this regard, we present a tool called Tutela that assists in implementing the framework. We then examine the ability of a system to remain safe under broad classes of variations of the prescribed human task. We develop a framework for addressing two issues. The first issue is: given a human task specification and a protection envelope, will the protection envelope properties still hold under standard erroneous executions of that task by the human operators? In other words how robust is the protection envelope? The second issue is: in the absence of a protection envelope, can we approximate a protection envelope encompassing those standard erroneous human behaviors that can be safely endured by the system? We present an extension of Tutela that implements this framework. The two frameworks mentioned above use Concurrent Game Structures (CGS) as models for both computer systems and their human operators. However, there are some shortcomings of this formalism for our uses. We add incomplete information concepts in CGSs to achieve better modularity for the players. We introduce nondeterminism in both the transition system and strategies of players and in the modeling of human operators and computer systems. Nondeterministic action strategies for players in \emph{i}ncomplete information \emph{N}ondeterministic CGS (iNCGS) is a more precise formalism for modeling human behaviors exhibited while operating a computer system. We show how we can reason about a human behavior satisfying a guarantee by providing a semantics of Alternating Time Temporal Logic based on iNCGS player strategies. In a nutshell this dissertation provides formal methodology for modeling and analyzing system robustness against both expected and erroneous human operator behaviors.

Coordinated pricing and inventory management

This dissertation mainly focuses on coordinated pricing and inventory management problems, where the related background is provided in Chapter 1. Several periodic-review models are then discussed in Chapters 2,3,4 and 5, respectively. Chapter 2 analyzes a deterministic single-product model, where a price adjustment cost incurs if the current selling price is changed from the previous period. We develop exact algorithms for the problem under different conditions and find out that computation complexity varies significantly associated with the cost structure. %Moreover, our numerical study indicates that dynamic pricing strategies may outperform static pricing strategies even when price adjustment cost accounts for a significant portion of the total profit. Chapter 3 develops a single-product model in which demand of a period depends not only on the current selling price but also on past prices through the so-called reference price. Strongly polynomial time algorithms are designed for the case without no fixed ordering cost, and a heuristic is proposed for the general case together with an error bound estimation. Moreover, our illustrates through numerical studies that incorporating reference price effect into coordinated pricing and inventory models can have a significant impact on firms' profits. Chapter 4 discusses the stochastic version of the model in Chapter 3 when customers are loss averse. It extends the associated results developed in literature and proves that the reference price dependent base-stock policy is proved to be optimal under a certain conditions. Instead of dealing with specific problems, Chapter 5 establishes the preservation of supermodularity in a class of optimization problems. This property and its extensions include several existing results in the literature as special cases, and provide powerful tools as we illustrate their applications to several operations problems: the stochastic two-product model with cross-price effects, the two-stage inventory control model, and the self-financing model.

Quantification of the human postural control system to perturbations

Human standing posture is inherently unstable. The postural control system (PCS), which maintains standing posture, is composed of the sensory, musculoskeletal, and central nervous systems. Together these systems integrate sensory afferents and generate appropriate motor efferents to adjust posture. The PCS maintains the body center of mass (COM) with respect to the base of support while constantly resisting destabilizing forces from internal and external perturbations. To assess the human PCS, postural sway during quiet standing or in response to external perturbation have frequently been examined descriptively. Minimal work has been done to understand and quantify the robustness of the PCS to perturbations. Further, there have been some previous attempts to assess the dynamical systems aspects of the PCS or time evolutionary properties of postural sway. However those techniques can only provide summary information about the PCS characteristics; they cannot provide specific information about or recreate the actual sway behavior. This dissertation consists of two parts: part I, the development of two novel methods to assess the human PCS and, part II, the application of these methods. In study 1, a systematic method for analyzing the human PCS during perturbed stance was developed. A mild impulsive perturbation that subjects can easily experience in their daily lives was used. A measure of robustness of the PCS, 1/MaxSens that was based on the inverse of the sensitivity of the system, was introduced. 1/MaxSens successfully quantified the reduced robustness to external perturbations due to age-related degradation of the PCS. In study 2, a stochastic model was used to better understand the human PCS in terms of dynamical systems aspect. This methodology also has the advantage over previous methods in that the sway behavior is captured in a model that can be used to recreate the random oscillatory properties of the PCS. The invariant density which describes the long-term stationary behavior of the center of pressure (COP) was computed from a Markov chain model that was applied to postural sway data during quiet stance. In order to validate the Invariant Density Analysis (IDA), we applied the technique to COP data from different age groups. We found that older adults swayed farther from the centroid and in more stochastic and random manner than young adults. In part II, the tools developed in part I were applied to both occupational and clinical situations. In study 3, 1/MaxSens and IDA were applied to a population of firefighters to investigate the effects of air bottle configuration (weight and size) and vision on the postural stability of firefighters. We found that both air bottle weight and loss of vision, but not size of air bottle, significantly decreased balance performance and increased fall risk. In study 4, IDA was applied to data collected on 444 community-dwelling elderly adults from the MOBILIZE Boston Study. Four out of five IDA parameters were able to successfully differentiate recurrent fallers from non-fallers, while only five out of 30 more common descriptive and stochastic COP measures could distinguish the two groups. Fall history and the IDA parameter of entropy were found to be significant risk factors for falls. This research proposed a new measure for the PCS robustness (1/MaxSens) and a new technique for quantifying the dynamical systems aspect of the PCS (IDA). These new PCS analysis techniques provide easy and effective ways to assess the PCS in occupational and clinical environments.