Lexicographic multi-objective problems, which impose a lexicographic importance order over the objectives, arise in many real-life scenarios. Existing Reinforcement Learning work directly addressing lexicographic tasks has been scarce. The few proposed approaches were all noted to be heuristics without theoretical guarantees as the Bellman equation is not applicable to them. Additionally, the practical applicability of these prior approaches also suffers from various issues such as not being able to reach the goal state. While some of these issues have been known before, in this work we investigate further shortcomings and propose fixes for improving practical performance in many cases. We also present a policy optimization approach using our Lexicographic Projection Algorithm (LPA) that has the potential to address these theoretical and practical concerns. Finally, we demonstrate our proposed algorithms on benchmark problems.

Signal Temporal Logic (STL) is a timed temporal logic formalism that has found widespread adoption for rigorous specification of properties in Cyber-Physical Systems. However, STL is unable to specify oscillatory properties commonly required in engineering design. This limitation can be overcome by the addition of additional operators, for example, signal-value freeze operators, or with first order quantification. Previous work on augmenting STL with such operators has resulted in intractable monitoring algorithms. We present the first efficient and scalable offline monitoring algorithms for STL augmented with independent freeze quantifiers. Our final optimized algorithm has a |ρ|log (|ρ|) dependence on the trace length |ρ| for most traces ρ arising in practice, and a |ρ|2 dependence in the worst case. We also provide experimental validation of our algorithms – we show the algorithms scale to traces having 100k time samples.

Researchers have previously proposed augmenting Signal Temporal Logic (STL) with the value freezing operator in order to express engineering properties that cannot be expressed in STL. This augmented logic is known as STL*. The previous algorithms for STL*monitoring were intractable, and did not scale formulae with nested freeze variables. We present offline discrete-time monitoring algorithms with an acceleration heuristic, both for Boolean monitoring as well as for quantitative robustness monitoring. The acceleration heuristic operates over time intervals where subformulae hold true, rather than over the original trace sample-points. We present experimental validation of our algorithms, the results show that our algorithms can monitor over long traces for formulae with two or three nested freeze variables. Our work is the first work with monitoring algorithm implementations for STL*formulae with nested freeze variables.

Signal temporal logic (STL) is a variant of metric temporal logic (MTL) which can express intricate temporal requirements over signals and has found wide adoption for expressing requirements over complex control systems models. A key factor in the success of STL has been that of quantitative robustness, and the development of efficient algorithms for computing the robustness values over traces. The real-valued quantitative robustness of a signal with respect to an STL property quantifies the degree of satisfaction or violation of the property by the signal. In this work, we introduce a notion of robustness for a more expressive logic, timed STL (TSTL), which can be seen as timed propositional temporal logic (TPTL) with predicates defined over real-valued signals. This logic can express many natural engineering requirements that STL cannot. We also develop algorithms for computing this robustness value over traces in the pointwise semantics. While the robustness computation for general TSTL formulas is PSPACE-hard due to the PSPACE-hardness of the monitoring problem for TPTL, for the special case of one variable TSTL, a fragment of TSTL which is still more expressive than STL, we develop an optimized algorithm which computes robustness in time linear in the length of the trace. Finally, we experimentally validate the tractability of our algorithms with our prototype tool in MATLAB.

The temporal logic Timed Propositional Temporal Logic () extends with freeze quantifiers in order to express timing constraints, and is strictly more expressive than Metric Temporal Logic () over future modalities. The monitoring problem is to check whether a particular timed trace satisfies a given temporal logic specification, and monitoring procedures form core subroutines of testing and falsification approaches for Cyber-Physical Systems. In this work, we develop an efficient linear time monitoring algorithm, linear in the length of the trace (for traces that have at most a constant number of sample points in any unit interval), for one variable in the pointwise semantics. This one variable fragment is known to be already more expressive than and thus allows specifications of richer timed properties. Our algorithm carefully combines a divide and conquer approach with dynamic programming in order to achieve a linear time algorithm. As a plus, our algorithm uses only a simple two-dimensional table, and a syntax tree of the formula, as the data structures, and hence can be easily implemented on various platforms. We demonstrate the tractability of our approach with our prototype tool implementation on Matlab; our experiments show the tool scales easily to long trace lengths.

