Decentralized Diagnosis of Event-Driven Systems for Safely Reacting to Failures

We introduce the notion of safe-codiagnosability, extending the notion of safe-diagnosability (Paoli and Lafortune, 2005) to the decentralized setting. For a system, a certain subbehavior is deemed safe (captured via a safety specification), and a further subbehavior is deemed nonfaulty (captured via a nonfault specification). Safe-codiagnosability requires that when the system executes a trace that is faulty, there exists at least one diagnoser that can detect this within bounded delay and also before the safety specification is violated. The above notion of safe-codiagnosability may also be viewed as an extension of the notion of codiagnosability (Qiu and Kumar, 2006), where the latter did not have any safety requirement. We show that safe-codiagnosability is equivalent to codiagnosability together with ldquozero-delay codiagnosabilityrdquo of ldquoboundary safe tracesrdquo. (A safe trace is a boundary safe trace if there exists a single-event extension that is unsafe.) We give an algorithm of polynomial complexity for verifying safe-codiagnosability. For a safe-codiagnosable system, the same methods as those proposed in (Qiu and Kumar, 2006) can be applied for offline synthesis of individual diagnosers, as well as for online diagnosis using them.     

Functional synthesis for linear arithmetic and sets

Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, synthesis algorithms should behave in a predictable way—they should succeed for a well-defined class of specifications. To guarantee correctness and applicability to software (and not just hardware), these algorithms should also support unbounded data types, such as numbers and data structures. To obtain appropriate synthesis algorithms, we propose to generalize decision procedures into predictable and complete synthesis procedures. Such procedures are guaranteed to find the code that satisfies the specification if such code exists. Moreover, we identify conditions under which synthesis will statically decide whether the solution is guaranteed to exist and whether it is unique. We demonstrate our approach by starting from a quantifier elimination decision procedure for Boolean algebra of set with Presburger arithmetic and transforming it into a synthesis procedure. Our procedure also works in the presence of parametric coefficients. We establish results on the size and the efficiency of the synthesized code. We show that such procedures are useful as a language extension with implicit value definitions, and we show how to extend a compiler to support such definitions. Our constructs provide the benefits of synthesis to programmers, without requiring them to learn new concepts, give up a deterministic execution model, or provide code skeletons.     

Discovering Robust Knowledge from Databases that Change

Many applications of knowledge discovery and data mining such as rule discovery for semantic query optimization, database integration and decision support, require the knowledge to be consistent with the data. However, databases usually change over time and make machine-discovered knowledge inconsistent. Useful knowledge should be robust against database changes so that it is unlikely to become inconsistent after database updates. This paper defines this notion of robustness in the context of relational databases and describes how robustness of first-order Horn-clause rules can be estimated. Experimental results show that our estimation approach can accurately identify robust rules. We also present a rule antecedent pruning algorithm that improves the robustness and applicability of machine discovered rules to demonstrate the usefulness of robustness estimation.     

On the Reachability Problem for Uncertain Hybrid Systems

In this paper, we revisit the problem of designing controllers to meet safety specifications for hybrid systems, whose evolution is affected by both control and disturbance inputs. The problem is formulated as a dynamic game and an appropriate notion of hybrid strategy for the control inputs is developed. The design of hybrid strategies to meet safety specifications is based on an iteration of alternating discrete and continuous safety calculations. We show that, under certain assumptions, the iteration converges to a fixed point, which turns out to be the maximal set of states for which the safety specifications can be met. The continuous part of the calculation relies on the computation of the set of winning states for one player in a two player, two target, pursuit evasion differential game. We develop a characterization of these winning states (as well as the winning states for the other player for completeness) using methods from nonsmooth analysis and viability theory.     

Distributed synthesis for well-connected architectures

We study the synthesis problem for external linear or branching specifications and distributed, synchronous architectures with arbitrary delays on processes. External means that the specification only relates input and output variables. We introduce the subclass of uniformly well-connected (UWC) architectures for which there exists a routing allowing each output process to get the values of all inputs it is connected to, as soon as possible. We prove that the distributed synthesis problem is decidable on UWC architectures if and only if the output variables are totally ordered by their knowledge of input variables. We also show that if we extend this class by letting the routing depend on the output process, then the previous decidability result fails. Finally, we provide a natural restriction on specifications under which the whole class of UWC architectures is decidable.     

Complexity issues in automated synthesis of failsafe fault-tolerance

