Consider a fixed number of disjoint regular languages L_1,…,L_k ⊆ Σ^*. A classifier for L_1,…,L_k is a transducer that receives each moment t in time an input letter σ_t ∈ Σ and outputs an index in {1,…,k} such that if the word σ_1 ⋯ σ_t, generated so far, is in some (unique) language L_i, then this index is i. Classifiers arise naturally in runtime monitoring and online stream processing, where a system must continuously determine which of several specifications or behaviors is currently being realized. The problem of generating classifiers of minimal size has been well studied. In many applications, the input alphabet is of the form 2^P, for a finite set P of signals. There, the complexity of classification stems not only from the languages but also from the presence of uncertainty, namely when the valuation to some signals may not be known. We introduce and study classification under uncertainty, where the input words may be partially observed. We consider three sources for uncertainty: (1) Given: the input to the problem specifies which signals may be sensed after each behavior. (2) Privacy: the input includes a list of secret behaviors, and the classifier should restrict sensing so that secrets are not revealed. (3) Budget: Sensing of signals incurs a cost, which the classifier should minimize.

Abstract In the synthesis problem, we are given a specification, and we automatically generate a system that satisfies the specification in all environments. We introduce and study synthesis with guided environments (SGE, for short), where the system may harness the knowledge and computational power of the environment during the interaction. The underlying idea in SGE is that in many settings, in particular when the system serves or directs the environment, it is of the environment’s interest that the specification is satisfied, and it would follow the guidance of the system. Thus, while the environment is still hostile, in the sense that the system should satisfy the specification no matter how the environment assigns values to the input signals, in SGE the system assigns values to some output signals and guides the environment via programs how to assign values to other output signals. A key issue is that these assignments may depend on input signals that are hidden from the system but are known to the environment, using programs like “copy the value of the hidden input signal x to the output signal y .” SGE is thus particularly useful in settings where the system has partial visibility. We solve the problem of SGE, show its superiority with respect to traditional synthesis, and study theoretical aspects of SGE, like the complexity (memory and domain) of programs used by the system, as well as the connection of SGE to synthesis of (possibly distributed) systems with partial visibility.

We study automatic synthesis of systems that interact with their environment and maintain privacy against an observer to the interaction. The system and the environment interact via sets $I$ and $O$ of input and output signals. The input to the synthesis problem contains, in addition to a specification, also a list of secrets, a function $cost: I\cup O\rightarrow\mathbb{N}$, which maps each signal to the cost of hiding it, and a bound $b\in\mathbb{N}$ on the budget that the system may use for hiding of signals. The desired output is an $(I/O)$-transducer $T$ and a set $H\subseteq I\cup O$ of signals that respects the bound on the budget, thus $\sum_{s\in H} cost(s)\leq b$, such that for every possible interaction of $T$, the generated computation satisfies the specification, yet an observer, from whom the signals in $H$ are hidden, cannot evaluate the secrets. We first show that the problem's complexity is 2EXPTIME-complete for specifications and secrets in LTL, making it no harder than synthesis without privacy requirements. We then analyze the complexity further, isolating the two aspects that do not exist in traditional synthesis: the need to hide secret values and the need to choose the set $H$. We do this by studying settings in which traditional synthesis is solvable in polynomial time -- when the specification formalism is deterministic automata and when the system is closed -- and show that each of these aspects adds an exponential blow-up in complexity. We continue and study bounded synthesis with privacy, where the input includes a bound on the synthesized transducer size, as well as a variant of the problem in which the observer has knowledge, either about the specification or about the system, which can be helpful in evaluating the secrets. Additionally, we study certified privacy, where the synthesis algorithm provides certification that the secrets remain hidden.

We study three levels in a hierarchy of nondeterminism: A nondeterministic automaton $\mathcal{A}$ is determinizable by pruning (DBP) if we can obtain a deterministic automaton equivalent to $\mathcal{A}$ by removing some of its transitions. Then, $\mathcal{A}$ is history deterministic (HD) if its nondeterministic choices can be resolved in a way that only depends on the past. Finally, $\mathcal{A}$ is semantically deterministic (SD) if different nondeterministic choices in $\mathcal{A}$ lead to equivalent states. Some applications of automata in formal methods require deterministic automata, yet in fact can use automata with some level of nondeterminism. For example, DBP automata are useful in the analysis of online algorithms, and HD automata are useful in synthesis and control. For automata on finite words, the three levels in the hierarchy coincide. We study the hierarchy for Büchi, co-Büchi, and weak automata on infinite words. We show that the hierarchy is strict, study the expressive power of the different levels in it, as well as the complexity of deciding the membership of a language in a given level. Finally, we describe a probability-based analysis of the hierarchy, which relates the level of nondeterminism with the probability that a random run on a word in the language is accepting. We relate the latter to nondeterministic automata that can be used when reasoning about probabilistic systems.

