@inproceedings{7348,
abstract = {The monitoring of event frequencies can be used to recognize behavioral anomalies, to identify trends, and to deduce or discard hypotheses about the underlying system. For example, the performance of a web server may be monitored based on the ratio of the total count of requests from the least and most active clients. Exact frequency monitoring, however, can be prohibitively expensive; in the above example it would require as many counters as there are clients. In this paper, we propose the efficient probabilistic monitoring of common frequency properties, including the mode (i.e., the most common event) and the median of an event sequence. We define a logic to express composite frequency properties as a combination of atomic frequency properties. Our main contribution is an algorithm that, under suitable probabilistic assumptions, can be used to monitor these important frequency properties with four counters, independent of the number of different events. Our algorithm samples longer and longer subwords of an infinite event sequence. We prove the almost-sure convergence of our algorithm by generalizing ergodic theory from increasing-length prefixes to increasing-length subwords of an infinite sequence. A similar algorithm could be used to learn a connected Markov chain of a given structure from observing its outputs, to arbitrary precision, for a given confidence. },
author = {Ferrere, Thomas and Henzinger, Thomas A and Kragl, Bernhard},
booktitle = {28th EACSL Annual Conference on Computer Science Logic},
isbn = {9783959771320},
issn = {1868-8969},
location = {Barcelona, Spain},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Monitoring event frequencies}},
doi = {10.4230/LIPIcs.CSL.2020.20},
volume = {152},
year = {2020},
}
@article{7426,
abstract = {This paper presents a novel abstraction technique for analyzing Lyapunov and asymptotic stability of polyhedral switched systems. A polyhedral switched system is a hybrid system in which the continuous dynamics is specified by polyhedral differential inclusions, the invariants and guards are specified by polyhedral sets and the switching between the modes do not involve reset of variables. A finite state weighted graph abstracting the polyhedral switched system is constructed from a finite partition of the state–space, such that the satisfaction of certain graph conditions, such as the absence of cycles with product of weights on the edges greater than (or equal) to 1, implies the stability of the system. However, the graph is in general conservative and hence, the violation of the graph conditions does not imply instability. If the analysis fails to establish stability due to the conservativeness in the approximation, a counterexample (cycle with product of edge weights greater than or equal to 1) indicating a potential reason for the failure is returned. Further, a more precise approximation of the switched system can be constructed by considering a finer partition of the state–space in the construction of the finite weighted graph. We present experimental results on analyzing stability of switched systems using the above method.},
author = {Garcia Soto, Miriam and Prabhakar, Pavithra},
issn = {1751570X},
journal = {Nonlinear Analysis: Hybrid Systems},
number = {5},
publisher = {Elsevier},
title = {{Abstraction based verification of stability of polyhedral switched systems}},
doi = {10.1016/j.nahs.2020.100856},
volume = {36},
year = {2020},
}
@article{6761,
abstract = {In resource allocation games, selfish players share resources that are needed in order to fulfill their objectives. The cost of using a resource depends on the load on it. In the traditional setting, the players make their choices concurrently and in one-shot. That is, a strategy for a player is a subset of the resources. We introduce and study dynamic resource allocation games. In this setting, the game proceeds in phases. In each phase each player chooses one resource. A scheduler dictates the order in which the players proceed in a phase, possibly scheduling several players to proceed concurrently. The game ends when each player has collected a set of resources that fulfills his objective. The cost for each player then depends on this set as well as on the load on the resources in it – we consider both congestion and cost-sharing games. We argue that the dynamic setting is the suitable setting for many applications in practice. We study the stability of dynamic resource allocation games, where the appropriate notion of stability is that of subgame perfect equilibrium, study the inefficiency incurred due to selfish behavior, and also study problems that are particular to the dynamic setting, like constraints on the order in which resources can be chosen or the problem of finding a scheduler that achieves stability.},
author = {Avni, Guy and Henzinger, Thomas A and Kupferman, Orna},
issn = {03043975},
journal = {Theoretical Computer Science},
pages = {42--55},
publisher = {Elsevier},
title = {{Dynamic resource allocation games}},
doi = {10.1016/j.tcs.2019.06.031},
volume = {807},
year = {2020},
}
@inproceedings{7505,
abstract = {Neural networks have demonstrated unmatched performance in a range of classification tasks. Despite numerous efforts of the research community, novelty detection remains one of the significant limitations of neural networks. The ability to identify previously unseen inputs as novel is crucial for our understanding of the decisions made by neural networks. At runtime, inputs not falling into any of the categories learned during training cannot be classified correctly by the neural network. Existing approaches treat the neural network as a black box and try to detect novel inputs based on the confidence of the output predictions. However, neural networks are not trained to reduce their confidence for novel inputs, which limits the effectiveness of these approaches. We propose a framework to monitor a neural network by observing the hidden layers. We employ a common abstraction from program analysis - boxes - to identify novel behaviors in the monitored layers, i.e., inputs that cause behaviors outside the box. For each neuron, the boxes range over the values seen in training. The framework is efficient and flexible to achieve a desired trade-off between raising false warnings and detecting novel inputs. We illustrate the performance and the robustness to variability in the unknown classes on popular image-classification benchmarks.},
author = {Henzinger, Thomas A and Lukina, Anna and Schilling, Christian},
booktitle = {24th European Conference on Artificial Intelligence},
location = {Santiago de Compostela, Spain},
title = {{Outside the box: Abstraction-based monitoring of neural networks}},
year = {2020},
}
@inproceedings{7808,
abstract = {Quantization converts neural networks into low-bit fixed-point computations which can be carried out by efficient integer-only hardware, and is standard practice for the deployment of neural networks on real-time embedded devices. However, like their real-numbered counterpart, quantized networks are not immune to malicious misclassification caused by adversarial attacks. We investigate how quantization affects a network’s robustness to adversarial attacks, which is a formal verification question. We show that neither robustness nor non-robustness are monotonic with changing the number of bits for the representation and, also, neither are preserved by quantization from a real-numbered network. For this reason, we introduce a verification method for quantized neural networks which, using SMT solving over bit-vectors, accounts for their exact, bit-precise semantics. We built a tool and analyzed the effect of quantization on a classifier for the MNIST dataset. We demonstrate that, compared to our method, existing methods for the analysis of real-numbered networks often derive false conclusions about their quantizations, both when determining robustness and when detecting attacks, and that existing methods for quantized networks often miss attacks. Furthermore, we applied our method beyond robustness, showing how the number of bits in quantization enlarges the gender bias of a predictor for students’ grades.},
author = {Giacobbe, Mirco and Henzinger, Thomas A and Lechner, Mathias},
booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
isbn = {9783030452360},
issn = {16113349},
location = {Dublin, Ireland},
pages = {79--97},
publisher = {Springer Nature},
title = {{How many bits does it take to quantize your neural network?}},
doi = {10.1007/978-3-030-45237-7_5},
volume = {12079},
year = {2020},
}