@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},
}
@inproceedings{6428,
abstract = {Safety and security are major concerns in the development of Cyber-Physical Systems (CPS). Signal temporal logic (STL) was proposedas a language to specify and monitor the correctness of CPS relativeto formalized requirements. Incorporating STL into a developmentprocess enables designers to automatically monitor and diagnosetraces, compute robustness estimates based on requirements, andperform requirement falsification, leading to productivity gains inverification and validation activities; however, in its current formSTL is agnostic to the input/output classification of signals, andthis negatively impacts the relevance of the analysis results.In this paper we propose to make the interface explicit in theSTL language by introducing input/output signal declarations. Wethen define new measures of input vacuity and output robustnessthat better reflect the nature of the system and the specification in-tent. The resulting framework, which we call interface-aware signaltemporal logic (IA-STL), aids verification and validation activities.We demonstrate the benefits of IA-STL on several CPS analysisactivities: (1) robustness-driven sensitivity analysis, (2) falsificationand (3) fault localization. We describe an implementation of our en-hancement to STL and associated notions of robustness and vacuityin a prototype extension of Breach, a MATLAB®/Simulink®toolboxfor CPS verification and validation. We explore these methodologi-cal improvements and evaluate our results on two examples fromthe automotive domain: a benchmark powertrain control systemand a hydrogen fuel cell system.},
author = {Ferrere, Thomas and Nickovic, Dejan and Donzé, Alexandre and Ito, Hisahiro and Kapinski, James},
booktitle = {Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control},
isbn = {9781450362825},
location = {Montreal, Canada},
pages = {57--66},
publisher = {ACM},
title = {{Interface-aware signal temporal logic}},
doi = {10.1145/3302504.3311800},
year = {2019},
}
@article{7109,
abstract = {We show how to construct temporal testers for the logic MITL, a prominent linear-time logic for real-time systems. A temporal tester is a transducer that inputs a signal holding the Boolean value of atomic propositions and outputs the truth value of a formula along time. Here we consider testers over continuous-time Boolean signals that use clock variables to enforce duration constraints, as in timed automata. We first rewrite the MITL formula into a “simple” formula using a limited set of temporal modalities. We then build testers for these specific modalities and show how to compose testers for simple formulae into complex ones. Temporal testers can be turned into acceptors, yielding a compositional translation from MITL to timed automata. This construction is much simpler than previously known and remains asymptotically optimal. It supports both past and future operators and can easily be extended.},
author = {Ferrere, Thomas and Maler, Oded and Ničković, Dejan and Pnueli, Amir},
issn = {0004-5411},
journal = {Journal of the ACM},
number = {3},
publisher = {ACM},
title = {{From real-time logic to timed automata}},
doi = {10.1145/3286976},
volume = {66},
year = {2019},
}
@inproceedings{7159,
abstract = {Cyber-physical systems (CPS) and the Internet-of-Things (IoT) result in a tremendous amount of generated, measured and recorded time-series data. Extracting temporal segments that encode patterns with useful information out of these huge amounts of data is an extremely difficult problem. We propose shape expressions as a declarative formalism for specifying, querying and extracting sophisticated temporal patterns from possibly noisy data. Shape expressions are regular expressions with arbitrary (linear, exponential, sinusoidal, etc.) shapes with parameters as atomic predicates and additional constraints on these parameters. We equip shape expressions with a novel noisy semantics that combines regular expression matching semantics with statistical regression. We characterize essential properties of the formalism and propose an efficient approximate shape expression matching procedure. We demonstrate the wide applicability of this technique on two case studies. },
author = {Ničković, Dejan and Qin, Xin and Ferrere, Thomas and Mateis, Cristinel and Deshmukh, Jyotirmoy},
booktitle = {19th International Conference on Runtime Verification},
isbn = {9783030320782},
issn = {0302-9743},
location = {Porto, Portugal},
pages = {292--309},
publisher = {Springer Nature},
title = {{Shape expressions for specifying and extracting signal features}},
doi = {10.1007/978-3-030-32079-9_17},
volume = {11757},
year = {2019},
}
@inproceedings{7232,
abstract = {We present Mixed-time Signal Temporal Logic (STL−MX), a specification formalism which extends STL by capturing the discrete/ continuous time duality found in many cyber-physical systems (CPS), as well as mixed-signal electronic designs. In STL−MX, properties of components with continuous dynamics are expressed in STL, while specifications of components with discrete dynamics are written in LTL. To combine the two layers, we evaluate formulas on two traces, discrete- and continuous-time, and introduce two interface operators that map signals, properties and their satisfaction signals across the two time domains. We show that STL-mx has the expressive power of STL supplemented with an implicit T-periodic clock signal. We develop and implement an algorithm for monitoring STL-mx formulas and illustrate the approach using a mixed-signal example. },
author = {Ferrere, Thomas and Maler, Oded and Nickovic, Dejan},
booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
isbn = {9783030296612},
issn = {16113349},
location = {Amsterdam, The Netherlands},
pages = {59--75},
publisher = {Springer Nature},
title = {{Mixed-time signal temporal logic}},
doi = {10.1007/978-3-030-29662-9_4},
volume = {11750},
year = {2019},
}
@inproceedings{299,
abstract = {We introduce in this paper AMT 2.0 , a tool for qualitative and quantitative analysis of hybrid continuous and Boolean signals that combine numerical values and discrete events. The evaluation of the signals is based on rich temporal specifications expressed in extended Signal Temporal Logic (xSTL), which integrates Timed Regular Expressions (TRE) within Signal Temporal Logic (STL). The tool features qualitative monitoring (property satisfaction checking), trace diagnostics for explaining and justifying property violations and specification-driven measurement of quantitative features of the signal.},
author = {Nickovic, Dejan and Lebeltel, Olivier and Maler, Oded and Ferrere, Thomas and Ulus, Dogan},
editor = {Beyer, Dirk and Huisman, Marieke},
location = {Thessaloniki, Greece},
pages = {303 -- 319},
publisher = {Springer},
title = {{AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic}},
doi = {10.1007/978-3-319-89963-3_18},
volume = {10806},
year = {2018},
}
@inproceedings{5959,
abstract = {Formalizing properties of systems with continuous dynamics is a challenging task. In this paper, we propose a formal framework for specifying and monitoring rich temporal properties of real-valued signals. We introduce signal first-order logic (SFO) as a specification language that combines first-order logic with linear-real arithmetic and unary function symbols interpreted as piecewise-linear signals. We first show that while the satisfiability problem for SFO is undecidable, its membership and monitoring problems are decidable. We develop an offline monitoring procedure for SFO that has polynomial complexity in the size of the input trace and the specification, for a fixed number of quantifiers and function symbols. We show that the algorithm has computation time linear in the size of the input trace for the important fragment of bounded-response specifications interpreted over input traces with finite variability. We can use our results to extend signal temporal logic with first-order quantifiers over time and value parameters, while preserving its efficient monitoring. We finally demonstrate the practical appeal of our logic through a case study in the micro-electronics domain.},
author = {Bakhirkin, Alexey and Ferrere, Thomas and Henzinger, Thomas A and Nickovicl, Deian},
booktitle = {2018 International Conference on Embedded Software (EMSOFT)},
isbn = {9781538655603},
location = {Turin, Italy},
pages = {1--10},
publisher = {IEEE},
title = {{Keynote: The first-order logic of signals}},
doi = {10.1109/emsoft.2018.8537203},
year = {2018},
}
@inproceedings{78,
abstract = {We provide a procedure for detecting the sub-segments of an incrementally observed Boolean signal ω that match a given temporal pattern ϕ. As a pattern specification language, we use timed regular expressions, a formalism well-suited for expressing properties of concurrent asynchronous behaviors embedded in metric time. We construct a timed automaton accepting the timed language denoted by ϕ and modify it slightly for the purpose of matching. We then apply zone-based reachability computation to this automaton while it reads ω, and retrieve all the matching segments from the results. Since the procedure is automaton based, it can be applied to patterns specified by other formalisms such as timed temporal logics reducible to timed automata or directly encoded as timed automata. The procedure has been implemented and its performance on synthetic examples is demonstrated.},
author = {Bakhirkin, Alexey and Ferrere, Thomas and Nickovic, Dejan and Maler, Oded and Asarin, Eugene},
isbn = {978-3-030-00150-6},
location = {Bejing, China},
pages = {215 -- 232},
publisher = {Springer},
title = {{Online timed pattern matching using automata}},
doi = {10.1007/978-3-030-00151-3_13},
volume = {11022},
year = {2018},
}
@inproceedings{144,
abstract = {The task of a monitor is to watch, at run-time, the execution of a reactive system, and signal the occurrence of a safety violation in the observed sequence of events. While finite-state monitors have been studied extensively, in practice, monitoring software also makes use of unbounded memory. We define a model of automata equipped with integer-valued registers which can execute only a bounded number of instructions between consecutive events, and thus can form the theoretical basis for the study of infinite-state monitors. We classify these register monitors according to the number k of available registers, and the type of register instructions. In stark contrast to the theory of computability for register machines, we prove that for every k 1, monitors with k + 1 counters (with instruction set 〈+1, =〉) are strictly more expressive than monitors with k counters. We also show that adder monitors (with instruction set 〈1, +, =〉) are strictly more expressive than counter monitors, but are complete for monitoring all computable safety -languages for k = 6. Real-time monitors are further required to signal the occurrence of a safety violation as soon as it occurs. The expressiveness hierarchy for counter monitors carries over to real-time monitors. We then show that 2 adders cannot simulate 3 counters in real-time. Finally, we show that real-time adder monitors with inequalities are as expressive as real-time Turing machines.},
author = {Ferrere, Thomas and Henzinger, Thomas A and Saraç, Ege},
location = {Oxford, UK},
pages = {394 -- 403},
publisher = {IEEE},
title = {{A theory of register monitors}},
doi = {10.1145/3209108.3209194},
volume = {Part F138033},
year = {2018},
}
@inproceedings{156,
abstract = {Imprecision in timing can sometimes be beneficial: Metric interval temporal logic (MITL), disabling the expression of punctuality constraints, was shown to translate to timed automata, yielding an elementary decision procedure. We show how this principle extends to other forms of dense-time specification using regular expressions. By providing a clean, automaton-based formal framework for non-punctual languages, we are able to recover and extend several results in timed systems. Metric interval regular expressions (MIRE) are introduced, providing regular expressions with non-singular duration constraints. We obtain that MIRE are expressively complete relative to a class of one-clock timed automata, which can be determinized using additional clocks. Metric interval dynamic logic (MIDL) is then defined using MIRE as temporal modalities. We show that MIDL generalizes known extensions of MITL, while translating to timed automata at comparable cost.},
author = {Ferrere, Thomas},
location = {Oxford, UK},
pages = {147 -- 164},
publisher = {Springer},
title = {{The compound interest in relaxing punctuality}},
doi = {10.1007/978-3-319-95582-7_9},
volume = {10951},
year = {2018},
}
@inproceedings{182,
abstract = {We describe a new algorithm for the parametric identification problem for signal temporal logic (STL), stated as follows. Given a densetime real-valued signal w and a parameterized temporal logic formula φ, compute the subset of the parameter space that renders the formula satisfied by the signal. Unlike previous solutions, which were based on search in the parameter space or quantifier elimination, our procedure works recursively on φ and computes the evolution over time of the set of valid parameter assignments. This procedure is similar to that of monitoring or computing the robustness of φ relative to w. Our implementation and experiments demonstrate that this approach can work well in practice.},
author = {Bakhirkin, Alexey and Ferrere, Thomas and Maler, Oded},
booktitle = {Proceedings of the 21st International Conference on Hybrid Systems},
isbn = {978-1-4503-5642-8 },
location = {Porto, Portugal},
pages = {177 -- 186},
publisher = {ACM},
title = {{Efficient parametric identification for STL}},
doi = {10.1145/3178126.3178132},
year = {2018},
}
@inproceedings{81,
abstract = {We solve the offline monitoring problem for timed propositional temporal logic (TPTL), interpreted over dense-time Boolean signals. The variant of TPTL we consider extends linear temporal logic (LTL) with clock variables and reset quantifiers, providing a mechanism to specify real-time constraints. We first describe a general monitoring algorithm based on an exhaustive computation of the set of satisfying clock assignments as a finite union of zones. We then propose a specialized monitoring algorithm for the one-variable case using a partition of the time domain based on the notion of region equivalence, whose complexity is linear in the length of the signal, thereby generalizing a known result regarding the monitoring of metric temporal logic (MTL). The region and zone representations of time constraints are known from timed automata verification and can also be used in the discrete-time case. Our prototype implementation appears to outperform previous discrete-time implementations of TPTL monitoring,},
author = {Elgyütt, Adrian and Ferrere, Thomas and Henzinger, Thomas A},
location = {Beijing, China},
pages = {53 -- 70},
publisher = {Springer},
title = {{Monitoring temporal logic with clock variables}},
doi = {10.1007/978-3-030-00151-3_4},
volume = {11022},
year = {2018},
}
@inproceedings{183,
abstract = {Fault-localization is considered to be a very tedious and time-consuming activity in the design of complex Cyber-Physical Systems (CPS). This laborious task essentially requires expert knowledge of the system in order to discover the cause of the fault. In this context, we propose a new procedure that AIDS designers in debugging Simulink/Stateflow hybrid system models, guided by Signal Temporal Logic (STL) specifications. The proposed method relies on three main ingredients: (1) a monitoring and a trace diagnostics procedure that checks whether a tested behavior satisfies or violates an STL specification, localizes time segments and interfaces variables contributing to the property violations; (2) a slicing procedure that maps these observable behavior segments to the internal states and transitions of the Simulink model; and (3) a spectrum-based fault-localization method that combines the previous analysis from multiple tests to identify the internal states and/or transitions that are the most likely to explain the fault. We demonstrate the applicability of our approach on two Simulink models from the automotive and the avionics domain.},
author = {Bartocci, Ezio and Ferrere, Thomas and Manjunath, Niveditha and Nickovic, Dejan},
location = {Porto, Portugal},
pages = {197 -- 206},
publisher = {Association for Computing Machinery, Inc},
title = {{Localizing faults in simulink/stateflow models with STL}},
doi = {10.1145/3178126.3178131},
year = {2018},
}
@inproceedings{636,
abstract = {Signal regular expressions can specify sequential properties of real-valued signals based on threshold conditions, regular operations, and duration constraints. In this paper we endow them with a quantitative semantics which indicates how robustly a signal matches or does not match a given expression. First, we show that this semantics is a safe approximation of a distance between the signal and the language defined by the expression. Then, we consider the robust matching problem, that is, computing the quantitative semantics of every segment of a given signal relative to an expression. We present an algorithm that solves this problem for piecewise-constant and piecewise-linear signals and show that for such signals the robustness map is a piecewise-linear function. The availability of an indicator describing how robustly a signal segment matches some regular pattern provides a general framework for quantitative monitoring of cyber-physical systems.},
author = {Bakhirkin, Alexey and Ferrere, Thomas and Maler, Oded and Ulus, Dogan},
editor = {Abate, Alessandro and Geeraerts, Gilles},
isbn = {978-331965764-6},
location = {Berlin, Germany},
pages = {189 -- 206},
publisher = {Springer},
title = {{On the quantitative semantics of regular expressions over real-valued signals}},
doi = {10.1007/978-3-319-65765-3_11},
volume = {10419},
year = {2017},
}