In recent years black-box optimization based search testing for Signal Temporal Logic (STL) specifications has been shown to be a promising approach for finding bugs in complex Cyber-Physical Systems (CPS) that are out of reach of formal analysis tools. The efficacy of this approach depends on efficiently exploring the input signal space, which for CPS is infinite. In this work, we present a framework for more efficient exploration of the input space for falsification of a class of engineering requirements. Our first contribution is a dimensionality reduction heuristic for optimization based falsification frameworks for dynamical systems over this augmented logic. This heuristic leverages the step response of the system - a standard system characteristic from Control engineering - to obtain a smaller time interval in which the optimizer needs to vary the inputs. Next, we note that system behaviors on a standard class of inputs such as on step inputs or sinusoids are often of paramount importance to engineers, and such inputs while easy to specify as functions, are difficult for temporal logics to capture. Our second contribution is a formalism to augment a commonly used fragment of Signal Temporal Logic (STL) to incorporate such signals for use in a black-box optimization based falsification framework. Finally, we demonstrate the effectiveness of our approach in falsification of temporal logic specifications on three case studies over complex Simulink models.

We propose a new model for formalizing reward collection problems on graphs with dynamically generated rewards which may appear and disappear based on a stochastic model. The robot routing problem is modeled as a graph whose nodes are stochastic processes generating potential rewards over discrete time. The rewards are generated according to the stochastic process, but at each step, an existing reward disappears with a given probability. The edges in the graph encode the (unit-distance) paths between the rewards' locations. On visiting a node, the robot collects the accumulated reward at the node at that time, but traveling between the nodes takes time. The optimization question asks to compute an optimal (or epsilon-optimal) path that maximizes the expected collected rewards. We consider the finite and infinite-horizon robot routing problems. For finite-horizon, the goal is to maximize the total expected reward, while for infinite horizon we consider limit-average objectives. We study the computational and strategy complexity of these problems, establish NP-lower bounds and show that optimal strategies require memory in general. We also provide an algorithm for computing epsilon-optimal infinite paths for arbitrary epsilon > 0.

The conformance testing problem for dynamical systems asks, given two dynamical models (e.g., as Simulink diagrams), whether their behaviors are “close” to each other. In the semi-formal approach to conformance testing, the two systems are simulated on a large set of tests, and a metric, defined on pairs of real-valued, real-timed trajectories, is used to determine a lower bound on the distance. We show how the Skorokhod metric on continuous dynamical systems can be used as the foundation for conformance testing of complex dynamical models. The Skorokhod metric allows for both state value mismatches and timing distortions, and is thus well suited for checking conformance between idealized models of dynamical systems and their implementations. We demonstrate the robustness of the metric by proving a transference theorem : trajectories close under the Skorokhod metric satisfy “close” logical properties in the timed linear time logic FLTL (Freeze LTL ) containing a rich class of temporal and spatial constraint predicates involving time and value freeze variables. We provide efficient window-based streaming algorithms to compute the Skorokhod metric for both piecewise affine and piecewise constant traces, and use these as a basis for a conformance testing tool for Simulink. We experimentally demonstrate the effectiveness of our tool in finding discrepant behaviors on a set of control system benchmarks, including an industrial challenge problem.

Many problems in the design and analysis of cyber-physical systems (CPS) reduce to the following optimization problem: given a CPS which transforms continuous-time input traces in R m to continuous-time output traces in R n and a cost function over output traces, find an input trace which minimizes the cost. Cyber-physical systems are typically so complex that solving the optimization problem analytically by examining the system dynamics is not feasible. We consider a black-box approach, where the optimization is performed by testing the input-output behaviour of the CPS. We provide a unified, tool-supported methodology for CPS testing and optimization. Our tool is the first CPS testing tool that supports Bayesian optimization. It is also the first to employ fully automated dimensionality reduction techniques. We demonstrate the potential of our tool by running experiments on multiple industrial case studies. We compare the effectiveness of Bayesian optimization to state-of-the-art testing techniques based on CMA-ES and Simulated Annealing.

