The rise of machine learning and cloud technologies has led to a remarkable influx of data within modern cyber-physical systems. However, extracting meaningful information from this data has become a significant challenge due to its volume and complexity. Timed pattern matching has emerged as a powerful specification-based runtime verification and temporal data analysis technique to address this challenge. In this paper, we provide a comprehensive tutorial on timed pattern matching that ranges from the underlying algebra and pattern specification languages to performance analyses and practical case studies. Analogous to textual pattern matching, timed pattern matching is the task of finding all time periods within temporal behaviors of cyber-physical systems that match a predefined pattern. Originally we introduced and solved several variants of the problem using the name of match sets, which has evolved into the concept of timed relations over the past decade. Here we first formalize and present the algebra of timed relations as a standalone mathematical tool to solve the pattern matching problem of timed pattern specifications. In particular, we show how to use the algebra of timed relations to solve the pattern matching problem for timed regular expressions and metric compass logic in a unified manner. We experimentally demonstrate that our timed pattern matching approach performs and scales well in practice. We further provide in-depth insights into the similarities and fundamental differences between monitoring and matching problems as well as regular expressions and temporal logic formulas. Finally, we illustrate the practical application of timed pattern matching through two case studies, which show how to extract structured information from temporal datasets obtained via simulations or real-world observations. These results and examples show that timed pattern matching is a rigorous and efficient technique in developing and analyzing cyber-physical systems.

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.

We describe a new algorithm for the parametric identification problem for signal temporal logic (STL), stated as follows. Given a dense-time 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.

Monitoring system behaviors using formal specifications appears to be an effective technique in analyzing cyber-physical systems. However, to achieve intended results in monitoring, specification languages need to be intuitive, elegant, and expressive at the first place. In this paper, we propose a metric extension of well-known Halpern-Shoham (hs) logic, called Metric Compass Logic (mcl), for monitoring purposes. Originally proposed for high-level temporal reasoning, the logic hs is very expressive and enables users to specify many temporal patterns in an intuitive and elegant way. As our main contribution, we present an offline monitoring technique for timed patterns specified in mcl. Our solution is built upon the framework developed for timed regular expressions (TRE) matching but explores a different (logical) direction. We finally study several practical features concerning atomic formulas and discuss a combined timed pattern speciication language with TRE.

In this paper we propose and implement a methodology for power reduction in digital circuits, closing the gap between conceptual (by designer) and local (by EDA) clock gating. We introduce a new class of coarse grained local clock gating conditions and develop a method for detecting such conditions and formally proving their correctness. The detection of these conditions relies on architecture characterization and statistical analysis of simulation, all done at the RTL. Formal verification is performed on an abstract circuit model. We demonstrate a significant power reduction from 33 to 40% of total power on a clusterized circuit design for video processing.

To program recently developed many-core systems-on-chip two traditionally separate performance optimization problems have to be solved together. Firstly, it is the parallel scheduling on a shared-memory multi-core system. Secondly, it is the co-scheduling of network communication and processor computation. This is because many-core systems are networks of multi-core clusters. In this paper, we demonstrate the applicability of modern constraint solvers to efficiently schedule parallel applications on many-cores and validate the results by running benchmarks on a real many-core platform.