We focus on the problem of synthesizing failsafe fault-tolerance where fault-tolerance is added to an existing (fault-intolerant) program. A failsafe fault-tolerant program satisfies its specification (including safety and liveness) in the absence of faults. However, in the presence of faults, it satisfies its safety specification. We present a somewhat unexpected result that, in general, the problem of synthesizing failsafe fault-tolerant distributed programs from their fault-intolerant version is NP-complete in the state space of the program. We also identify a class of specifications, monotonic specifications, and a class of programs, monotonic programs, for which the synthesis of failsafe fault-tolerance can be done in polynomial time (in program state space). As an illustration, we show that the monotonicity restrictions are met for commonly encountered problems, such as Byzantine agreement, distributed consensus, and atomic commitment. Furthermore, we evaluate the role of these restrictions in the complexity of synthesizing failsafe fault-tolerance. Specifically, we prove that if only one of these conditions is satisfied, the synthesis of failsafe fault-tolerance is still NP-complete. Finally, we demonstrate the application of monotonicity property in enhancing the fault-tolerance of (distributed) nonmasking fault-tolerant programs to masking.     

Symbolic synthesis of masking fault-tolerant distributed programs

We focus on automated addition of masking fault-tolerance to existing fault-intolerant distributed programs. Intuitively, a program is masking fault-tolerant, if it satisfies its safety and liveness specifications in the absence and presence of faults. Masking fault-tolerance is highly desirable in distributed programs, as the structure of such programs are fairly complex and they are often subject to various types of faults. However, the problem of synthesizing masking fault-tolerant distributed programs from their fault-intolerant version is NP-complete in the size of the program’s state space, setting the practicality of the synthesis problem in doubt. In this paper, we show that in spite of the high worst-case complexity, synthesizing moderate-sized masking distributed programs is feasible in practice. In particular, we present and implement a BDD-based synthesis heuristic for adding masking fault-tolerance to existing fault-intolerant distributed programs automatically. Our experiments validate the efficiency and effectiveness of our algorithm in the sense that synthesis is possible in reasonable amount of time and memory. We also identify several bottlenecks in synthesis of distributed programs depending upon the structure of the program at hand. We conclude that unlike verification, in program synthesis, the most challenging barrier is not the state explosion problem by itself, but the time complexity of the decision procedures.     

CLF based designs with robustness to dynamic input uncertainties

The problem of robust stabilization of nonlinear systems in the presence of input uncertainties is of great importance in practical implementation. Stabilizing control laws may not be robust to this type of uncertainty, especially if cancellation of nonlinearities is used in the design. By exploiting a connection between robustness and optimality, “domination redesign” of the control Lyapunov function (CLF) based Sontag's formula has been shown to possess robustness to static and dynamic input uncertainties. In this paper we provide a sufficient condition for the domination redesign to apply. This condition relies on properties of local homogeneous approximations of the system and of the CLF. We show that an inverse optimal control law may not exist when these conditions are violated and illustrate how these conditions may guide the choice of a CLF which is suitable for domination redesign.     

Nominally Robust Model Predictive Control With State Constraints

In this paper, we present robust stability results for constrained discrete-time nonlinear systems using a finite-horizon model predictive control (MPC) algorithm for which we do not require the terminal cost to have any particular properties. We introduce a definition that attempts to characterize the robustness properties of the MPC optimization problem. We assume the systems under consideration satisfy this definition (for which we give sufficient conditions) and make two further assumptions. These are that the value function is bounded by a K_infin function of a state measure (related to the distance from the state to some target set) and that this measure is detectable from the stage cost used in the MPC algorithm. We show that these assumptions lead to stability that is robust to sufficiently small disturbances. While in general the results are semiglobal and practical, when the detectability and upper bound assumptions are satisfied with linear K_infin functions, the stability and robustness are either semiglobal or global (with respect to the feasible set). We discuss algorithms employing terminal inequality constraints and also provide a specific example of an algorithm that employs a terminal equality constraint.     

The scenario approach to robust control design

This paper proposes a new probabilistic solution framework for robust control analysis and synthesis problems that can be expressed in the form of minimization of a linear objective subject to convex constraints parameterized by uncertainty terms. This includes the wide class of NP-hard control problems representable by means of parameter-dependent linear matrix inequalities (LMIs). It is shown in this paper that by appropriate sampling of the constraints one obtains a standard convex optimization problem (the scenario problem) whose solution is approximately feasible for the original (usually infinite) set of constraints, i.e., the measure of the set of original constraints that are violated by the scenario solution rapidly decreases to zero as the number of samples is increased. We provide an explicit and efficient bound on the number of samples required to attain a-priori specified levels of probabilistic guarantee of robustness. A rich family of control problems which are in general hard to solve in a deterministically robust sense is therefore amenable to polynomial-time solution, if robustness is intended in the proposed risk-adjusted sense.     

