Automata theoretic verification commonly uses an automaton S to specify the behaviors of a system being analyzed and another automaton P to specify the property of interest. These automata are assumed to be finite state machines accepting finite or infinite words. The key step is to verify whether the language inclusion L(S) ⊆ L(P ) holds. Failing this inclusion, a counterexample σ is generated such that σ ∈ L(S) whereas σ ∈ L(P ). Another important area lies in runtime verification, wherein given a sequence of observations represented by σ ∈ Σ * , we wish to check whether these observations satisfy the specification: σ ∈ L(P ).
The verification community has considered numerous extensions to these basic ideas such as richer models of the system S that allow for succinct specifications (e.g., hierarchical state machines, state-charts), or go beyond finite state machines and include features such as real-time (timed automata) [4], physical quantities (hybrid automata) [3], and matching calls/returns [8,23,6]. The complexity of the language inclusion and membership problems in these settings are also well understood [11]. However, inclusion and membership problems lead to yes/no Boolean answers. The no answer for an inclusion problem is witnessed by a counterexample trace. However, the yes answer provides nothing further. A quantitative approach to these questions was proposed independently by Fainekos et al. [16], Donze et al. [14] and Rizk et al. [21] for the satisfaction of metric/signal temporal logic formula ϕ for a trace σ generated by continuous and hybrid systems. Therein, the authors use the euclidean metric over real-valued traces that defines a metric distance d(σ, σ ) between traces σ, σ in order to check whether traces that are in the epsilon neighborhood of a given trace σ also satisfy the formula: (∀σ ) d(σ, σ ) < ⇒ σ |= ϕ. Recent work, notably by Hasuo et al [24,1] and Deshmukh et al [12] generalizes these notions to time domain as well as the signal data domain. Efficient algorithms for computing the robustness of a trace with respect to metric (signal) temporal formulas are known, and furthermore, the theory led to numerous approaches to finding falsifications of complex Simulink/Stateflow models, mining robust requirements and other monitoring problems [7].
Robustness Using Weighted Transducers. In this paper, we specify distances between finite words over Σ * , using the notion of cost functions. A cost function assigns a non-negative rational cost to each pair of words (w 1 , w 2 ) ∈ Σ * × Σ * , modelling the cost of rewriting w 1 into w 2 . By bounding the costs of rewritings, it models how words can be transformed. As a result, a neighborhood can be defined for each word, assuming that the cost of "rewriting" a word w back to itself is 0. This, in turn, allows to reason about robustness of languages. In order to model cost functions, we use weighted transducers with non-negative weights [15] along with an aggregator that combines the cost of each individual rewriting of the transducer into an overall cost between the input and output words. We now provide motivating examples for the cost functions that can be specified by such a model. A formal definition is provided in Section 2. Motivating Example. Consider the transducer T of Figure 1. This transducer is over alphabet Σ : {a 1 , a 2 , b}. It allows to rewrite the letter a 1 into a 1 (at cost 0), and the letter a 2 into either a 2 (at cost 0) or b (at cost 1). Additionally, these rewritings are possible only at state q 1 . This allows us to have a model wherein errors appear in bursts rather than individually: I.e, an error at a location increases the likelihood of one at the subsequent location. Thus, the transducer models all possible words w that a given input word w can be rewritten into. As an example, the word w : a 1 a 2 a 2 a 2 into w : a 1 bba 2 through transitions that rewrite the first two occurrences of a 2 into b. At the same time, the transducer forbids certain rewritings. For instance, the word w above cannot be rewritten into the word w : bba 2 a 1 since the rewrite from an a 1 into a b or an a 2 into an a 1 is clearly disallowed by the transducer T in Figure 1.
While the transducer T specifies the cost for individual rewritings through its transitions, we define the cost of rewriting the entire word w into another w by additionally specifying an aggregator function. For simplicity, we assume that there is exactly one run of the transducer that rewrites w into w . The case of nondeterministic transducers is defined in Section 2.
Given a discount factor λ ∈ Q ∩ (0, 1), the cost of rewriting a word w into another word w is defined as n i=1 λ (i-1) τ i , wherein n is the size of a run through the transducer and τ i is the cost associated with the i th transition.
This aggregator computes the mean cost:
This aggregator computes the sum:
Returning to our example, the Sum-cost of rewriting a 1 a 2 a 2 a 2 into a 1 bba 2 is 2, for the DSum-cost with discount factor 1/2, it is 3/4, and for Mean-cost it is 1/2.
Our approach handles a more general nondeterministic transducer model that can allow for insertions of new letters, deletion of letters, transpositions and arbitrary substitutions of one letter by a finite word. Cost functions defined by such transducers may not satisfy the axioms of a metric, however many commonly encountered type of metrics between words such as the Cantor distance and the Levenstein (or edit) distance can be modeled as weighted transducers [13]. For example, edit distance is naturally modelled by a sum-transducer. Cantor distance maps any pair of word (w 1 , w 2 ) of same length to 2 -i where i the first position where w 1 and w 2 differ, and to 0 if w 1 = w 2 . This metric can be modelled by a discounted-sum transducer with discount factor 1/2.
Given a cost function c : (Σ * × Σ * ) → Q ≥0 defined by a weightedtransducer with an aggregator function, we can define "neighborhoods" of languages for a given distance ν ≥ 0. For a regular language N ⊆ Σ * and a threshold ν ∈ Q ≥0 , let us define its ν-neighborhood N ν : {w ∈ Σ * | (∃w ∈ N ) c(w, w ) ≤ ν}. Given a property L ⊆ Σ * , we consider the following robustness problems:
Robust inclusion: Given N, ν and L, check whether N ν ⊆ L. Threshold synthesis: Given N, L, find the largest threshold ν such that N ν ⊆ L.
Example 1. Consider the transducer of Figure 1 using the the Sum aggregator. We take L as the set of words which does not have bbb as a subword. Now, any word of the form (a 1 a 2 ) * are ν-robust for any threshold ν since the letter a 1 is not rewritten by the transducer T . Such questions are tackled using the robust inclusion problem. On the other hand, let us choose a word w ∈ a 2 a 2 a 2 (a * 1 ). It is ν-robust for all the thresholds ν ≤ 2 but not for ν ≥ 3. This is determined using the threshold synthesis problem. For all ν ≥ 3, the set of ν-robust words in N = Σ * is (a 1 + a 1 a 2 + a 1 a 2 a 2 ) * , and for ν ≤ 2, any word in Σ * is ν-robust. Such questions are solved using the robust kernel synthesis problem.
Weighted Transducers for Robustness Verification Contributions. We show that the robust inclusion problem is solvable in PTime when N and L are regular languages (given as NFA and DFA respectively) and the weighted-transducer defining the cost function is also given as input (Corollary 12). To obtain this result, we show that we can effectively compute in PTime the largest threshold ν as defined before, thus solving the threshold synthesis problem (Theorem 11). This result holds for the three measures Sum, DSum and Mean. For Sum, we show that the robust kernel is effectively regular (Lemma 14) and testing its non-emptiness is PSpace-complete (Theorem 15). For Mean, we show that the robust kernel is not regular in general (Lemma 16), and its non-emptiness is undecidable (Theorem 17). For DSum, we leave those questions partially open. We conjecture that the robust kernel is non-regular in general and provide a sufficient condition under which it is regular (Theorem 22).
Next, we present an implementation of the algorithms to synthesize robustness thresholds and report some experiments with our implementation, illustrating its application to analyzing manual control strategies under the presence of human error and approximate pattern analysis in type-1 diabetes data. Here we analyze a publicly available dataset of blood glucose values for people with type-1 diabetes. In both cases, we use a weighted transducer to model some of the specifics of human error and glucose sensor noise patterns. For the type-1 diabetes application, we use a robust pattern matching to detect behaviors that are clinically significant while accounting for the peculiarities of the glucose sensor.
Our work bears some similarities with earlier work by Henzinger et al [17,22]. In these papers, notions of robustness for string to string transformations are studied and the notion of continuity of these transformations is defined. This is different from our setting, in which we use weighted transducers to define notions of distances, and these transducers are not necessarily continuous. Our notion of robustness is with respect to the rewriting of the words of one language and not about the transducers. The transducers themselves serve to define neighborhoods of strings.
Let Σ be an alphabet. We denote the empty word by the symbol ε ∈ Σ and we write Σ * for the set of finite words over Σ. Let Σ ε = Σ ∪ {ε}. As usual, we write Q for the set of rationals, N = {0, 1, . . . } for naturals, and N * for the words over the infinite alphabet N.
A finite automaton over Σ is a tuple
that there exist q 0 , q 1 , . . . , q n and for all 1 ≤ i ≤ n, t i = (q i-1 , a i , q i ). The run r is simple if no state repeats along r, i.e. i = j implies that q i = q j and, it is a cycle if q 0 = q n . We say that r is a simple cycle if its a cycle and t 2 . . . t n is simple. Also, r is accepting if it starts from an initial state q 0 ∈ Q I and ends into a final state q n ∈ Q F . We denote by AccRun A (u) the set of accepting runs of A on the word u. The language defined by A is the set of words
Weighted transducers extend finite automata with string outputs and weights on transitions [15]. Any accepting run over some input word rewrites each input symbol into a (possibly empty) word, with some cost in N. Transducers can also have -input transitions with non-empty outputs, such that output symbols can be produced even though nothing is read on the input (e.g. allowing for symbol insertions). The output of a run is the concatenation of all output words occurring on its transitions. Its cost is defined by an aggregator function C : N * → Q ≥0 , which associates a rational number to a sequence of non-negative integers.
We consider three different aggregator functions, given later. Since there are possibly several accepting runs over the same input, and generating the same output, we take the minimal cost of them to compute the value of a pair of input and output words.
and Dest(t) = q . We say that a transition t ∈ ∆ can be triggered by T if it is in state Orig(t) and reads In(t) on its input (note that it is always possible to read In(t) = ε). It, then, moves to Dest(t) and rewrites its input into Out(t). A run r = t 1 . . . t n of T is a run of A. We write In(r) = In(t 1 ) . . . In(t n ) and Out(r) = Out(t 1 ) . . . Out(t n ) and say that r is a run of T on the pair of words (In(r), Out(r)). Let (u 1 , u 2 ) = (In(r), Out(r)). If moreover r is accepting, we say that (u 1 , u 2 ) is accepted by T , and denote by AccRun T (u 1 , u 2 ) the set of accepting runs over (u 1 , u 2 ). We also say that u 1 is accepted by T if (u 1 , u 2 ) is accepted by T for some u 2 ∈ Σ * . We denote the weight sequence of r by
A transducer T defines a relation from Σ * to itself, called a translation, denoted R T and defined by: R T
The domain of T , denoted dom(T ) is the set of words u 1 for which there exists u 2 such that (u 1 , u 2 ) ∈ R T . The cost of a pair of words (u 1 , u 2 ) is given by:
Note that since runs consume at least one symbol of the input or one of the output, there are finitely many runs on a pair (u 1 , u 2 ), hence the min is well-defined. Finally, given ν ∈ Q and an input word u 1 ∈ dom(T ), we define the threshold output language T ≤ν (u 1 ) of u 1 as:
This notation extends naturally to languages N ⊆ Σ * by setting: T ≤ν (N ) = u1∈N ∩dom(T ) T ≤ν (u 1 ).
This assumption requires that each point must belong to any of its neighborhoods, which naturally comes from the indiscernibility axiom of distance. However, we do not require the triangle inequality axiom, that the edit distance does not satisfy.
Cost functions. We consider three aggregator functions, namely the sum, the mean and the discounted-sum. Let λ ∈ Q ∩ (0, 1) be a discount factor. Given a sequence of weights τ = τ 1 . . . τ n , those three functions are defined by:
Weighted Transducers for Robustness Verification Weighted-automata. When a C-transducer outputs only empty words, then its output component can be removed and we get what is called a C-automaton, which defines a function from words to costs. For C = Sum, this definition of Sum-automaton coincides with the classical notion weighted automata over the semiring (N ∪ {+∞}, min, +) from [15].
Robustness problems. We study the following three fundamental problems related to robustness for three different aggregator functions C ∈ {Sum, Mean, DSum}. Given a threshold ν ∈ Q, a C-transducer T and a regular language L, a word u ∈ dom(T ) is said to be ν-robust
In other words, all its rewritings of cost ν at most are in L. A language N ⊆ Σ * is said to be ν-robust if N ∩ dom(T ) contains only ν-robust words. Finally, the ν-robust kernel of T is the set Rob T (ν, L) of ν-robust words:
We prove that as the error threshold grows, so does the robust kernel.
We are in a position to formally define the three key problems studied in this paper. For these definitions, we let C ∈ {Sum, Mean, DSum}.
Given a C-transducer T , a regular language N ⊆ Σ * as an NFA, a threshold ν ∈ Q ≥0 and a language L ⊆ Σ * as a DFA, the robust inclusion problem is to decide whether N ⊆ Rob T (ν, L), i.e. whether T ≤ν (N ) ⊆ L.
Note that we consider our specification language L deterministically presented, for tractability. Problem 6 (Threshold Synthesis). Given a C-transducer T , a regular language N ⊆ Σ * as an NFA, and a regular language L ⊆ Σ * as a DFA, the threshold synthesis problem is to output a partition of the set of thresholds Q ≥0 = G B into sets G and B of good and bad thresholds, i.e.
As direct consequence of Proposition 4, the sets G and B are intervals of values, that is for all
For the cases where we provide algorithms for solving the non-emptiness of the robust kernel, we also succeed in synthesizing the robust kernel as an automaton.
Given an instance of the threshold synthesis problem, we show how to compute the interval of good thresholds G and the interval of bad thresholds B in PTime for all the three measures we consider. As a corollary, we show that the robust inclusion problem for Sum, Mean, DSum measures is in PTime. In the following, we assume that N = dom(T ). This is w.l.o.g. as transducers are closed (in polynomial time) under regular domain restriction (using a product construction of T with the automaton for N ). With this assumption, the set of good thresholds G becomes Then, we associate with every transducer T and property L given by some DFA A (assumed to be complete), a graph called the weighted-graph associated with T and A, and denoted by G T,A . Intuitively, G T,A is obtained by first taking the synchronised product of T and A (where A is simulated on the outputs of T ) and then by projecting this product on the inputs.
Formally, given T = (Q, Q I , Q F , ∆, W) and A = (P, p I , P F , δ), the synchronised product
is the set of edges e = (q, p) → (q , p ) such that there exists a ∈ Σ ε and a transition t = (q, a, u, q ) ∈ ∆ such that p = δ(p, u) where δ has been extended to words in the expected way. We say that e is compatible with t.
For all e ∈ E, W (e) = min{W(t) | e is compatible with some t ∈ ∆}. Additionally, we note
the set of final vertices of this graph. Given a path π in this graph as a sequence of edges e 1 . . . e n , we let C(π) = C(W (e 1 ) . . . W (e n )).
The following lemma establishes some connection between ν T,L and the paths of G T,A .
Lemma 9. The infimum cost of paths from a vertex in
Proof. We first show that any path π from V I to V F satisfies C(π) ≥ ν T,L . Take such a path. By construction of G T,A , there exists an input word u 1 ∈ dom(T ), some output word u 2 / ∈ L and an accepting run
Weighted Transducers for Robustness Verification the minimal value of all accepting runs of T over (u 1 , u 2 ), we have C(r) ≥ C T (u 1 , u 2 ) and u 1 is not robust for threshold C T (u 1 , u 2 ), a fortiori for threshold C(r), from which we get
Suppose that ν T,L is strictly smaller than this infinimum (that we denote m) and take some rational number ν such that ν T,L < ν < m. Since ν T,L < ν, it is a bad threshold which means that there exists u 1 ∈ dom(T ) such that u 1 ∈ Rob T (ν, L). Hence there exists u 2 ∈ L such that C T (u 1 , u 2 ) ≤ ν, and by definition of G T,A , there exists a path π from V I to V F of value C(π) ≤ ν. This contradicts the fact that ν < m by definition of m. Hence, ν T,L = m, concluding the proof.
The next lemma establishes that the infimum of values of paths between two sets of states in a weighted graph can be computed in PTime and it is also decidable in PTime if the infimum is realized by a path, for all the three measures considered in this paper. As a direct corollary of this lemma we obtain the main theorem of the section. The full proof can be found in Appendix.
Lemma 10. For a weighted graph G = (V, E, W : E → Q ≥0 ), a set of sources V I ⊆ V and a set of targets V F ⊆ V , the infimum of the weights of paths from V I to V F can be computed in PTime for all C ∈ {Sum, DSum, Mean}. Moreover, we can decide in PTime if this infimum is realizable by a path.
First, if no state of V F are reachable from some state of V I , we have ν T,L = +∞. Otherwise we use different procedures, depending on the aggregator C.
For Sum, the infimum can be computed in Ptime using Dijkstra algorithm and it is always feasible. For Mean, we first note that the infimum is the Mean value of either a simple path or the value of a reachable cycle that can be iterated before moving to some target. In the latter case, the infimum is not feasible but can be approximated as close as possible by iterating the cycle. So, the infimum is feasible iff it is the Mean value of a simple path. The minimal Mean values amongst simple paths and cycles can be computed in Ptime with dynamic programming thanks to [18]. For DSum, Theorem 1 of [5] provides a PTime algorithm that computes for all v ∈ V , the infimum of DSum values x v of paths reaching the target V F from v.
Theorem 11. For a given C-transducer T , a language N ⊆ Σ * given as an NFA and L ⊆ Σ * given as a DFA, the set partition of good and bad thresholds (G, B) for C ∈ {Sum, DSum, Mean} can be computed in PTime.
Proof. First, we restrict the domain of T to N by taking the product of T and the automaton for N (simulated over the input of T ). Then, according to Lemma 10, we can compute in PTime the value ν T,L . This value is the infimum of B. If this infimum is feasible then the interval B is left closed and equal to [ν T,L , +∞) while G = [0, ν T,L ), and on the contrary, if this infimum is not feasible, then B is left open and equal to (ν T,L , +∞), while G = [0, ν T,L ]. Note that when ν T,L = 0 and is feasible, then G = [0, 0) = ∅.
As a direct consequence, the robust inclusion problem for a threshold ν can be solved by checking if ν ∈ G, and so we have the following corollary.
In this section, we show that the robust kernel is regular for Sum-transducers, and checking its emptiness is PSpace-complete. For Mean, we show that it is not necessarily regular, and checking its emptiness is undecidable. For DSum, we conjecture that the robust kernel is non-regular and give sufficient condition under which it is regular and computable, implying decidability of its emptiness.
To show robust kernel regularity, we rely on the construction of Theorem 2 of [2] in the context of weighted automata over the semiring (N ∪ {+∞}, min, +). The following lemma, use the same automata construction and provides an upper bound on the number of states required to denote a threshold language with a DFA.
Lemma 13. Let U be an n state Sum-automaton and ν ∈ N. The threshold language L ν (U ) = {w | U (w) ≥ ν}, where U (w) is defined as +∞ if there is no accepting run on w, otherwise as the minimal sum of the weights along accepting runs on w, is regular. Moreover L ν (U ) is recognized by a DFA with O (ν + 2) n states.
Proof. First, let assume that U has universal domain (i.e. any word has some accepting run), otherwise we complete it by assigning value ν to each word of its complement.
Then, U (w) ≥ ν iff all the accepting runs on w have value at least ν. We design a DFA D that accepts exactly those words. Since the weights of U are non-negative, D just has to monitor the sum of all runs up to ν, by counting in its states. If Q is the set of states of U , the set of states of D is 2 Q×{0,...,ν-1,ν + } , where ν + intuitively means any value ≥ ν. We extend natural addition to X = {0, . . . , ν -1, ν + } by letting a + b = ν + iff a = ν + , or b = ν + , or a + b ≥ ν. Then, D is obtained by subset construction: there is a transition P σ -→ P in D iff P = {(q , i + j) | (q, i) ∈ P ∧ q σ|j --→ U q }. A state P is accepting if P ∩ (Q \ F ) × {0, . . . , ν -1} = ∅, where F are the accepting states of U .
Though simple, the latter construction does not give the claimed complexity, as the number of states of D is 2 nν . But the following simple observation allows us to get a better state complexity. Consider an input word of the form uv. If after reading u, D reaches some state P such that for some state q, there exists (q, i), (q, j) ∈ P such that i < j, then if there is an accepting run of U from q on v, with sum s, there is an accepting run on uv with sum i + s and one with sum j + s. Therefore if i + s ≥ ν, then j + s ≥ ν and the pair (q, j) is useless in P . So, we can keep only the minimal elements in the states of D, where minimality is defined with respect to the partial order (q, i) (p, j) if q = p and i ≤ j. Let us call D opt the resulting "optimised" DFA. Its states can be therefore seen as functions from Q to {0, . . . , ν -1, ν + }, so that we get the claimed state-complexity. Lemma 14 (Robust language regularity). Let T be a Sum-transducer, ν ∈ N and L be regular language. The language of robust words Rob T (ν, L) is a regular language. Moreover, if L is given by a DFA with n L states and T has n T states, then Rob T (ν, L) is recognisable by a DFA with O (ν + 2) n T ×n L states.
Proof of this lemma is provided in the appendix.
C O N C U R 2 0 2 0 17:10 Weighted Transducers for Robustness Verification Theorem 15. Let T be a Sum-transducer, ν ∈ N given in binary and L a regular language given as a DFA. Then, it is PSpace-complete to decide whether there exists a robust word w ∈ Rob T (ν, L). The hardness holds even if ν is a fixed constant, T is letter-to-letterfoot_0 and io-unambiguousfoot_1 , and its weights are fixed constants in {0, 1}.
Proof. From Lemma 14, Rob T (ν, L) is recognisable by a DFA with O (ν + 2) n T ×n L states, where n T is the number of states of T and n A the number of states of the DFA defining L. Checking emptiness of this automaton can be done in PSpace (apply the standard NLogSpace emptiness checking algorithm on an exponential automaton that needs not be constructed explicitly, but whose transitions can be computed on-demand).
To show PSpace-hardness, we reduce the problem from [19] of checking the non-emptiness of the intersection of n regular languages given by n DFA A 1 , . . . , A n , over some alphabet Γ. In particular, we construct T , ν and a DFA A such that i L(A i ) = ∅ iff there exists a robust word with respect to T ,ν and L.
We define the alphabet as Σ = Γ ∪ {# 1 , . . . , # n , } where we assume that # 1 , . . . , # n , / ∈ Γ, and construct a transducer T which reads a word w of length k = |w| + 1 with w ∈ Γ * , and rewrites it into either itself, or (# i ) k for all i ∈ {1, . . . , n}. The identity rewriting has total weight 0 while the rewriting into # k i has total weight 1 if w ∈ L(A i ), and 0 otherwise. The transducer T is constructed as the disjoint union of n + 1 transducers T 1 , . . . , T n , T . For all i ∈ {1, . . . , n}, T i simulates A i on the input and outputs # i whenever it reads an input letter different from , with weight 0. When reading from an accepting state of A i , it outputs with weight 1, and if it reads from a non-accepting state, it outputs with weight 0. Finally, T just realizes the identify function with weight 0. Note that T has polynomial size in A 1 , . . . , A n and it is letter-to-letter and (input,output)-deterministic. Now we prove that a word w is robust iff w ∈ i L(A i ). Assume that there exists a robust word w for the property L = (Γ ∪ { })
* and threshold ν = 0. Equivalently, it means that for all rewritings α ∈ Σ * , if Sum T (w , α) ≤ 0 then α ∈ L. It is equivalent to say that all its rewritings α satisfies either Sum T (w , α) ≥ 1 or α ∈ L. By definition of T , it is equivalent to say that all rewritings α are such that either α ∈ (# i ) * • for some i and w ∈ L(A i ), or α = w . Since T necessarily rewrites w into w , as well as into (# 1 ) k , . . . , (# n ) k , where k = |w| + 1, the latter assumption is equivalent to saying that w ∈ L(A i ) for all i ∈ {1, . . . , n}, concluding the proof.
Let us first establish non-regularity of the robust kernel.
Lemma 16. Given a regular language L, a Mean-transducer T and ν ∈ Q ≥0 , the language Rob T (ν, L) is not necessarily regular, but recursive.
Proof. Consider the language L = {w | ∃i ∈ N : w(i) = a} on the alphabet Σ = {a, b}, i.e. the set of words on Σ that contain at least one a. Now, consider a (one state) transducer T that can non-deterministically copy letters or change the current letter from a to b with weight one. Now, if we fix ν to be equal to 1 2 , then all the translations of w by T of cost less than
We describe an evaluation of the ideas presented thus far and their application to two case studies: one involving robustness of control strategies to human mistakes and the other involving glucose values for patients with type-1 diabetes. We have implemented in Python the threshold synthesis problem (Problem 6) for the discounted and average costs. Our implementation supports the specification of a language L specified as an NFA, a weighted transducer T and a property P specified as some DFA. The implementation is available upon request.
An industrial motor operates under many gears g 1 , . . . , g 5 . Under fault, the human operator must take control of the machine and achieve the following: If the system goes into a fault the operator must ensure that (a) the system is immediately set in gears 3 -5. Subsequently, for the next 5 cycles: (b) it must never go to gear g 1 or g 2 ; and (c) must shift and stay at a higher gear g 4 or g 5 after the 5 th cycle until the fault is resolved.
Figure 3 shows a finite state machine P that accepts all words satisfying this property: fault is not in the operator's control but g 1 , . . . , g 5 are operator actions. Consider that the operator can perform this task in two different ways: σ 1 : fault g 4 g 4 g 4 g 5 g 5 versus σ 2 : fault g 3 g 3 g 3 g 3 g 4 . The input σ 1 induces the run s, s 0 , t 1 , t 2 , t 3 , r 4 , r 5 whereas the input σ 2 induces the run s, s 0 , s 1 , s 2 , s 3 , s 4 , t 5 . Both σ 1 , σ 2 satisfy the property of interest and as such there is nothing to choose one over the other. Suppose the human operator can make mistakes, especially since they are under stress. We will consider that the operator can substitute a command for gear g i with g i-1 (for i > 1) or g i+1 (for i < 5). We use a weighted transducer T 0 shown in Figure 4 to model these substitutions. The transducer defines possible ways in which a string σ can be converted to σ with a notion of cost for the conversion. In this example we consider two notions of cost: the DSum-cost, and the Mean-cost. These costs now allow us to compare σ 1 versus σ 2 . For instance, under both notions we will discover that σ 1 is much more robust than σ 2 . The robustness of σ 1 under both cost models is ∞ since any change to σ 1 under the transducer continues to satisfy the desired property. On the other hand σ 2 has a finite robustness, since operator mistakes can cause violations.
The use of a transducer allows for a richer specification of errors. For instance, transducer T 2 in Fig. 4 shows a model of "bounded" number of mistakes that assume that the operator makes at most 2 mistakes whereas T 3 in Fig. 4 shows a model with "bursty" mistakes that C O N C U R 2 0 2 0 17:14 Weighted Transducers for Robustness Verification
id, 0
id, 0
id, 0
id, 0
Figure 4 Transducers modeling potential human operator mistakes along with their costs: T0 allows arbitrarily many mistakes whereas T1 restricts the number of mistakes to at most 2, whereas T2 models a "bursty" set of mistakes. The edge a | b, w denotes a replacement of the letter a by b with a cost w. For convenience T2 uses an transition that can be removed. assume that mistakes occur in bursts of at least 2 but at most 3 mistakes at a time. These models are useful in capturing fine grained assumptions about errors that are often the case in the study of human error or errors in physical systems. Using the prototype implementation, we report on the robustness of various inputs for this motivating example under the three transducer error models. The property P is as shown in Figure 3 and the transducers T 0 -T 2 are as shown in Fig. 4. Table 1 reports the robustness values for various input strings and the running time. We note that while our approach takes about 0.3 seconds for a string of length 50, the prototype can be made much more efficient to reduce the time to compute robustness. Also we note that discounted sum becomes smaller as the strings grow larger while the average robustness value does not. We conclude that average robustness is a more useful measure due to this property in this particular example.
We will now apply our ideas to the robust pattern matching problem for analyzing clinical data for patients with type-1 diabetes. People with type-1 diabetes are required to monitor their blood glucose levels periodically using devices such as continuous glucose monitors (CGMs). Data from CGMs is uploaded online and available for review by clinicians during periodic doctor visits. Many applications such as Medtronic Carelink(tm) support the automatic upload and visualization of this data by clinicians. Physicians are commonly interested in analyzing the data to reveal potentially dangerous patterns of blood glucose levels: (a) Prolonged Hypoglycemia (P1): Do the blood glucose levels stay below 70 mg/dl (hypoglycemia) for more than 3 hours continuously?foot_2 (b) Prolonged Hyperglycemia (P2): Do the blood glucose levels remain above 300 mg/dl (hyperglycemia) for more than 3 hours continuously? 4 ; and (c) Rebound Hyperglycemia (P3): Do the blood glucose levels go below 70 mg/dl and then rise rapidly up to 300 mg/dl or higher within 2 hours?foot_4 Note that these patterns specify "bad" events that should not happen. A straightforward and strict pattern matching approach based on specifying the properties above will "hide" potentially bad scenarios that "nearly" match the desired pattern for two main reasons. First, the CGM can be noisy and inaccurate in a way that depends on the actual blood glucose value measured when it was last calibrated. (see Figure 5 and more detailed description below). Secondly, the cutoffs involved such as 70 mg/dl and 3 hours are not "set stone". For instance, a clinician will consider a scenario wherein the patient's blood glucose levels stays at 71 mg/dl for 2.75 hours as a serious case of prolonged hypoglycemia even though such a scenario would not satisfy the property P1.
We propose to solve the approximate "pattern matching" problem. I.e, given a string w, a transducer T and a language L, we are looking for a word w such that w ∈ L and C T (w , w) is as small as possible. In other words, we solve the threshold synthesis problem (Problem 6) for a language L that is the complement of P1 (P2 or P3).
We partition the range of CGM outputs [40, 400] mg/dl into intervals of size 10 mg/dl over the range [40, 80] mg/dl and 20 mg/dl intervals over the remaining range [80, 400] mg/dl. This yields a finite alphabet Σ where |Σ| = 20. For instance a 60,70 ∈ Σ represents a range [60, 70]mg/dl. CGMs provide a reading periodically at 5 minute intervals. This yields a string where each letter describes the interval that contains the glucose value.
Transducer. The CGM error model is given by a transducer that considers possible errors that a CGM can make (see Fig. 5). The transducer has four states: (a) Not Calib denoting that no calibration has happened, (b) Calib: denoting a calibration event in the past, (c) DropoutNC: a sensor drops out under the non calibrated mode and (d) DropoutC: a calibration event has happened and sensor drops out. The cost of changing a reading in the range [lb, ub] to one in the range [lb , ub ] is denoted by a function cost(lb, ub, lb , ub ) These costs are set to be higher for ranges [lb, ub] that are close to hypoglycemia. Also note that we can model calibration events and the doubling of costs if the sensor is in the calibrated mode.
Property Specifications. We specify the three different properties described above formally using finite state machines over the alphabet Σ as defined above. The prolonged hypoglycemia property can be written as a regular expression: Σ * (a 40,50 + a 50,60 + a 60,70 ) 36 Σ * which can be easily translated into an NFA with roughly 38 states. The number 36 represents a period of 180 minutes since CGM values are sampled at 5 minute intervals. Similarly, the other two properties are also easily expressed as NFAs.
Finally, we compose the transducer model with the properties P1-P3 individually and calculate mean robustness. More precisely, for each sequence of measures w, we compute the minimal threshold ν such that w can be rewritten by T at mean cost ν into some w satisfying P1 (and P2, P3 respectively). The discounted sum robustness is not useful in this situation since the patterns can match approximately anywhere in the middle of a trace. Also, in most cases the discounted sum robustness value was very close to zero for any discount factor < 1 or became forbiddingly large for discount factors slightly larger than 1, due to the large size of the traces.
Patient Data. We used actual patient data involving nearly 50 patients with type-1 diabetes undergoing a clinical trial of an artificial pancreas device, and nearly 40 nights of data per patient, leading to an overall 2032 nights. Each night roughly corresponds to a 12 hour period when CGM data was recorded [20]. This is converted to a string of size 140 (or slightly larger, depending on how many calibration events occurred). The threshold synthesis problem (Problem 6) was solved for each of the input strings, and the results were sorted by the threshold robustness value for properties P1-P3. Table 2 shows for each property, the total time taken to complete the analysis of the full patient data, and the number of matches obtained corresponding to various threshold values. As the table reveals, no single trace matches any of the properties perfectly. However, our approach is more nuanced, and thus, allows us to find numerous approximate matches that can be sorted by their robustness threshold values. Note that many of the input traces yield a threshold value of ∞: this signifies that no possible translation as specified by the transducer can cause the property to hold.
Figure 6 shows two of the approximate pattern matches obtained with a small robustness value. Notice that the CGM values on the left do not satisfy the criterion for a "prolonged hypoglycemia" for 3 hours (P1) in a strict sense due to a single point at the end of the trace that is slightly above the 70 mg/dl threshold. Nevertheless, our approach assigns this trace a very low robustness. Likewise, the plot on the right shows a rapid rise from a hypoglycemia to a hyperglycemia within 120 minutes (P3) towards the beginning, except that the peak value just falls short of the threshold of 300 mg/dl. Note that related work in the area of monitoring cyber-physical systems (CPS) mentioned earlier [16,14,12,1] can be used to perform approximate pattern matching using robustness of temporal properties over hybrid traces. However, we note important differences that are achieved due to the theory developed in this paper. For one, the use of a transducer can provide a nuanced model of how errors transform a trace, wherein the transformation itself changes based on the transducer state. A detailed transducer model of CGM errors remains beyond the scope of this study but will likely be desirable for applications to the analysis of patterns in type-1 diabetes data.
In conclusion, we have shown how notions of robustness can be defined through weighted transducers along with approaches for solving and kernel synthesis problems for various cost aggregators such as Sum, DSum and Mean. In the future, we will investigate these notions for richer classes of systems including timed and hybrid systems. We also plan to investigate connections to robust learning of automata from examples.
w 1 ∈ Rob T (ν, L). The run r is called dangerous if |r| ≥ n and DSum(r) ≤ ν -B n . A dangerous run r can possibly be extended to a bad run rr . It is possible iff there exists a continuation r of r such that the of rr is not in L. Note that the cost of rr does not matter because the largest value r can achieve is B n , keeping DSum(rr ) smaller than ν. Hence, when a dangerous run is met, only a regular property has to be tested to extend it to a bad run. We exploit this idea in the automata construction. Namely, A n will accept words for which there exists a bad run of length n at most, or a dangerous run of length n which can be extended to a bad run.
• Automata construction. Let Runs ≤n T be the runs of T of length at most n, and Q its set of states. We assume that for all (w 1 , w 2 ) ∈ R T , w 2 ∈ L holds. This can be ensured by taking the synchronised product of T (on its outputs) with an automaton recognizing the complement of L. Let us now build the NFA A n . Its set of states is Runs ≤n T ∪ Q. Its transitions are defined as follows: for all T -runs r of length n -1 at most ending in some state q, for all σ ∈ Σ ε , if there exists a transition t of T from state q on reading σ, then we create the transition r σ -→ rt in A n . From any run r of length n, we consider two cases: if r is not dangerous, then r has no outgoing transitions in A n . If r is a dangerous run, then we add some ε-transition to its last state: r ε -→ p where p is the last state of r. Finally, we add a transition from any state q to any state q on σ in A n whenever there is a transition from q to q on input σ in T . Accepting states are bad runs of Runs ≤n T and accepting states of T . • Correctness. Let us show that the family A n satisfies the requirements of the lemma. First, we show that L(A n ) ⊆ L(A n+1 ). Let w ∈ L(A n ) and ρ some accepting run of A n on w. To simplify the notations, we assume here in this proof that runs of A n , A n+1 and T are just sequences of states rather than sequences of transitions. By definition of A n , ρ can be decomposed into two parts ρ 1 ρ 2 such that ρ 1 ∈ (Runs ≤n T ) * and ρ 2 ∈ Q * with an -transition from the last state of ρ 1 to the first of ρ 2 . We consider two cases. If |ρ 2 | = 0, then ρ = ρ 1 and by definition of A n+1 , ρ is still an accepting run of A n+1 . In the other case, there is a dangerous run r of T such that ρ 1 can be written ρ 1 = r[: 1]r[: 2] . . . r[: n] where r[: i] is the prefix of r up to position i, and ρ 2 = q 1 q 2 . . . q k is a proper run of T . Note that q 1 is the last state of r by construction of A n . Moreover, rρ 2 is bad. Since r was dangerous at step n, we also get that rq 2 is dangerous at step n + 1, in the sense that |rq 2 | = n + 1 and DSum(rq 2 ) ≤ ν -B n+1 , by definition of B n+1 and the fact that DSum(r) ≤ ν -B n . So, we get that the sequence of states ρ 1 .(rq 2 ).q 2 . . . q k is a run of A n+1 on w is accepting in A n+1 (note that rq 2 here is a state of A n+1 and there is an -transition from (rq 2 ) to q 2 ), concluding the first part of the proof. Now, suppose that ν is -isolated for some . Then, take n * as given by Lemma 18 and let us show that Rob T (ν, L) ∩ dom(T ) ⊆ L(A n * ) (the other inclusion has just been proved for all n). Let w ∈ dom(T ) such that w ∈ Rob T (ν, L). There exists (w 1 , w 2 ) ∈ R T and an accepting run r of T on it such that DSum(r) ≤ ν and w 2 ∈ L. In other words, r is bad. If
A transducer is letter-to-letter if ∆ ⊆ Q × Σ × Σ × Q.
For all word pairs (w1, w2), there exists at most one run of T on w1 outputting w2.
Such an event can lead to dangerous (and silent) nighttime seizures.
Such an event can lead to a potentially dangerous condition called diabetic ketacidosis.
Rebound hyperglycemia can lead to large future swings in the blood glucose level, raising the burden on the patient for managing their blood glucose levels.