Apprentissage de langages réguliers sur des alphabets de grandes tailles L'apprentissage de langages réguliers est un sous-ensemble de l'apprentissage automatique qui s'est révélé utile dans de nombreux domaines tels que l'intelli-gence artificielle, les réseaux de neurones, l'exploration de données, la vérification, etc. De plus, l'intérêt dans les langages définis sur des alphabets infinis ou de grande taille est croissant au fil des années. Même si plusierurs propriétés et théories se généralisent à partir du cas fini, l'apprentissage de tels langages est une tâche difficile.En effet, dans ce contexte, l'application naïve des algorithmes d'apprentissage traditionnel n'est pas possible.Dans cette thèse, nous présentons un schéma algorithmique général pour l'ap-prentissage de langages définis sur des alphabets infinis ou de grande taille, comme par exemple des sous-ensembles bornés de N or R ou des vecteurs booléens de grandes dimensions. Nous nous restreignons aux classes de langages qui sont acceptés par des automates déterministes symboliques utilisant des prédicats pour définir les transitions, construisant ainsi une partition finie de l'alphabet pour chaque état.Notre algorithme d'apprentissage, qui est une adaptation du L* d'Angluin, combine l'apprentissage classique d'un automate par la caractérisation de ses états, avec l'apprentissage de prédicats statiques définissant les partitions de l'alphabet. Nous utilisons l'apprentissage incrémental avec la propriété que deux types de requêtes fournissent une information suffisante sur le langage cible. Les requêtes du premier type sont les requêtes d'adhésions, qui permettent de savoir si un mot proposé appartient ou non au langage cible. Les requêtes du second type sont les requêtes d'équivalence, qui vérifient si un automate proposé accepte le langage cible; dans le cas contraire, un contre-exemple est renvoyé.Nous étudions l'apprentissage de langages définis sur des alphabets infinis ou de grande tailles dans un cadre théorique et général, mais notre objectif est de proposer des solutions concrètes pour un certain nombre de cas particuliers. Ensuite, nous nous intéressons aux deux principaux aspects du problème. Dans un premier temps, nous supposerons que les requêtes d'équivalence renvoient toujours un contre-exemple minimal pour un ordre de longueur-lexicographique quand l'automate proposé est incorrect. Puis dans un second temps, nous relâchons cette hypothèse forte d'un oracle d'équivalence, et nous la remplaçons avec une hypothèse plus réaliste où l'équivalence est approchée par un test sur les requêtes qui utilisent un échantillonnage sur l'ensemble des mots. Dans ce dernier cas, ce type de requêtes ne garantit pas l'obtention de contre-exemples, et par conséquent de contre-exemples minimaux. Nous obtenons alors une notion plus faible d'apprent-issage PAC (Probably Approximately Correct), permettant l'apprentissage d'une approximation du langage cible.Tout les algorithmes ont été implémentés, et leurs performances, en terme de construction d'automate et de taille d'alphabet, ont été évaluées empiriquement.

Extrinsic apoptosis is a programmed cell death triggered by external ligands, such as the TNF-related apoptosis inducing ligand (TRAIL). Depending on the cell line, the specific molecular mechanisms leading to cell death may significantly differ. Precise characterization of these differences is crucial for understanding and exploiting extrinsic apoptosis. Cells show distinct behaviors on several aspects of apoptosis, including (i) the relative order of caspases activation, (ii) the necessity of mitochondria outer membrane permeabilization (MOMP) for effector caspase activation, and (iii) the survival of cell lines overexpressing Bcl2. These differences are attributed to the activation of one of two pathways, leading to classification of cell lines into two groups: type I and type II. In this work we challenge this type I/type II cell line classification. We encode the three aforementioned distinguishing behaviors in a formal language, called signal temporal logic (STL), and use it to extensively test the validity of a previously-proposed model of TRAIL-induced apoptosis with respect to experimental observations made on different cell lines. After having solved a few inconsistencies using STL-guided parameter search, we show that these three criteria do not define consistent cell line classifications in type I or type II, and suggest mutants that are predicted to exhibit ambivalent behaviors. In particular, this finding sheds light on the role of a feedback loop between caspases, and reconciliates two apparently-conflicting views regarding the importance of either upstream or downstream processes for cell-type determination. More generally, our work suggests that these three distinguishing behaviors should be merely considered as type I/II features rather than cell-type defining criteria. On the methodological side, this work illustrates the biological relevance of STL-diagrams, STL population data, and STL-guided parameter search implemented in the tool Breach. Such tools are well-adapted to the ever-increasing availability of heterogeneous knowledge on complex signal transduction pathways.

Reducing the effects of off-chip memory access latency is a key factor in exploiting efficiently embedded multicore platforms. We consider architectures that admit a multi-core computation fabric, having its own fast and small memory to which the data blocks to be processed are fetched from external memory using a DMA (direct memory access) engine, employing a double- or multiple-buffering scheme to avoid processor idling. In this paper we focus on application programs that process two dimensional data arrays and we determine automatically the size and shape of the portions of the data array which are subject to a single DMA call, based on hardware and applications parameters. When the computation on different array elements are completely independent, the asymmetry of memory structure leads always to prefer one-dimensional horizontal pieces of memory, while when the computation of a data element shares some data with its neighbors, there is a pressure for more "square" shapes to reduce the amount of redundant data transfers. We provide an analytic model for this optimization problem and validate our results by running a mean filter application on the CELL simulator.

In this paper we investigate a general approach to automate some deployment decisions for a certain class of applications on multi-core computers. We consider data-parallelizable programs that use the well-known double buffering technique to bring the data from the off-chip slow memory to the local memory of the cores via a DMA (direct memory access) mechanism. Based on the computation time and size of elementary data items as well as DMA characteristics, we derive optimal and near optimal values for the number of blocks that should be clustered in a single DMA command. We then extend the results to the case where a computation for one data item needs some data in its neighborhood. In this setting we characterize the performance of several alternative mechanisms for data sharing. Our models are validated experimentally using a cycle-accurate simulator of the Cell Broadband Engine architecture.