Robust controller design for a non-colocated spring-mass system via mixed 𝓁/∞ optimization

A successful controller design paradigm must take into account both model uncertainty and performance specifications. Model uncertainty can be addressed using the ??^∞ robust control framework. However, this framework cannot accommodate the realistic case where in addition to robustness considerations, the system is subject to time-domain specifications. We recently proposed design procedures to explicitly incorporate time-domain specifications into the ??^∞ framework. In this paper we apply these design procedures to the simple mass-spring system used as a benchmark in the 1990–1992 ACC, with the goal of minimizing the peak control effort while satisfying disturbance rejection, settling time, tracking and robustness specifications. The results show that there exist a severe trade-off between peak control action and robustness to unstructured model uncertainty.     

The robust knapsack problem with queries

We consider robust knapsack problems where item weights are uncertain. We are allowed to query an item to find its exact weight,where the number of such queries is bounded by a given parameter Q. After these queries are made, we need to pack the items robustly, i.e., so that the choice of items is feasible for every remaining possible scenario of item weights.The central question that we consider is: Which items should be queried in order to gain maximum profit? We introduce the notion of query competitiveness for strict robustness to evaluate the quality of an algorithm for this problem, and obtain lower and upper bounds on this competitiveness for interval-based uncertainty. Similar to the study of online algorithms, we study the competitiveness under different frameworks, namely we analyze the worst-case query competitiveness for deterministic algorithms, the expected query competitiveness for randomized algorithms and the average case competitiveness for known distributions of the uncertain input data. We derive theoretical bounds for these different frameworks and evaluate them experimentally. We also extend this approach to Γ-restricted uncertainties introduced by Bertsimas and Sim.Furthermore, we present heuristic algorithms for the problem. In computational experiments considering both the interval-based and the Γ-restricted uncertainty, we evaluate their empirical performance. While the usage of a Γ-restricted uncertainty improves the nominal performance of a solution (as expected), we find that the query competitiveness gets worse.     

The Unit-B method: refinement guided by progress concerns

We present Unit-B, a formal method inspired by Event-B and UNITY. Unit-B aims at the stepwise design of software systems, satisfying safety and liveness properties. The method features the novel notion of coarse and fine schedules, a generalisation of weak and strong fairness for specifying events’ scheduling assumptions. Based on events schedules, we propose proof rules to reason about progress properties and a refinement order preserving both liveness and safety properties. We illustrate our approach by an example to show that systems development can be driven by not only safety but also liveness requirements.     

Discrete-time certainty equivalence output feedback: allowing discontinuous control laws including those from model predictive control

We present certainty equivalence output feedback results for discrete-time nonlinear systems that employ possibly discontinuous control laws in the feedback loop. Coupling assumptions of nominal robustness with uniform observability or detectability assumptions, we assert nominally robust stability for output feedback closed loops. We further show that model predictive control (MPC) can be used to generate a feedback control law that is robustly globally asymptotically stabilizing when used in a certainty equivalence output feedback closed loop. Allowing for discontinuous feedback control laws is important for systems employing MPC, since the method can, and sometimes necessarily does, result in discontinuous control laws.     

A Functional Rephrasing of the Assumption/Commitment Specification Style

The assumption/commitment (also called rely/guarantee) style has been advocated for the specification of interactive components of distributed systems. It suggests the structuring of specifications into assumptions about the behavior of the component's environment and into commitments that are fulfilled by the component, provided the environment fulfills these assumptions. One of its motivations is to achieve modularity (also called compositionality) for state transition specifications of system components. Another reason for writing specifications in this format lies in proof rules that refer to this format. We define the assumption/commitment formats for functional system specifications. In particular, we work out a canonical decomposition of system specifications following the assumption/commitment format into safety and liveness aspects. We demonstrate the format of assumption/commitment specifications by a number of examples. Finally, we discuss the methodological significance of the assumption/commitment format in the stepwise development of specifications.     

A complete algebraic characterization of behavioral subtyping