We investigate quantifying the difference between two hybrid dynamical systems under noise and initial-state uncertainty. While the set of traces for these systems is infinite, it is possible to symbolically approximate trace sets using \emph{reachpipes} that compute upper and lower bounds on the evolution of the reachable sets with time. We estimate distances between corresponding sets of trajectories of two systems in terms of distances between the reachpipes.

The Skorokhod distance is a natural metric on traces of continuous and hybrid systems. It measures the best match between two traces, each mapping a time interval [0, T] to a metric space O, when continuous bijective timing distortions are allowed. Formally, it computes the infimum, over all timing distortions, of the maximum of two components: the first component quantifies the timing discrepancy of the timing distortion, and the second quantifies the mismatch (in the metric space O) of the values after the timing distortion. Skorokhod distances appear in various fundamental hybrid systems analysis concerns: from definitions of hybrid systems semantics and notions of equivalence, to practical problems such as checking the closeness of models or the quality of simulations. Despite its extensive use in semantics, the computation problem for the Skorokhod distance between two finite sampled-time hybrid traces remained open.

We introduce quantatitive timed refinement metrics and quantitative timed simulation functions, incorporating zenoness checks, for timed systems. These functions assign positive real numbers between zero and infinity which quantify the timing mismatches between two timed systems, amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximum timing mismatch that can arise, (2) the "steady-state" maximum timing mismatches, where initial transient timing mismatches are ignored; and (3) the (long-run) average timing mismatches amongst two systems. These three kinds of mismatches constitute three important types of timing differences. Our event times are the global times, measured from the start of the system execution, not just the time durations of individual steps. We present algorithms over timed automata for computing the three quantitative simulation functions to within any desired degree of accuracy. In order to compute the values of the quantitative simulation functions, we use a game theoretic formulation. We introduce two new kinds of objectives for two player games on finite state game graphs: (1) eventual debit-sum level objectives, and (2) average debit-sum level objectives. We present algorithms for computing the optimal values for these objectives for player 1, and then use these algorithms to compute the values of the quantitative timed simulation functions.

The notion of delays arises naturally in many computational models, such as, in the design of circuits, control systems, and dataflow languages. In this work, we introduce automata with delay blocks (ADBs), extending finite state automata with variable time delay blocks, for deferring individual transition output symbols, in a discrete-time setting. We show that the ADB languages strictly subsume the regular languages, and are incomparable in expressive power to the context-free languages. We show that ADBs are closed under union, concatenation and Kleene star, and under intersection with regular languages, but not closed under complementation and intersection with other ADB languages. We show that the emptiness and the membership problems are decidable in polynomial time for ADBs, whereas the universality problem is undecidable. Finally we consider the linear-time model checking problem, i.e., whether the language of an ADB is contained in a regular language, and show that the model checking problem is PSPACE-complete.

We study synthesis of controllers for real-time systems, where the objective is to stay in a given safe set. The problem is solved by obtaining winning strategies in the setting of concurrent two-player timed automaton games with safety objectives. To prevent a player from winning by blocking time, we restrict each player to strategies that ensure that the player cannot be responsible for causing a zeno run. We construct winning strategies for the controller which require access only to (1) the system clocks (thus, controllers which require their own internal infinitely precise clocks are not necessary), and (2) a linear (in the number of clocks) number of memory bits. Precisely, we show that for safety objectives, a memory of size (3 •|C| + lg(|C|+1)) bits suffices for winning controller strategies, where C is the set of clocks of the timed automaton game, significantly improving the previous known exponential bound. We also settle the open question of whether winning region controller strategies require memory for safety objectives by showing with an example the necessity of memory for region strategies to win for safety objectives.