We develop a stochastic local search algorithm for finding Pareto points for multi-criteria optimization problems. The algorithm alternates between different single-criterium optimization problems characterized by weight vectors. The policy for switching between different weights is an adaptation of the universal restart strategy defined by [LSZ93] in the context of Las Vegas algorithms. We demonstrate the effectiveness of our algorithm on multi-criteria quadratic assignment problem benchmarks and prove some of its theoretical properties.

We develop a computational framework for solving the problem of finding the cheapest configuration (in terms of the number of processors and their respective speeds) of a multiprocessor architecture on which a task graph can be scheduled within a given deadline. We then extend the problem in three orthogonal directions: taking communication volume into account, considering the case where a stream of instances of the task graph arrives periodically and reformulating the problem as a bi-criteria optimization for which we approximate the Pareto front.

Under-determined dynamical systems are those that need additional information in order to produce simulation traces. This information may correspond to initial conditions, parameter values or dynamic external influences. The paper discusses this issue and surveys some common approaches to reconcile this fact with the practice of simulation.

This paper is concerned with reachable set computation for non-linear systems using hybridization. The essence of hybridization is to approximate a non-linear vector field by a simpler (such as affine) vector field. This is done by partitioning the state space into small regions within each of which a simpler vector field is defined. This approach relies on the availability of methods for function approximation and for handling the resulting dynamical systems. Concerning function approximation using interpolation, the accuracy depends on the shapes and sizes of the regions which can compromise as well the speed of reachability computation since it may generate spurious classes of trajectories. In this paper we study the relationship between the region geometry and reachable set accuracy and propose a method for constructing hybridization regions using tighter interpolation error bounds. In addition, our construction exploits the dynamics of the system to adapt the orientation of the regions, in order to achieve better time-efficiency. We also present some experimental results on a high-dimensional biological system, to demonstrate the performance improvement.

In this talk I present my own perspective on the beginning (I refer mostly to the period 1988-1998) of hybrid systems research at the computer science side, focusing on the contributions of the late Amir Pnueli, mildly annotated with some opinions of mine.

We develop and implement a methodology for automatic abstraction of systems defined as networks of timed components modeled by timed automata. The abstraction technique yields an abstract model with much less clocks and states which over-approximate the timed behavior of the concrete system. Using this technique we can analyze timed system of size beyond the capabilities of contemporary analysis tools for timed automata.

In this paper we address the following problem: given an acyclic program scheme with if-then-else control structures, together with the duration of each procedure, and given an architecture consisting of n identical processors, compute offline a scheduling policy that guarantees minimal execution time (in the worst-case) for the entire program on this architecture. Since this is a problem of scheduling under uncertainty (the results of the branching decisions are not known in advance) it cannot be solved in a satisfactory manner using static or fixed priority schedulers but rather requires a state-dependent scheduling strategy. We use timed automata technology to derive such strategies using algorithms for finding shortest paths on game graphs.

In this article, we definetimed regular expressions, a formalism for specifying discrete behaviors augmented with timing information, and prove that its expressive power is equivalent to thetimed automataof Alur and Dill. This result is the timed analogue of Kleene Theorem and, similarly to that result, the hard part in the proof is the translation from automata to expressions. This result is extended from finite to infinite (in the sense of Büchi) behaviors. In addition to these fundamental results, we give a clean algebraic framework for two commonly accepted formalisms for timed behaviors, time-event sequences and piecewise-constant signals.

In this paper, we suggest a novel methodology for synthesizing switching controllers for continuous and hybrid systems whose dynamics are defined by linear differential equations. We formulate the synthesis problem as finding the conditions upon which a controller should switch the behavior of the system from one "mode" to another in order to avoid a set of bad states and propose an abstract algorithm that solves the problem by an iterative computation of reachable states. We have implemented a concrete version of the algorithm, which uses a new approximation scheme for reachability analysis of linear systems.

In this paper we define timed regular expressions, and extension of regular expressions for specifying sets of dense-time discrete-valued signals. We show that this formalism is equivalent in expressive power to the timed automata of Alur and Dill by providing a translation procedure from expressions to automata and vice versa. the result is extended to /spl omega/-regular expressions (Buchi's theorem).

Exponential upper and lower bounds on the size of the cascaded (Krohn-Rhodes) decomposition of automata are given. These results are used to obtain elementary algorithms for various translations between automata and temporal logic, where the previously known translations were nonelementary. The relevance of the result is discussed.>