We present a model-theoretic study of correct behavioral subtyping for first-order, deterministic, abstract data types with immutable objects. For such types, we give a new algebraic criterion for proving correct behavioral subtyping that is both necessary and sufficient. This proof technique handles incomplete specifications by allowing proofs of correct behavioral subtyping to be based on comparison with one of several paradigmatic models. It compares a model to a selected paradigm with a generalization of the usual notion of simulation relations. This generalization is necessary for specifications that are not term-generated and that use multiple dispatch. However, we also show that the usual notion of simulation gives a necessary and sufficient proof technique for the special cases of term-generated specifications and specifications that only use single dispatch. Received: 12 November 1997 / 12 November 1999     

Robust and adaptive control: fidelity or an open relationship?

Robust and adaptive control are essentially meant to solve the same control problem. Given an uncertain LTI model set with the assumption that the controlled plant slowly drifts or occasionally jumps in the allowed model set, find a controller that satisfies the given servo and disturbance rejection specifications. Specifications on the transient response to a sudden plant change or “plant jump” are easily incorporated into the robust control problem, and if a solution is found, the robust control system does indeed exhibit satisfactory transients to plant jumps. The reason to use adaptive control is its ability, when the plant does not jump, to maintain the given specifications with a lower-gain control action (or to achieve tighter specifications), and also to solve the control problem for a larger uncertainty set than a robust controller. Certainly equivalence-based adaptive controllers, however, often exhibit insufficient robustness and unsatisfactory transients to plant jumps. It is therefore suggested in this paper that adaptive control always be built on top of a robust controller in order to marry the advantages of robust and adaptive control. The concept is called adaptive robust control. It may be compared with gain scheduling, two-time scale adaptive control, intermittent adaptive control, repeated auto-tuning, or switched adaptive control, with the important difference that the control is switched between robust controllers that are based on plant uncertainty sets that take into account not only the currently estimated plant model set but also the possible jumps and drifts that may occur until the earliest next time the controller can be updated.     

Fault-tolerant strategies in the Iterated Prisoner's Dilemma

The aim of this paper is to determine how well can strategies in the Iterated Prisoner's Dilemma (IPD) behave in the presence of errors. A highly desirable property of strategies in IPD, even without errors, is their robustness. A strategy σ is called robust, if in any population consisting of copies of two types of strategies, σ itself and some other strategy τ, the strategy σ is never worse than τ. For example, the well known simple strategy tit-for-tat is robust. However, tit-for-tat is very vulnerable to errors: already one mistake in its execution can cause it to lose the property of robustness. The ultimate resistance to errors is captured by the notion of perfect fault-tolerance: a strategy has this property, if any distortion of it on an arbitrary finite number of moves remains robust. Do there exist perfectly fault-tolerant strategies in IPD? Somewhat surprisingly, the answer is yes: indeed we describe such a strategy and we prove that it has this very strong resistance to errors. However, we prove that no strategy with bounded memory can have this property. We then go on to show that preserving robustness under distortions on any fixed initial segment of moves is possible with bounded memory.     

Control of nondeterministic discrete-event systems for bisimulation equivalence

Most prior work on supervisory control of discrete event systems is for achieving deterministic specifications, expressed as formal languages. In this paper we study supervisory control for achieving nondeterministic specifications. Such specifications are useful when designing a system at a higher level of abstraction so that lower level details of system and its specification are omitted to obtain higher level models that may be nondeterministic. Nondeterministic specifications are also meaningful when the system to be controlled has a nondeterministic model due to the lack of information (caused for example by partial observation or unmodeled dynamics). Language equivalence is not an adequate notion of behavioral equivalence for nondeterministic systems, and instead we use the finest known notion of equivalence, namely the bisimulation equivalence. Choice of bisimulation equivalence is also supported by the fact that bisimulation equivalence specification is equivalent to a specification in the temporal logic of /spl mu/-calculus that subsumes the complete branching-time logic CTL*. Given nondeterministic models of system and its specification, we study the design of a supervisor (possibly nondeterministic) such that the controlled system is bisimilar to the specification. We obtain a small model theorem showing that a supervisor exists if and only if it exists over a certain finite state space, namely the power set of Cartesian product of system and specification state spaces. Also, the notion of state-controllability is introduced as part of a necessary and sufficient condition for the existence of a supervisor. In the special case of deterministic systems, we provide an existence condition that can be verified polynomially in both system and specification states, when the existence condition holds.