Abstract We study automatic synthesis of systems that interact with their environment and maintain privacy against an observer to the interaction. The system and the environment interact via sets I and O of input and output signals. The input to the synthesis problem contains, in addition to a specification, also a list of secrets , a function $$\textsf{cost}: I \cup O \rightarrow {\mathbb N}$$ cost : I ∪ O → N , which maps each signal to the cost of hiding it, and a bound $$b \in {\mathbb N}$$ b ∈ N on the budget that the system may use for hiding of signals. The desired output is an ( I / O )-transducer $$\mathcal {T}$$ T and a set $$\mathcal {H} \subseteq I \cup O$$ H ⊆ I ∪ O of signals that respects the bound on the budget, thus $$\sum _{s \in \mathcal {H}} \textsf{cost}(s) \le b$$ ∑ s ∈ H cost ( s ) ≤ b , such that for every possible interaction of $$\mathcal {T}$$ T , the generated computation satisfies the specification, yet an observer from which the signals in $$\mathcal {H}$$ H are hidden, cannot evaluate the secrets. We first show that the complexity of the problem is 2EXPTIME-complete for specifications and secrets in LTL, thus it is not harder than synthesis with no privacy requirements. We then analyze the complexity of the problem more carefully, isolating the two aspects that do not exist in traditional synthesis, namely the need to hide the value of the secrets and the need to choose the set $$\mathcal {H}$$ H . We do this by studying settings in which traditional synthesis can be solved in polynomial time – when the specification formalism is deterministic automata and when the system is closed, and show that each of the two aspects involves an exponential blow-up in the complexity. We continue and study bounded synthesis with privacy , where the input also includes a bound on the size of the synthesized transducer, as well as a variant of the problem in which the observer has knowledge about the specification , which can be helpful in evaluating the secrets. We study the effect of both variants on the different aspects of the problem and provide algorithms with a tight complexity.

We study three levels in a hierarchy of nondeterminism: A nondeterministic automaton A is determinizable by pruning (DBP) if we can obtain a deterministic automaton equivalent to A by removing some of its transitions. Then, A is good-for-games (GFG) if its nondeterministic choices can be resolved in a way that only depends on the past. Finally, A is semantically deterministic (SD) if different nondeterministic choices in A lead to equivalent states. Some applications of automata in formal methods require deterministic automata, yet in fact can use automata with some level of nondeterminism. For example, DBP automata are useful in the analysis of online algorithms, and GFG automata are useful in synthesis and control. For automata on finite words, the three levels in the hierarchy coincide. We study the hierarchy for Büchi, co-Büchi, and weak automata on infinite words. We show that the hierarchy is strict, study the expressive power of the different levels in it, as well as the complexity of deciding the membership of a language in a given level. Finally, we describe a probability-based analysis of the hierarchy, which relates the level of nondeterminism with the probability that a random run on a word in the language is accepting.

A regular language R of finite words induces three repetition languages of infinite words: the language lim(R), which contains words with infinitely many prefixes in R, the language ∞ R, which contains words with infinitely many disjoint subwords in R, and the language R^ω, which contains infinite concatenations of words in R. Specifying behaviors, the three repetition languages provide three different ways of turning a specification of a finite behavior into an infinite one. We study the expressive power required for recognizing repetition languages, in particular whether they can always be recognized by a deterministic Büchi word automaton (DBW), the blow up in going from an automaton for R to automata for the repetition languages, and the complexity of related decision problems. For lim R and ∞ R, most of these problems have already been studied or are easy. We focus on R^ω. Its study involves some new and interesting results about additional repetition languages, in particular R^#, which contains exactly all words with unboundedly many concatenations of words in R. We show that R^ω is DBW-recognizable iff R^# is ω-regular iff R^# = R^ω, and there are languages for which these criteria do not hold. Thus, R^ω need not be DBW-recognizable. In addition, when exists, the construction of a DBW for R^ω may involve a 2^{O(n log n)} blow-up, and deciding whether R^ω is DBW-recognizable, for R given by a nondeterministic automaton, is PSPACE-complete. Finally, we lift the difference between R^# and R^ω to automata on finite words and study a variant of Büchi automata where a word is accepted if (possibly different) runs on it visit accepting states unboundedly many times.